MW: Recap: we showed that PAT implies ΦT, where ΦT is the set of all formulas
Now we have to show the converse, that PA+ΦT implies PAT. But first let’s wave our hands, hopefully shaking off some intuition, like a dog shaking off water.
Below is a diagrammatic description of PAT. 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 PAT. 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 PAT. If φ were provable from PA, then it would paint the entire rectangle blue.
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 
As before, some subtleties lurk, but not enough to derail the conclusion. We must interpret the assumption “
The reverse implication, 
In fact (this is the fine point),
Why? Well, if Tn 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
As we saw earlier, ΦT is equivalent to the collection of all statements of this form:
So in PA+ΦT, we can prove both 
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.
