Godel in second-order logic?
post by Abhimanyu Pallavi Sudhir (abhimanyu-pallavi-sudhir) · 2020-07-26T07:16:26.995Z · LW · GW · No commentsThis is a question post.
Contents
Answers 6 Kutta 3 algon33 None No comments
I'm following the HAE sequence [Godel's Completeness and Incompleteness Theorem [? · GW]], and I can see what it means for first-order logic to be incomplete.
I don't understand how Godel's incompleteness theorem can still apply to second-order logic -- doesn't PA with second-order logic allow us to uniquely pin down a model?
But Godel's sentence can still be constructed, so second-order logic must still be incomplete -- I just don't understand how we can have models with a "weird idea of what it means to be a proof [? · GW]" if we don't have non-standard numbers.
I asked on Math Stackexchange and was told that second-order logic "doesn't have a computable deduction system". Unfortunately, I don't really understand what this means.
Answers
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 , either 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.
↑ comment by Abhimanyu Pallavi Sudhir (abhimanyu-pallavi-sudhir) · 2020-07-27T03:13:37.122Z · LW(p) · GW(p)
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?
Replies from: Kutta↑ comment by Kutta · 2020-07-27T09:56:29.778Z · LW(p) · GW(p)
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.
Second order logic can also arithmatise sentences, and also has fixed points. So the usual proofs carry over about the 1st incompleteness theorem. But there's an easier way to see this. There can't be any computable procedure to check if a second order sentence is valid or not, because if there was we could check if PA->Theorem and therefore decide Peano Arithmetic and therefore the Halting problem.
No comments
Comments sorted by top scores.