# Practical Foundations of Mathematics

## 2.8  Higher Order Logic

Well-foundedness is a second order property because it is defined by quantifying the induction scheme over all predicates q[x]. In higher order logic, predicates (or, by comprehension, subsets) are first class citizens, allowing quantification over predicates on predicates.

First order schemes   Before ascending to the second order, let us note first that there is a tradition (with almost a strangle-hold over twentieth century logic [ Sha91]) of reading any quantification over predicates or types as a scheme to be instantiated by each of the formulae which can be defined in the first order part. This has a profound qualitative effect.

REMARK 2.8.1 The completeness of first order model theory - the fact that the syntax and semantics exactly match (Remark 1.6.13) - has strange corollaries for the cardinality of its models. If a theory has arbitrarily large finite models then it has an infinite one (the compactness theorem), and in this case there are models of any infinite cardinality (the Löwenheim-Skolem Theorems). Second order logic has no such property.

In particular, first order logic is unable to characterise N or R up to isomorphism. Abraham Robinson [Rob66 ] exploited this fact to develop non-standard analysis: it is possible to construct models which obey exactly the same first order statements as the standard R, but which contain infinite or infinitesimal magnitudes. If we can demonstrate some first order property in the non-standard structure, possibly employing infinitesimals, then it also holds in the standard one. Since results in the differential calculus can be obtained very rapidly using this technique, it is sometimes advocated as a way of teaching this subject, but it is easy to forget that it depends on a rather sophisticated logical phenomenon.

The first order theory of R is of algebraic interest in itself. It suffices to say that -1 is not a sum of squares, and every odd-degree polynomial equation has a root, cf Example 2.5.2(c).

Addition and multiplication are definable by recursion from successor in second order Peano arithmetic (Example 2.7.8). Moj\.zesz Presburger (1930) showed that, in stark contrast, first order arithmetic with addition is decidable, as it can only express (in)congruence modulo fixed numbers and so-called linear programming. Arithmetic with addition and multiplication allows Diophantine equations, which are undecidable.

The type of propositions   Even though set theory can be presented in a first order meta-language, the subject itself is plainly intended to handle higher order logic. By the definition of powerset (Definition 2.2.5ff), the type of propositions is isomorphic to P(1).

NOTATION 2.8.2 We shall use the symbol W for the type of propositions. It is a hybrid of the Greek letter W (omega) used for this purpose in topos theory, and the digit 2, since classically W = {^,T}.

As Johann Lambert observed, any subset U Ì X gives rise to a function by x® T if x Î U and ^ otherwise. Intuitionistically, the correspondence can be made precise simply by a change of notation.

PROPOSITION 2.8.3 P(X) º WX.

PROOF: Write lx:X.f instead of {x:X|f[x]} for the term of type P(X) corresponding to the predicate f[x] . The membership relation (a Î U) is application (Ua) and the b-, h- and equality rules for the powerset are special cases of those for the l-calculus. []

REMARK 2.8.4 The h-rule for the powerset says that

inter-provable propositions (fÛ y) are equal ( f = y),

so bi-implication (Û ) is a congruence (Definition  1.2.12). This special case of the extensionality axiom (Remark 2.2.9(a)) is rather mysterious (Exercise 2.54); Remark  9.5.10 considers what need there is for it.

In particular q is equivalent to (q = T), cf Exercise 2.21.

Definability of the connectives   In Remarks 2.3.11 and  2.7.10 we made use of the l-calculus to avoid the need to introduce new variable-binding operations for the (+E)- and (List  E)-rules.

REMARK 2.8.5 We may also introduce constants

T,^:W        equal:X® (X® W) and,or,implies: W® (W® W)        som-1mu e, all:(X® W)® W m-1mu ember = ev:X® ((X® W)® W),

and then treat \$x:X.f as an abbreviation for som-1mu e\mkern1mu(lx:X.f).

This is little more than a shift of notation, but there is a further reduction based on a more profound idea. In the following formulae (due to Russell) we use q for the variable bound by ", because we shall find that it always plays the same special role , namely that of the arbitrary conclusion or result type in the elimination rules for ^, Ú, +, \$ and  List.

PROPOSITION 2.8.6 In the second order predicate calculus,

omitted eqnarray* environment

