MW: OK, back to the main plotline. Enayat asks for a “natural” axiomatization of PAT. Personally, I don’t find PAT all that “unnatural”, but he needs this for Theorem 7. (It’s been a while, so remember that Enayat’s T is a recursively axiomatizable extension of ZF.)
He defines ΦT to be the set of all formulas
In other words, φ ranges over all sentences (closed formulas) of L(PA), and Tn ranges over all finite “initial fragments” of T (i.e., the first n sentences of T). Enayat proves that PA+ΦT is equivalent to PAT.
Before looking at the proof of the equivalence, let’s ask: where did ΦT come from? What’s the meaning of these formulas 
The proof of the equivalence has some fine points. Start with the implication, 
has a false antecedent, so we’re home free! On the other hand, if φ does hold in 
You might think we’re done, but not so! Notice the Tn in Enayat’s ΦT . All we’ve shown so far is that 
This might seem like a minor issue. To show it’s not, let’s look at PA+¬Con(PA). (Feel familiar? The last post did the same thing with ZF in place of PA.) This is consistent! At least if PA is consistent, by Gödel’s second incompleteness theorem. Let’s call it PAinsecure, because it’s a self-doubting theory. Since it’s consistent, it has a model, call it N.
Well it’s quite simple. N has a proof of a contradiction of non-standard length.
Returning to
Resolving this steers us straight into one of the key issues in logic: the sort-of definability of truth.
As Tarski taught us, truth is undefinable—the notion, “m is the Gödel number of a statement in L(ZF) that is true”, can’t be expressed in L(ZF). But Tarski also gave us a definition of truth, expressed using set-theoretical concepts. Examine his definition carefully, and you walk away with two useful approximations to truth:
- For any natural number d, there’s a formula in L(ZF), Truthd(m), expressing the notion “m is the Gödel number of a statement of L(ZF) with at most d quantifiers that is true.”
- For any set K and any binary relation E on M, there’s a formula in L(ZF), Truth(K, E, m), expressing the notion “m is the Gödel number of a statement of L(ZF) that is true for the structure (K, E).”
Before Tarski and Gödel we had Skolem, who gave us the downward Löwenheim-Skolem theorem. (Well, the exact history is more complicated than I want to get into.) When you apply this to set theory (and skirt some pitfalls), you get what’s called the Reflection Principle. This tells us that there’s a model (K,E) of any finite number of true statements in L(ZF). Also K is a set. (Actually, it tells us more than that, but that’s all we need here.) Important: the Reflection Principle is a theorem of ZF.
Putting it all together: we argued, informally, that if φ holds in 
We still have to do the reverse implication, but maybe it’s time to catch our breath.
JB: [Panting.] Yeah… let me think about this a while as I catch my breath.
First of all, what’s this about sneaking around Tarski’s theorem on the undefinability of truth by restricting to sentences with at most d quantifiers? How come nobody ever told me about this? It seems like such cheap dodge. Sort of like: “I can’t tell you which sentences for true, but any d, I can tell you whether sentences of length at most d are true.” I know it’s not the same thing, but my instinctive reaction is “Wow, you’re a fussy sort of fellow, but that’s good enough for me.” Sort of like “I can’t give you all the money you might ask for, but for any d I can give you up to d dollars.”
Of course I can guess it must have to do with how there’s no way to string all the definitions of truth into a single one. If what you’re saying is true I guess there can’t be an algorithm that, given d, prints out the definition of truth for sentences with at most d quantifiers. So they must get more and more complicated in a nasty way.
Can you say a bit about how this works? I feel it’s a big hole in my education!
MW: It’s not nearly that bad! Or even surprising when you think about it. And there certainly is an algorithm to generate the series of formulas Truthd.
Let’s back up and look at Tarski’s definition of truth, aka satisfaction (⊨). It’s pretty much the obvious induction:
if and only if not
if and only if
and
if and only if for some
,
You can write the analogous clauses for ∨ and ∀ easily enough, or you can treat these as defined symbols. (I’m being brief, but any model theory book will have the details. Or my Basics of First-order Logic.)
We’re skirting the edges of philosophy here, or at least post 5. Don’t you need to know what ‘not’, ‘and’, and ‘for some’ mean, to make sense of the right hand sides?
Well yes. Initially view this definition through the rose-colored lenses of informal set theory, the basic mathematical intuition we absorbed in infancy with our mother’s milk. But when it comes time to formalize the definition, we have a few options.
We can treat this as an inductive definition of Truthd+1 in terms of Truthd. So it goes a little like this:
The corner brackets ⌜and⌝ as usual stand for the Gödel number of the formula, but they’re also a way to nod at some messy recursive functions—functions that can be coded into the language of PA. PA officially talks only about numbers, but via Gödel numbering it can also discuss strings of symbols. So the end of the Truthd+1 formula is saying, “If you have an existentially quantified formula ∃xα(x), then it’s true if and only if there is a number c such that α(c) is Trued; here α(c) is the result of substituting the numeral for c into the formula α(x).” The substitution function, fairly transparent at the formula level, becomes a tedious mess if you can refer only to the Gödel numbers of formulas. Kind of like those coded conversations in spy movies, where “The water buffaloes have grazed their fill and are herding towards the house with the sparrows” means something about troop movements. Still, PA is fully up to the task.
Textbooks have to spend serious time on this, but you should just take away two observations: (a) We obtain the formula for Truthd+1 by cobbling together (modified) copies of Truthd, plus connective tissue; (b) The occurrence of ∃c represents a genuine quantifier in the language of PA. In other words, the quantifiers of a closed formula α “bleed through” to the formula Truthd(⌜α⌝). Technically, Truthd is a Σd formula. So as d increases, the formulas Truthd become more and more complicated, but in a very uniform manner.
I guess we’re not actually working over PA, but over ZF. That makes it even easier. Each formula gets a Gödel set to represent it. Actually. the slickest approach is to code the formulas as parse trees. Representing finite trees as sets is something ZF can do in its sleep.
In your money analogy, we don’t have a single philanthropist, but an infinite series of philanthropists, who can give more and more moola.
As I said, this isn’t the only way to formalize truth. But as this theme will recur again and again, let’s leave it there for now.
JB: Hmm, I’m still confused about why you can’t parlay all these very systematically defined Truthd predicates into a single truth predicate, something that amounts to ∃dTruthd.
Of course I know from Tarski’s theorem on the undefinability of truth that this can’t work! But I still want to know why. It’s sort of like perpetual motion machines. If someone hands you a design for one, you can either invoke general laws to assure yourself it won’t work, or you can examine the design carefully to see exactly where it goes wrong. It all depends on how patient you’re feeling.
But okay, let’s leave it here for now: this is a bone I can chew on in my own spare time.
MW: What you’re suggesting would work if Truthd(u) was a single formula with two parameters, one being d. In other words, Truth(d,u). Then you could quantify over d. However, what we have is a sequence of ever longer and more complicated formulas indexed by d.
as a set of predicates whose free variables are chosen from the set S. The fact that B is a functor captures our ability to substitute variables, or in other words rename them.
