Practical Foundations of Mathematics

Paul Taylor

9.6  Universes

The real test of foundations is of course how they support the edifice above. We have already demonstrated this throughout the book, but without going beyond its proper scope, we may ask what our logic has to say about its own construction: meta-mathematics as an example of mathematics. This does put the theory in jeopardy as the main question is consistency.

The description of the object language is in two parts: in these last two chapters we have said what it is to be a structure for a certain fragment of logic, and Chapters VI and VII constructed the free such structure.

REMARK 9.6.1 Example 8.1.12 gave the generalised algebraic theory of categories, which may be summed up semantically by the display

mor
x,y:O, f:H[x,y]
    src,tgt    O2
together with operation-symbols id and compose satisfying the axioms for a category. Then we may add constants unit,empty O and operations

productcoproductexponential :OxO O
to this language, together with those for the corresponding direct and indirect operations, b- and h-rules, cf Exercise  8.1 and Remark 9.5.8. With a little more work the class of monos can also be encoded, and hence the subobject classifier W and powersets (Exercise  9.58). In this way we can speak of an internal topos or other logical structure.

Gödel's incompleteness theorem   Consider first the free structure. Although Cantor's theorem is valid inside, from the outside the objects (contexts) and maps (substitutions of terms) are defined syntactically. So, by the techniques of Section  6.2, there is a recursive cover of each hom-set, in particular N\twoheadrightarrow H[unit,P], where P is the internal version of P(N) (as long as the sorts, operation-symbols and axioms are recursively enumerable). This is the Skolem paradox, page 2.2.9.

In 1931 Kurt Gödel used powers of primes to describe the enumeration, but recent authors seem to forget that any modern technology that they may employ to write books about his argument works with Gödel numbers as a matter of course. (These spectacularly infeasible calculations do, however, illustrate the need for exponentials, in both the logical and arithmetical senses.) Instead of numbers, it is more natural to use texts, ie terms of type List(A), where the alphabet A contains everything used in the syntax of [], including variables and the meta-notation for substitution and proofs. It might be the set of distinct symbols used in this book, including my TEX  macros for proof trees and boxes, which specify the two-dimensional arrangement of formulae using a linear stream of tokens. We also need a quoting function \qqdash :List(A)List(A) such as

\qq [3,0,5,7] = [0,4,1,6,8,0], relative to some A N .

THEOREM 9.6.2 Let [] be a consistent fragment of logic that is recursively axiomatisable and adequate for arithmetic. Then [] cannot prove its own consistency.

PROOF: Using primitive recursion, it is a decidable property of a triplet (p,G,f) of texts whether p is a well formed proof in [] whose last line is G\vdash f ( cf the proof of Proposition 6.2.6). This property can itself be expressed as a text ok List(A) containing (symbols in A for) variables x, y and z. Using the informal notation ok[\qq p,\qq G,\qq f] to indicate substitution for x, y and z, it satisfies

(a)
an introduction rule for each sequent rule r of [],
omitted prooftree environment
that ok[\qq p1,\qq G1,\qq f1],, ok[\qq pk,\qq Gk,\qq fk]  \vdash   ok[\qq r([(p)\vec]),\qq D,\qq q],

(b)
and an elimination rule that
ok[\qq p,\qq G,\qq f] \vdash   ok 
\qq _
p
 
,  \qq [  ], \qq $q .ok[\qq q,\qq G,\qq f]
,
where [`(p)] and q are obtained from p by structural recursion.

In this notation, inconsistency of [] is the statement

y $p.ok[\qq p,  \qq [  ],  \qq ^].
We shall show that this is equivalent to the Gödel sentence
q $p.ok
  \qq p,  \qq [y,z],   \qq \lnot $q.ok[\qq q,y,z]  
.
Note that y and z are not free variables of q - they are not variables at all, being quoted. Using the introduction rule (a) for r = (^E ), and for weakening by y and z, we have y\vdash q. Conversely, from q we deduce
$q.ok
\qq q,  \qq [  ],  \qq q
by the elimination rule (b), and also
$p.ok
\qq r(p),  \qq [  ],  \qq \lnot q
by (a), the introduction rule, where r is the cut that substitutes
\qq [y,z] for y     and    \qq \lnot $p .ok
\qq p,y,z] for z.
But then, using the introduction rule for r = (\lnot E ), we have q\vdash y. Hence if [] is consistent, \lnot y and \lnot q are true, but \lnot q actually says that \lnot q is unprovable. Notice that each f[x] \lnot ok[x,\qq [  ],\qq ^] is provable in [], but "x.f[x] is not, as this is \lnot y. []

One might suppose that Gödel's theorem says that the concept of truth is metaphysical, and needs simply to be replaced by provability. On the contrary, André Joyal (1973) considered the free model Cn[]L instead of Set for the outer world, and then the internal free model within that. As the objects, maps and equality in Cn[]L are given by the syntax of [], their truth is our provability, and the internal notion is different again.

In particular, the property y of inconsistency says that there is a map unit empty, ie that the global sections functor U H[unit,-] does not preserve the initial object ( cf Theorem  7.7.10(a)). The subobject classified by the Gödel sentence q is then the non-empty equaliser

\subsetneqq {*|q}\subsetneqq 1     yes   
\rTono U[coproduct (unitunit)].