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

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 T_EX  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

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₁,\qq G₁,\qq f₁],¼, 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

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