I see. So the answer is that it is indeed true that Godel’s statement is true in all models of second-order PA, but unprovable nonetheless since Godel’s completeness theorem isn’t true for second-order logic?
Yes. To expand a bit, in fact the straightforward way to show that second-order arithmetic isn’t complete in the first sense is by using the Gödel sentence G.
G says via an encoding that G is not provable in second-order arithmetic. Since the only model (up to isomorphism) is the model with the standard natural numbers, an internal statement which talks about encoded proofs is interpreted in the semantics as a statement which talks about actual proof objects of second-order arithmetic. This is in contrast to first-order arithmetic where we can interpret an internal statement about encoded proofs as ranging over nonstandard numbers as well, and such numbers do not encode actual proof objects.
Therefore, when we interpret second-order G, we always get the semantic statement “G is not provable in second-order arithmetic”. From this and the soundness of the proof system, it follows that G is not provable. Hence, G holds in all models (recall that there is just one model up to isomorphism), but is not provable.
I see. So the answer is that it is indeed true that Godel’s statement is true in all models of second-order PA, but unprovable nonetheless since Godel’s completeness theorem isn’t true for second-order logic?
Yes. To expand a bit, in fact the straightforward way to show that second-order arithmetic isn’t complete in the first sense is by using the Gödel sentence G.
G says via an encoding that G is not provable in second-order arithmetic. Since the only model (up to isomorphism) is the model with the standard natural numbers, an internal statement which talks about encoded proofs is interpreted in the semantics as a statement which talks about actual proof objects of second-order arithmetic. This is in contrast to first-order arithmetic where we can interpret an internal statement about encoded proofs as ranging over nonstandard numbers as well, and such numbers do not encode actual proof objects.
Therefore, when we interpret second-order G, we always get the semantic statement “G is not provable in second-order arithmetic”. From this and the soundness of the proof system, it follows that G is not provable. Hence, G holds in all models (recall that there is just one model up to isomorphism), but is not provable.