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.
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]
|
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
|
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
|
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),
|
|
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.
| |||||||||||||||||||||||||||||||||||||