6
$\begingroup$

The incompleteness of first-order arithmetic is relatively easy to wrap your head around -- there are non-standard models of PA in which Godel's sentence has a non-standard Godel number and so is "provable" in the model, and therefore false. So us "understanding that Godel's sentence is actually true" is just us operating in a stronger system, like ZFC or second-order arithmetic, in which the standard model of $\mathbb{N}$ is uniquely pinned down.

But with second-order logic, we have statements which are actually true but unprovable under standard semantics.

This I'm confused by. What is the "stronger system" that proves Godel's sentence for SOL? Surely there is one, since we know that Godel's sentence is "true but unprovable" in SOL? What system are we operating in?

"How" do we know/what kind of system knows that there is no model in which Godel's sentence is false?

$\endgroup$
7
  • 5
    $\begingroup$ You're confusing the completeness of a logic with the completeness of a theory. First-order logic is complete. $\endgroup$ Commented Sep 9, 2020 at 9:05
  • 2
    $\begingroup$ Sorry, I just used the wrong phrase. I know they are different, and I'm precisely asking about the incompleteness of second-order logic. $\endgroup$ Commented Sep 9, 2020 at 9:27
  • $\begingroup$ I gave this answer some time ago addressing the two notions of completeness. Perhaps this may help. $\endgroup$ Commented Sep 9, 2020 at 9:27
  • $\begingroup$ But if you're talking about the incompleteness of second-order logic, what does a Gödel sentence have to do with it? $\endgroup$ Commented Sep 9, 2020 at 9:28
  • 1
    $\begingroup$ We prove that in ZFC, which can interpret second-order logic, and prove that there is a unique model of second-order arithmetic. $\endgroup$ Commented Sep 9, 2020 at 9:30

1 Answer 1

Reset to default
5
$\begingroup$

Be careful with the definitions, and the answer should fall out nicely. We say that an FOL theory is syntactically complete iff it proves or disproves every sentence over its language. We say that FOL is semantically complete because for every set $A$ of FOL axioms over language $L$ and sentence $Q$ over $L$ such that every model of $A$ satisfies $Q$, we can prove (within the deductive system for FOL) $Q$ from $A$. These are two completely different concepts, but the qualifier before "complete" is often dropped because the first is about theories and the second is about logics (with associated deductive systems).

SOL (second-order logic) has two main flavours, one being Henkin semantics and the other being full semantics. SOL has a computable deductive system that is complete for Henkin semantics (since it can be reduced to FOL), but does not have any computable deductive system for full semantics. So although PA2 (second-order PA) under full semantics has a unique model under isomorphism, there is no computable deductive system that proves all and only its true statements.

So "provable in SOL" is not a well-defined notion for full semantics, because there is no computable notion of "proof" for full semantics. We could say that $\text{Th}(ℕ)$ proves all arithmetical sentences that are truths of PA2 under full semantics, but that is useless since $\text{Th}(ℕ)$ is not computable. Also, there is no such thing as "the Godel sentence for SOL", because Godel's theorems (even when generalized) are about computable formal systems. See here for the question about the Godel sentence for PA2 under Henkin semantics; of course it fails to prove it.

And all these can be proven in a meta-system like ZFC. That is, ZFC proves that every model of PA2 under full semantics is isomorphic to $ℕ$ (constructed from the minimal inductive set), and so on...

$\endgroup$
8
  • 1
    $\begingroup$ +1. Note that exactly this argument leads to the result that the entailment relation for SOL is not SOL-definable (using the standard semantics, which is right and proper :P). Going back to FOL, keep in mind that the fact that the entailment relation for FOL is FOL-definable is highly nontrivial (a priori it's $\Pi^1_1$, and even that requires an invocation of Lowenheim-Skolem): this is what the completeness theorem (+ the arithmetization of syntax) does for us. $\endgroup$ Commented Sep 11, 2020 at 3:23
  • $\begingroup$ Isn't the situation even worse for full semantics? That is, any proof procedure that is sound and consistent must be incomplete, even if non-computable or non-finitistic. For if there were any sound, complete, and consistent procedure $\rhd$, soundness would entail that $PA_2\rhd G$ (Gödel sentence for $PA$), consistency that not-($PA_2\rhd\neg G$), and completeness that $PA_2\nvDash\neg G$, which entails existence of the non-standard full model for $PA_2$, a contradiction. That is there are no candidates whatsoever for proof procedures for full semantics. $\endgroup$ Commented Feb 19, 2021 at 10:38
  • $\begingroup$ Second thoughts: actually you could take $\{A\mid PA_2\vDash A\}$ (for full semantics) as an axiomatic basis, that is trivially sound and complete. $\endgroup$ Commented Feb 19, 2021 at 10:47
  • 1
    $\begingroup$ @MadHatter: Ah, yes, sorry I misinterpreted your comment, but that didn't change anything, since indeed the full second-order theory of ℕ would be sound and complete. Regarding Turing jumps, first make sure you understand the proof of the generalized incompleteness theorem given in the linked post, and then note that the same theorem and proof holds if you change "program" to mean "program that can use the halting oracle (i.e. the set encoding all answers to the halting problem)". That is what is known as relativizing the theorem (to the halting oracle) as briefly mentioned over there as well. $\endgroup$ Commented Feb 19, 2021 at 19:36
  • 1
    $\begingroup$ Note that the halting oracle is also the first Turing jump. The $k+1$-th Turing jump is defined as the halting oracle for programs that can invoke the $k$-th Turing jump. The relativization works for any finite Turing jump because halting of a given program using a fixed finite Turing jump can be expressed as an arithmetical sentence. This fails once we reach the $ω$-th Turing jump, because Th(ℕ) can be computed using the $ω$-th Turing jump. Does that help? =) $\endgroup$ Commented Feb 19, 2021 at 19:38

You must log in to answer this question.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.