It is important to distinguish the “complete” which is in Gödel’s completeness theorem and the “complete”-s in the incompleteness theorems, because these are not the same.
The first one presupposes two things, a) a syntax for a logical language, also containing a syntax for proofs b) a notion of model. Then, a combination of a) and b) is complete if every sentence which holds in all models is also syntactically provable.
The second one for our purpose can be summarized as follows: a syntax for a logical language is complete if for every sentence A, either A or its negation is provable. This sense of completeness does not mention models or semantics!
The main point in Gödel’s first incompleteness theorem is the ability to internally represent the syntax and proof theory of the language. In the case of first-order PA, all syntactic objects appear as certain finitely deep and finitely branching trees, and the job is to use arithmetic operations and properties to encode various finitary trees as just unary branching trees, i.e. the natural numbers. The syntax of second-order arithmetic does not differ in a relevant way; it is also just finitary trees, and since second-order arithmetic is a strict extension of first-order arithmetic, analogous internal encoding works in it as well.
That second-order logic “doesn’t have a computable deduction system” sounds false to me. It certainly does not have the completeness property (in the first sense) with respect to the standard notion of model, precisely because of Gödel’s incompleteness + ruling out nonstandard semantic natural numbers. But second-order logic still has finitary, recursively enumerable syntax and proofs, with decidable proof validation.
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.
It is important to distinguish the “complete” which is in Gödel’s completeness theorem and the “complete”-s in the incompleteness theorems, because these are not the same.
The first one presupposes two things, a) a syntax for a logical language, also containing a syntax for proofs b) a notion of model. Then, a combination of a) and b) is complete if every sentence which holds in all models is also syntactically provable.
The second one for our purpose can be summarized as follows: a syntax for a logical language is complete if for every sentence A, either A or its negation is provable. This sense of completeness does not mention models or semantics!
The main point in Gödel’s first incompleteness theorem is the ability to internally represent the syntax and proof theory of the language. In the case of first-order PA, all syntactic objects appear as certain finitely deep and finitely branching trees, and the job is to use arithmetic operations and properties to encode various finitary trees as just unary branching trees, i.e. the natural numbers. The syntax of second-order arithmetic does not differ in a relevant way; it is also just finitary trees, and since second-order arithmetic is a strict extension of first-order arithmetic, analogous internal encoding works in it as well.
That second-order logic “doesn’t have a computable deduction system” sounds false to me. It certainly does not have the completeness property (in the first sense) with respect to the standard notion of model, precisely because of Gödel’s incompleteness + ruling out nonstandard semantic natural numbers. But second-order logic still has finitary, recursively enumerable syntax and proofs, with decidable proof validation.
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.