No, he's almost certainly not. Keep in mind, I know nothing about PL. I'm solely relying on my background as a mathematician to think of the most reasonable in

No, he's almost certainly not. Keep in mind, I know nothing about PL. I'm solely relying on my background as a mathematician to think of the most reasonable interpretation for what he's saying. He's saying something like, "You can axiomatize Peano Arithmetic in PL and explore the idea of provability therein because that's what PL was invented for. At first glance we might try to use something like PL to do what we're setting out to do, but it's so specialized that it winds up not being worthwhile." This makes more sense in the context of his paper, anyhow. Gödel's Incompleteness Theorem basically says that Peano Arithmetic can't prove its own consistency within PA unless it's inconsistent So, we could model PA inside another logical system (e.g., PL) which has notation for certain meta-mathematical statements like "P(X): it is provable that X". You'd then need to demonstrate that a version of PA axiomatized with this logic is both complete and sound WRT PA, etc. etc.