4
$\begingroup$

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?

$\endgroup$
  • $\begingroup$ You should really make your question brief. I doubt you will find many peoples willing to read such a long post. Find a way to condense it. $\endgroup$ – Trismegistos Dec 16 '14 at 8:42
  • $\begingroup$ Second order logic syntax is already defined in a number of texts... it's higher order syntax that is muddy, particularly how you handle third order terms (second order function and predicate variables) as different types, as a sort of multi-sorted logic that starts to encroach on type theory. $\endgroup$ – dezakin Dec 16 '14 at 18:06
  • 1
    $\begingroup$ Have a look at the documentation for the HOL4 system, particularly the Logic manual that you can find via hol.sourceforge.net/documentation.html $\endgroup$ – Rob Arthan Dec 17 '14 at 23:14
3
$\begingroup$

For syntax and semantics of higher-type classical logic, you can see : Part I : CLASSICAL LOGIC, of

$\endgroup$
1
$\begingroup$

For higher order logic (as in Church's type theory), a good reference is Andrews "An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof".

The key is that it is based on lambda calculus (as a syntax for anonymous functions). A set is identified with its characteristic function $i \rightarrow o$, a predicate over sets is then of type $(i \rightarrow o) \rightarrow o$ and a predicate over predicates over sets is $((i \rightarrow o) \rightarrow o) \rightarrow o$ and so forth.

Here, then is an example, an axiom of extensionality for such third-order predicates: $$\forall x:((i \rightarrow o) \rightarrow o) \rightarrow o. p~x = q~x \Rightarrow p = q $$

Function application is just written as juxtaposition here, e.g. $p~x$.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.