Last time we looked at Tarski’s inductive definition of truth, expressed informally. We saw how for models of PA, it can be formalized as an infinite sequence of formulas True0, True1, …, formulas belonging to L(PA) itself. But not as a single formula in L(PA).
“Expressed informally” means, “in naive set theory”. ZF wouldn’t be worth its salt if it couldn’t handle Tarski’s definition. But there’s a catch. We know there has to be a catch, because one of the incarnations of the Undefinability Theorem says that no single formula in L(ZF) can define truth for all sentences of L(ZF). That is, for the “real universe” V.
Let L be a first-order language. L has a set of relation symbols, a set of function symbols, and a set of constants. So L can be packaged up as a set, once we establish some coding conventions; I won’t bother to spell them out. PA can handle syntax via Gödel numbering; it’s even easier in ZF. Syntactic elements, after all, are combinatorial objects, and ZF can deal with that! For example, I’m going to regard formulas in L as parse trees.
Let S be a set-based structure for a language L. This means that the domain of S (dom(S)) is a set and not a proper class. Therefore the relations and functions on the domain must also be sets. In fact, the whole structure can be packaged up as a set—the set S. Again I won’t spell out conventions, but they’re not hard to cook up. S should be a tuple, say (dom, rel, const, …); there should be functions telling us which relations of S interpret which relation symbols of L, etc.
Formalizing the Tarski definition for S as a structure for L, one obtains a formula True in L(ZF), with three free variables:
True(L,S,φ) means
S is a set-based structure for L and φ is a sentence of L and S ⊧ φ.
There’s also a parametrized version, True(L,S,φ,u), where u is a finite list of elements of dom(S) to be assigned to the free variables in φ.
Let me flesh out the ideas, without going full formal. We start with the representation of formulas as parse trees. For example ∃x(φ(x)∧ψ(x)) has a node labeled ∃ with a child labeled ∧, which in turn has two subtrees for φ(x) and ψ(x). For clarity, I’ll label nodes with complete subformulas: ∃x(φ(x)∧ψ(x)) and φ(x)∧ψ(x) instead of just ∃ and ∧, for example.
Even if the tree represents a closed formula, it may contain subtrees whose formulas are not closed. I’m going to associate an instantiation tree with the parse tree. The nodes of the instantiation tree contain sets of closed formulas, in the expanded language where we’ve added a name for every element of the domain of S. Here’s the idea: let’s say a subtree of the parse tree represents a subformula ψ(x1,…,xn), with free variables as shown. We populate the corresponding node of the instantiation tree with all possible closed formulas ψ(c1,…,cn), where the c‘s are names of elements of dom(S).
Here’s a picture for ∃x(φ(x)∧ψ(x)).
(Since φ(x) and ψ(x) represent subformulas with their own internal structure, there are more nodes below the ones displayed. Also, I’ve picked three names a,b,c to suggest the whole crew of all possible names. Add “…” if you like.)
The truth evaluation of an instantiation tree assigns a truth-value to every formula living in the tree. The rules are just what you’d expect. For example, φ(a)∧ψ(a) is assigned ‘true’ iff φ(a) and ψ(a) are both assigned ‘true’. And a node ∃xθ(x) is assigned ‘true’ iff some formula θ(c) of the child node is assigned ‘true’.
ZF is powerful enough to:
- define the notion of an instantiation tree;
- show that there is exactly one instantiation tree for every parse tree;
- define the notion of a truth evaluation function eval for an instantiation tree;
- prove that there is exactly one such eval for any instantiation tree.
Informally you do a “bottom up” evaluation, just the way compilers evaluate expressions. When you formalize all this in ZF, you’ll end up something like this, for the definition of eval:
eval is a function from the closed formulas in the nodes of the instantiation tree X to {true, false}, and
(∀ nodes p in X) (∀ formulas φ in p) […]
There’s a lot of hair in those three dots, […]. Stuff saying how eval(φ∧ψ) has the right value, likewise eval(∃xθ(x)). We do a scan over the tree, checking things locally (i.e., for a node and its immediate children). Here is the pivotal point: we’ll need one more quantifier, to handle the case of eval(∃xθ(x)). We won’t need a quantifier for each quantifier appearing in the tree—the tree could have a thousand ∃’s, but our definition of eval will still need only those three ∀’s I mentioned. Syntactic quantifiers that are “buried in the parse tree” don’t “bleed through” to the ZF formula True(L,S,φ).
You can see why this definition requires the structure S to be set-based. If dom(S) wasn’t a set, but a proper class (like the “class of all sets” V), then the nodes of the instantiation tree would have to contain proper classes of formulas. But ZF forbids proper classes, at least formally. Even Gödel-Bernays set theory (GB) is very sniffy about them: a proper class can’t be an element of anything else, so it certainly can’t live inside a node of a tree. (Informally, people often refer to classes when discussing ZF. But this is just a way of referring to formulas in L(ZF) with a free variable.)
The upshot: True(L,S,φ) does not apply to the “real universe” (V,∈) as a structure for L(ZF). (V,∈) may be a ‘structure’ (depending on your definitions), but it’s not a set-based structure. Thus we avoid a confrontation with the Undefinability Theorem.
Last time we mentioned a nice property of Trued:
For all φ of depth at most d, N ⊧ φ iff N ⊧ Trued(⌜φ⌝).
We can prove something analogous, informally. For any sentence φ of L,
S ⊧ φ iff True(L,S,φ).
But we can’t do this formally in ZF, because True(L,S,φ) is our formalization of “S ⊧ φ”! (However, ZF can prove the equivalence of “N ⊧ φ” and “N ⊧ Trued(⌜φ⌝)” for shallow enough φ’s, now that we know how to formalize this in ZF.)
Last time we also had:
For all φ of depth at most d, PA ⊢ φ↔Trued(⌜φ⌝).
Again we have nothing really analogous. But the notions of ‘theory’, ‘proof’, and ‘consistency’ can be formalized in ZF. Then we have for any theory T in a language L
ZF ⊢ (S ⊧ T) ∧ (T ⊢ φ) →(S ⊧ φ)
The right hand side is vernacular: we formalize “S ⊧ T” and “S ⊧ φ” using the formula True, and “T ⊢ φ” using the ZF formalization of ‘proof’. Using this, ZF can formally prove that if a theory has a model, it is consistent. As for the converse, the usual proofs of the Completeness Theorem can be done inside ZFC.
Closing remark: I’ve written φ rather than ⌜φ⌝, because I said that formulas are parse trees. But it’s sometimes useful to think of formulas more informally, and to say that the parse tree, as a set, is the “Gödel set” of φ, and denote it by ⌜φ⌝.
Diagonal Argument 
I am wondering how much of the above can be formalized in PA. As we’ve discussed previously (and assuming I understood it properly), PA can understand finite sets perfectly. I’m unclear on whether it can understand infinite sets perfectly except for not knowing one exists, or whether, even when it’s told one exists, it is still crippled in reasoning about consequences of that. I’m guessing it probably is crippled, by not having omega to use as a “scaffolding” — but what if you also tell it “omega exists” (as a new hypothesis in every theorem you ask it to prove) — then can it do everything ZF can do?
I read somewhere that PA can prove that ZF can prove that PA is consistent. Do you agree? (I’m not sure how related this is to the prior question.)
(I hope my 2nd question’s answer is “definitely yes — just have PA check a (provided) valid ZF-proof of Con(PA), line by line, which even a weaker theory than PA can easily do.”
Here’s an analogy to conjure with:
PA : infinite sets :: ZF : proper classes.
So also, PA : finite sets :: ZF : sets. In ZF, we can formally define Truth provided we deal only with sets. In PA, we can define Truth provided we deal only with finite sets. This idea, when developed, gives so-called Δ0 satisfaction. The next post in this series treats this.
PA deals with infinite sets via predicates, i.e., formulas with free variables. That’s also how ZF deals with proper classes. Famous example: the axiom V=L, from Godel’s work on the CH, is really ∀x Λ(x), where Λ(x) is a formula expressing the fact that “x belongs to the proper class L”. For a PA example, to express formally Primes∩Evens={2}, we must write isEven(x)∧isPrime(x)↔x=2. (Of course, both isEven and isPrime have to be expanded out, not too hard for these predicates.)
The “manner of speaking” has one big limitation: we can’t quantify over proper classes in ZF, and over sets of numbers in PA.
Generally speaking, if T is a recursively axiomatized theory, and T ⊢ φ, then PA can prove that T proves φ. This is because “T ⊢ φ” amounts to a finite computation, and finite computations can be coded into PA and verified by PA. (This is called the Σ1-completeness of PA; see this post.) So yes, since ZF can prove Con(PA), PA can prove that ZF proves this. Speaking very anthropomorphically, it’s like Trudy checking the spelling of an essay in Russian using a dictionary; Trudy knows no Russian, and the essay is about Trudy.