6 ms·

The axioms of second order Peano arithmetic are certainly recursively enumerable, in fact you can pick a formulation that only uses a finite number of axioms. A

The axioms of second order Peano arithmetic are certainly recursively enumerable, in fact you can pick a formulation that only uses a finite number of axioms. And second order arithmetic is much weaker than the type system of Lean, which is probably somewhere between Zermelo set theory and ZFC set theory in terms of proof-theoretic strength. More generally, I think that computer scientists (in particular PL theorists and type theorists) are much more likely to use powerful logics than mathematicians, with the obvious exception of set theorists.

gedpeck 2y ago
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. https://mathoverflow.net/questions/97077/z-2-versus-second-order-pa https://mathoverflow.net/questions/97077/z-2-versus-second-o... 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-standard-model-of-pa-so-that-a-space-alien-could-understand/332266#332266 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 2y 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_full_system 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...
  - gedpeck 2y ago
    You know more than me on logic so I defer to your expertise. https://math.stackexchange.com/questions/4753432/g%C3%B6dels-incompleteness-theorem-false-for-natural-numbers https://math.stackexchange.com/questions/4753432/g%C3%B6dels... 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-order-arithmetic-subject-to-g%C3%B6dels-first-incompleteness-theorem-if-s?rq=1 https://math.stackexchange.com/questions/4972693/is-second-o...
    - Tainnor 2y ago
      > 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)
- Tainnor 2y ago
  > 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.
  - gedpeck 2y ago
    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. https://math.stackexchange.com/questions/4753432/g%C3%B6dels-incompleteness-theorem-false-for-natural-numbers https://math.stackexchange.com/questions/4753432/g%C3%B6dels...
    - Tainnor 2y ago
      > 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.
      - gedpeck 2y 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.

gedpeck 2y ago

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. https://mathoverflow.net/questions/97077/z-2-versus-second-order-pa https://mathoverflow.net/questions/97077/z-2-versus-second-o... 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-standard-model-of-pa-so-that-a-space-alien-could-understand/332266#332266 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 2y 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_full_system 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...
- gedpeck 2y ago
  You know more than me on logic so I defer to your expertise. https://math.stackexchange.com/questions/4753432/g%C3%B6dels-incompleteness-theorem-false-for-natural-numbers https://math.stackexchange.com/questions/4753432/g%C3%B6dels... 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-order-arithmetic-subject-to-g%C3%B6dels-first-incompleteness-theorem-if-s?rq=1 https://math.stackexchange.com/questions/4972693/is-second-o...
  - Tainnor 2y ago
    > 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)
Tainnor 2y ago
> 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.
- gedpeck 2y ago
  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. https://math.stackexchange.com/questions/4753432/g%C3%B6dels-incompleteness-theorem-false-for-natural-numbers https://math.stackexchange.com/questions/4753432/g%C3%B6dels...
  - Tainnor 2y ago
    > 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.
    - gedpeck 2y 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.