where x has any type X (which may be W), u:X® W and the other variables are of type W. In fact the formulae on the right satisfy the introduction and elimination rules for the connectives, even when the latter are not in the language.

PROOF: Consider the third: f\vdash "q.(fÞ q)Þ q amounts to (Þ E ); for the converse put q = f. The other results are obtained by substituting a first order equivalence into this one. []

We shall give a detailed proof for the conjunction in Example  2.8.12, from which we see that these equivalences do not depend on the extensionality axiom (Remark  2.8.4). There is a similar result for equality, cf congruence, Definition 1.2.12.

PROPOSITION 2.8.7 [ Leibniz' principle, 1666]

 x = y \dashv \vdash "q.q[x]Û q[y ],
where x,y:X and q:X® W. In particular the same holds in the case X = W, where equality is replaced by bi-implication. []

Cantor's diagonalisation theorem

PROPOSITION 2.8.8 There is no injective function m:P(X)\hookrightarrow X.

PROOF: Suppose first that we also have p:X\twoheadrightarrow P(X) splitting m, ie pom = \idP(X). Put R = {y|\lnot (y Î p(y))} and z = m(R), so

omitted eqnarray* environment

Using a guarded quantifier (Remark 1.5.2), we may in fact define

 a[x,y]    as    "U:P(X). æè m(U) = x öø Þ y Î U,
whence p:x® {y:X|a[x,y]} satisfies the argument above because

omitted eqnarray* environment

since (m(U) = m(V))Û (U = V), as m is an injective function. []

According to Cantor (1891), P(X) is ``bigger than'' X, since there is an injective function x® {x} in one direction but none the other way. He was ignoring Galileo's 1638 warning about ``how gravely one errs in trying to reason about infinities by using the same attributes that we apply to finites,'' in response to the observation that the squares form a proper but equinumerous subset of N, from which he concluded that ``equal, greater and less have no place in the infinite.'' Cantor's interpretation has prevailed (so far), even though it is well known that his motivations were religious at least as much as they were mathematical [Dau79]. Much has also been made of the self- referential nature of this and similar results such as Gödel's Incompleteness Theorem [Hof79]. We shall return to these matters at the end of the book.

Second order types   Quantification over predicates was needed for induction, so (applying the ideas of Section 2.4) quantification over types should tell us something about recursion. We leave discussion of the type of types to the final section of the book.

EXAMPLE 2.8.9 If we delete the dependency on n, Peano induction for N becomes the second order formula

 "q.q® (q® q)® q,
whose proofs correspond to the Church numerals (Example  2.4.1).

DEFINITION 2.8.10 The second order polymorphic l-calculus was introduced independently in proof theory by Jean-Yves Girard (1972) and in programming by John Reynolds (1974). To the base types of the l-calculus (Section  2.3) it adds type variables, and an operation of `` quantification over types'' (a),

 omitted prooftree environment
where we list the free type variables (a, b, ...) together with the ordinary variables (x, y, ...) on the left of the turnstile, subject to the condition that for each ordinary variable x:V in G, any free type variables in V must occur beforehand (Definition  2.2.8). In particular, when we write `` G,a'' as a context, we presuppose that G was already a valid context, so a must not be free in the type of any variable x Î G. This is important because, if x Î FV(p), then x remains free in la.p in the (PÁ )-rule.

 omitted prooftree environment        omitted prooftree environment
Chapter 11 of [GLT89] provides an accessible introduction to this very powerful calculus. In particular it can define many interesting pure types, whereas predicative type theory cannot get off the ground without some user-supplied base types. Girard argues that it has the advantage of eliminating a lot of the ah doc type declarations in programming languages. The (strong) normalisation theorem holds ( op. cit. , Chapter 15), from which it follows that the closed normal forms of the type called N below are numerals.

Examples 9.6.10 briefly describe some models of this calculus.

REMARK 2.8.11 The type analogue of Proposition 2.8.6 would be

omitted eqnarray* environment

but John Reynolds showed that the type Pq.((P(P(q))® q)® q) violates Cantor's theorem.

EXAMPLE 2.8.12 Consider the fifth of these in detail.

 0    p4 = p2(p3):y® q    = -125pt omitted proofbox environment \vtop \proofvbl1:UxV \proofvbl7 = lq.l\proofvbl2.\proofvbl6