Gap in understanding of Logical Pinpointing

I had origi­nally found my­self very con­fused by how the sec­ond or­der ax­iom of in­duc­tion re­stricted PA to a sin­gle model, lead­ing to this dis­cus­sion where I thought do­ing so would vi­o­late the in­com­plete­ness the­o­rem.

What I mi­s­un­der­stood is that while the ax­iom schema of in­duc­tion effec­tively quan­tifies over prop­er­ties defin­able in PA, the SOL ver­sion quan­tifies over ALL prop­er­ties, in­clud­ing those you can’t even define in PA.

This seems like a re­ally sub­tle point that wasn’t ob­vi­ous to me from the ar­ti­cle, know­ing FOL but not SOL. I ac­tu­ally re­al­ized my mis­take when I saw that Eliezer was rep­re­sent­ing prop­er­ties as sets in the vi­sual di­a­gram.

Any­way, I thought oth­ers might benefit by learn­ing from my mis­take. Also, I’d like to point out that this defi­ni­tion of the nat­u­ral num­bers yields no pro­ce­dure that lets you pro­duce the­o­rems of PA as sec­ond-or­der logic has no com­putable com­plete defi­ni­tion of prov­abil­ity. Just use the ax­iom schema of in­duc­tion in­stead of the sec­ond or­der ax­iom of in­duc­tion and you will be able to pro­duce the­o­rems though.