|
|
|
|
|
by gedpeck
548 days ago
|
|
You know more than me. That is certain. However, my understanding is that the incompleteness results apply to only recursively enumerable axiomatic systems. I can find references for this. If I take the standard model of ZFC and collect all true statements in the one model of PA_2 and make that my axiomatic system then I have an axiomatic system that is not recursively enumerable and contains PA_1. It’s not a nice set of axioms. It’s not computable. But it shows that one can have an axiomatic system that contains PA_1 for which the Incompleteness theorems don’t apply. Andreas wrote “meaningless” not “nonsensical”. I’m not a pedant but the former term evokes in me the idea of “does not apply in this situation becausethe hypotheses of the incompleteness theorem are not satisfied”. From a mathematical logic book is the following. It’s the set up for the Incompleteness theorems. Suppose that A is a collection of axioms in the language of number theory such that A is consistent and is simple enough so that we can decide whether or not a given formula is an element of A. PA_2 is not such a system and as such the Incompleteness Theorems don’t apply. Maybe we are talking past each other. You know more than me. |
|
That's a matter of semantics as to what you consider the first incompleteness theorem to be precisely (of which there are several variants). Gödel's proof itself doesn't directly work for second-order logic. But the statement "if Γ is some axiomatic system that satisfies certain conditions, then for any sound proof calculus there is a sentence that isn't provable from Γ in this calculus" is true in second order logic too, it's just that the "failure" happens much "earlier" (and is in some sense obvious) than in the case of FOL.
> PA_2 is not such a system and as such the Incompleteness Theorems don’t apply.
I'm really not all that familiar with second-order PA, but it is my understanding that the set of its axioms is decidable. It consists of a finite collection of axioms plus one schema (comprehension axiom) which is valid when it's instantiated by any given sentence - but deciding whether something is a valid sentence is easy. Therefore, what you quoted applies to second-order PA too.