I know this is sort of a broad question, but I'm having trouble getting a handle on the syntax for higher order logic, when going from first order logic. Basically I want to be able to do resolution proofs in higher order logic since it works so well for first order logic.
The syntax of first order logic I understand as this:
A first order term is either a variable or a first order function of some arity. Functions of arity zero can be represented as constants. A first order function takes only terms as its arguments. There are an infinite number of first order element variables. There are an infinite number of free (constant) first order functions. Nothing else is a term.
A first order predicate takes only first order terms as arguments. Predicates that take no arguments can be represented as propositional constants.
A first order logical formula consists of predicates, and logical formula connected by logical connectives, including negation, conjunction, disjunction, and quantifiers. Quantifiers quantify element variables, either universal or existential. Logical connectives can connect to predicates or other logical formula. Nothing else is a logical formula.
Example first order statement: $\forall$x$\exists$y P(x,y) $\rightarrow$ Q(f(x), g(y))
Now, we can extend this to second order logic by allowing quantification of functions and predicates/relations. Now first order function constants and predicate constants are no longer required to be free constants, but may be bound variables. Other than that it's identical to first order logic. The semantics may be more complicated, because the completeness and compactness theorem no longer apply in full semantics, and higher order proof calculus may be more complicated because higher order Skolemization is more complicated and may require the axiom of choice, but the syntax isn't much different. But quantified functions and relations in second order logic still take first order terms and return first order terms and truth values respectively.
Using our first order example as quantified second order logic:
$\forall$P$\exists$Q$\forall$f$\exists$g$\forall$x$\exists$y P(x,y) $\rightarrow$ $Q(f(x), g(y))$
This seems pretty straightforward if I want to do resolution proofs in second order logic. I can use most of the same proof calculus as first order logic, with new rules for unifying function variables and predicate variables.
But when we go higher orders the syntax seems more muddy. Do we have second order terms as different types from first order terms? For instance I can have a third order function variable that takes a second order function variable as an argument... and have its domain be first order terms, or second order functions, of all sorts of different arities and signatures. Or a fourth order predicate that takes a third order function of a specific arity and a second order function, and a first order term. It looks to me like there's an explosion of syntactical complexity at third order logic and higher, but I haven't seen many explicit examples of third or higher order syntax.
In first and second order logic, as far as I understand, the only complexity of the signature of functions and relations is the arity; just how many arguments it takes. But it appears to me that the signature of higher order functions and relations is much more complicated, since higher order functions can take as arguments and have a domain more than just the first order terms.
I've heard higher order logic is similar to type theory, in that higher order terms are essentially different types, and higher order logic can be represented as many sorted first order logic. Can someone explain how higher order syntax is supposed to work? Or point me to a reference for formal syntax (or syntaxes?) for higher order logics?
