| HN Mirror

https://mathoverflow.net/questions/97077/z-2-versus-second-o...

Do you have a reference for the second order induction schema being recursively enumerable? My understanding - I’m not a logician - is that the second order Peano Axioms are categorical. The Incompleteness theorems don’t apply to this system since the axioms are not recursively enumerable. The second order Axioms are different than second order Arithmetic.

In the following mathoverflow answer Nik says,

These are fundamental questions. We know that any computable set of axioms which holds of the natural numbers must also have nonstandard models.

The second order Peano Axioms are not computable since those axioms are categorical.

https://mathoverflow.net/questions/332247/defining-the-stand...

Are you of the opinion that mathematics is computer science? I have a hard time believing that the Jacobian Conjecture is computer science.

semolinapudding 547 days ago

If you look at the Wikipedia page for second order arithmetic, there is a definition in the language of first order logic as a two-sorted theory comprising a handful of basic axioms, the comprehension scheme, and the second-order induction axiom (in your first mathoverflow link, this is called Z_2):

https://en.wikipedia.org/wiki/Second-order_arithmetic#The_fu...

An other equivalent option would be to use the language of second order logic, where you only need a finite amount of axioms, because the comprehension scheme is already included in the rules of second order logic. This one is PA_2.

Since these definitions do not refer to anything uncomputable such as mathematical truth, both systems are clearly recursively enumerable. This means that Gödel's incompleteness theorem applies to both, in the sense that you can define a sentence in the language of arithmetic that is unprovable in Z_2 or PA_2, and whose negation is also unprovable.

All of these considerations have little to do with models or categoricity, which are semantic notions. I think your confusion stems from the fact that model theorists have the habit of using a different kind of semantics for Z_2 (Henkin semantics) and PA_2 (full semantics). Henkin semantics are just first order semantics with two sorts, which means that Gödel's completeness theorem applies and there are nonstandard models. Full semantics, on the other hand, are categorical (there is only one model), but this has nothing to do with the axioms not being recursively enumerable -- it is just because we use a different notion of model.

PS: I certainly do not consider mathematics to be included in computer science. Even though as a logician, I have been employed in both mathematics departments and computer science departments...

https://math.stackexchange.com/questions/4753432/g%C3%B6dels...

You know more than me on logic so I defer to your expertise.

Andreas Blass in the comments says that the Incompleteness results don’t apply to the second order Axioms (tabling about PA_2 here and not Z_2) and that the second order axioms are not computably enumerable. Maybe that’s the correct concept I was remembering from mathematical logic class. Don’t know if computably enumerable is the same as recursively enumerable but given what you’ve said I’m guessing they are different notions.

Consider the standard model of ZFC. Assume ZFC is consistent. Within this model there is one model of PA_2. Collect all true statements in this model of PA_2. Call that Super PA. That’s now my axiomatic system. I now have an axiomatic system that proves all true statements of arithmetic. Surely this set of axioms is not recursively enumerable.

Full semantics, on the other hand, are categorical (there is only one model), but this has nothing to do with the axioms not being recursively enumerable -- it is just because we use a different notion of model.

If those axioms were recursively enumerable then the Incompleteness theorems would apply, right?

What Noah Schweber says here seems pertinent:

https://math.stackexchange.com/questions/4972693/is-second-o...

semolinapudding 547 days ago

There's a bit of a definition issue at play here. When Andreas Blass and Noah Schweber say that there is no proof system for PA_2, they mean that there is no effective proof system that is complete for the full semantics. If you subscribe to their definition of a proof system, you end up saying that there is no such thing as a proof in PA_2, and thus that incompleteness is meaningless -- which I personally find a bit silly.

On the other hand, proof theorists and computer scientists are perfectly happy to use proof systems for second order logic which are not complete. In that case, there are many effective proof systems, and given that the axioms of PA_2 are recursively enumerable (they are in finite number!), Gödel's incompleteness will apply.

If you are still not convinced, I encourage you to decide on a formal definition of what you call PA_2, and what you call a proof in that system. If your proof system is effective, and your axioms are recursively enumerable, then the incompleteness theorem will apply.

Thanks for the reply.

> and that the second order axioms are not computably enumerable

He says that true sentences in second order logic aren't computably enumerable, he's not talking about the axioms.

> Don’t know if computably enumerable is the same as recursively enumerable

I've only ever seen them used as synonyms.

> Collect all true statements in this model of PA_2. Call that Super PA. That’s now my axiomatic system. I now have an axiomatic system that proves all true statements of arithmetic. Surely this set of axioms is not recursively enumerable.

What you call "Super PA" is called "the theory of PA". Its axioms are indeed not computably enumerable. That doesn't mean that the axioms of PA themselves aren't computably enumerable. And this much is true both for first and second order logic.

(edit: in fact, the set of Peano axioms isn't just computably enumerable, it's decidable - otherwise, it would be impossible to decide whether a proof is valid. This is at least true for FOL, but I do think it's also valid for SOL)

https://math.stackexchange.com/questions/617124/peano-arithm...

Thanks for the reply.

...it's decidable - otherwise, it would be impossible to decide whether a proof is valid.

Isn't that the whole issue with PA_2 vs. PA? In PA_2 with "full semantics" there is no effective procedure for determining if a statement is an axiom. In my mind this is what I mean by the incompleteness results not applying to PA_2. They do apply to Z_2 since that is an effective (computable?) system.

But Z2 is usually studied with first-order semantics, and in that context it is an effective theory of arithmetic subject to the incompleteness theorems. In particular, Z2 includes every axiom of PA, and it does include the second-order induction axiom, and it is still incomplete.

Therefore, the well-known categoricity proof must not rely solely on the second-order induction axiom. It also relies on a change to an entirely different semantics, apart from the choice of axioms. It is only in the context of these special "full" semantics that PA with the second-order induction axiom becomes categorical.

Thanks for the knoweledge. I'm going to read up more on this stuff.

> My understanding - I’m not a logician - is that the second order Peano Axioms are categorical. The Incompleteness theorems don’t apply to this system since the axioms are not recursively enumerable

Incompleteness does apply to second order arithmetic (it applies to every logical system that contains first order PA), but due to different reasons: second order logic doesn't have a complete proof calculus. "Second-order PA is categorical" means that there is only one model of second-order PA, that is, for every sentence P, either PA2 |= P or PA2 |= not(P), but you'll still have sentences P such that neither PA2 |- P nor PA2 |- not(P) - and for "practical" purposes, the existence of proofs is what matters.

https://math.stackexchange.com/questions/4753432/g%C3%B6dels...

I think you are wrong in your first sentence. Take the collection of all true statements and make that your axiomatic system.

Andreas Blass in the comments says that Incompleteness does not apply to PA_2.

> Take the collection of all true statements and make that your axiomatic system.

A complete proof system needs to be able to derive Γ |- φ for every pair Γ, φ such that Γ |= φ. Not just when Γ is the complete theory of some structure. Completeness of first-order logic (and its failure for second-order logic) is about the logical system itself, while the incompleteness theorems are about specific theories - people often mix these up, but they talk about very different things.

> Andreas Blass in the comments says that Incompleteness does not apply to PA_2.

He says something rather different, namely that its "meaningless". That's a value judgement. Incomplete proof calculi for second order logic do exist (e.g. any first-order proof calculus) and for those, what I wrote is true. Andreas Blass would probably just think of this as an empty or obvious statement.

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.

> However, my understanding is that the incompleteness results apply to only recursively enumerable axiomatic systems. I can find references for this.

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.