**MW:** Recap: we showed that PA^{T} implies Φ_{T}, where Φ_{T} is the set of all formulas

Now we have to show the converse, that PA+Φ_{T} implies PA^{T}. But first let’s wave our hands, hopefully shaking off some intuition, like a dog shaking off water.

Below is a diagrammatic description of PA^{T}. The outer rectangle contains all models of PA, the inner oval contains all those that are (isomorphic to) ω’s of models of *T*. In other words, all models of PA* ^{T}*. Now let’s say φ is a sentence that cannot be proved using only PA, but

*can*be proved from

*T*. So for

*T*=ZF, φ could be the Paris-Harrington principle, or Goodstein’s theorem, or Con(PA). The blue region represents all the models where φ holds. So it includes the oval, but not all of the rectangle. The oval is the intersection of all such blue regions, as φ ranges over all of PA

*. If φ were provable from PA, then it would paint the entire rectangle blue.*

^{T}Next I want to take a second look at Φ_{T}. I’m going to turn its formulas inside-out and upside-down. Start with

The contrapositive is

Basic results from proposition logic tells us that for *any* sentence φ and *any* theory *T*, ¬Con(*T*+φ) is equivalent to *T*⊢¬φ. (“Proof by contradiction”.) So we have

Since φ ranges over *all* sentences of the language of PA, we might as well replace ¬φ with φ. Upshot: Φ_{T} is equivalent to

Let me explain the quote marks. Provability is a syntactic property, an assertion about strings of symbols. Or maybe I should say strings of strings of symbols. We can code syntactic claims into PA; the quoted stuff stands for the formalization of that claim into the language of PA. Kind of like the corner brackets for Gödel numbers, but more general.

The sentences of Φ_{T} say “Trust *T*.” In other words, “If *T* proves it, then it’s true.”

Let’s take a second look at the implication . We want to show that the formula “paints the oval blue”, i.e., holds in all models of *T*. Well, if , then “it stands to reason” that φ should hold in the of a model of *T*. That’s the intuition, at least.

As before, some subtleties lurk, but not enough to derail the conclusion. We must interpret the assumption “” *inside* the model . The proof of could have non-standard length! The trick is to bring the whole intuitive argument inside the model of *T*, which we can do thanks to the items mentioned last time: the Reflection Principle of ZF, and the existence of a formal truth predicate for formulas with up to *d* quantifiers (for any given *d*).

The reverse implication, , takes less work, though there is one fine point. Suppose *T* yields . Then some finite fragment does, say

.

In fact (this is the fine point),

.

Why? Well, if *T _{n}* proves something, then PA can

*prove*that it proves it. People often argue (correctly) that if the Goldbach conjecture is false, then it’s

*provably*false in PA: if we have a counterexample, we can check that it

*is*a counterexample with a finite calculation, which we can code into PA. The same holds for . Technically this is known as the Σ

_{1}-completeness of PA. Both “

*T*proves φ” and “the Goldbach conjecture is false” are Σ

_{n}_{1}statements, unlike “there are infinitely many prime pairs”, which is Π

_{2}. It’s quite conceivable that the prime pair conjecture could go either way without PA having a proof.

As we saw earlier, Φ_{T} is equivalent to the collection of all statements of this form:

.

So in PA+Φ_{T}, we can prove both and , for any φ in PA^{T}. Modus ponens takes it from there!