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: metamathematics 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 } O^{2} 

together with operationsymbols id and compose
satisfying the axioms for a category. Then we may add constants
unit,empty Î O and operations
product, coproduct, exponential :OxO® O 

to this language, together with those for the corresponding direct and indirect
operations, b and hrules, 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 homset, in particular
N\twoheadrightarrow H[unit,P],
where P is the internal version of P(N)
(as long as the sorts, operationsymbols 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 metanotation
for substitution and proofs. It might be the set of distinct symbols used
in this book, including my T_{E}X macros for proof trees and boxes, which
specify the twodimensional 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 p_{1},\qq G_{1},\qq f_{1}],¼, ok[\qq p_{k},\qq G_{k},\qq f_{k}] \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 nonempty equaliser
Æ\subsetneqq {*q}\subsetneqq 1 ® ^{ yes }  \rTo_{no } U[coproduct (unit, unit)]. 
