6 ms·

There are statements provably true about the natural numbers that can’t be proven in first order PA. Are such statements part of computer science? If so, how?

jerf 2y ago
That question contains so many false or unnecessary assumptions that it would take far longer to unpack them than it took you to type them, so I will limit myself to the observation that we do not even remotely confine ourselves to first order anything in computer science, nor should we.
- gedpeck 2y ago
  What false assumption did I make? I just pointed out a fact and asked a question. How many false assumptions could I have made with just one statement of fact and two questions? If you don’t have a valid answer to the question then don’t respond. I’m a mathematician and not a computer scientist. The first order PA axioms are recursively enumerable. Hence it’s clearly something of interest to computer scientists. The second order PA axioms aren’t so…are they part of computer science? What do computer scientists think about proofs in second order PA? There are no computable models of ZFC so wouldn’t it be the case that while computer scientists deal with ZFC that ZFC isn’t part of computer science? what is your definition of computer science? Physicists deal with a vast amount of mathematics but math isn’t physics. In the same way mathematics isn’t computer science. Overall I think most mathematicians would not consider mathematics as part of computer science.
  - immibis 2y ago
    why should computer science be limited to things that are first order PA?
    - gedpeck 2y ago
      It shouldn’t and I didn’t say it should. I gave a fact and asked a question. Why is PA_2 computer science? Computer science ought to be about computation, right? There are non-computable objects that mathematicians study. Is that part of computer science?
      - naasking 2y ago
        > There are non-computable objects that mathematicians study. What's an example of such a non-computable object? Constructionism is based on the fact that every proof is a construction, which corresponds to a program, so you're claiming that there are proofs that do not correspond to any construction/program, and I'm curious what that might look like.
        gedpeck 2y ago
        The set of statements about natural numbers that are true.
        naasking 2y ago
        Using the law of the excluded middle is definitely a shortcut in such proofs, but there is no proof I'm aware of that shows no comparable constructive proof is possible. We reason with non-computable objects all of the time, such constructions are simply never fully materialized, and the need to materialize them are typically eliminated in later stages to prove concrete results. It's a good example but I don't think it's sufficient to exclude math from computer science.
        Tainnor 2y ago
        Constructivism is not mainstream mathematics. The theorem that every vector space has a basis, something that is used fairly often, is actually equivalent to the axiom of choice, something that isn't valid in constructive logic. For many vector spaces you won't be able to write down a basis. And there are other examples, e.g. almost none of the automorphisms of C can be written down (only the identity and the conjugate map).
  - hughesjj 2y ago
    To be fair I've heard gripes about statistics, and sometimes even probability being considered as part of mathematics. The lines between (academic) fields are blurry -- academic fields do not form a set theoretic partitioning over areas of study.
  - semolinapudding 2y ago
    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...
- Vt71fcAqt7 2y ago
  >it would take far longer to unpack them than it took you to type them Why is this a barometer for whether to answer a question or unpack assumptions?
- justincredible 2y ago
  Would it take too long or is it just that the margin is too small?

jerf 2y ago

That question contains so many false or unnecessary assumptions that it would take far longer to unpack them than it took you to type them, so I will limit myself to the observation that we do not even remotely confine ourselves to first order anything in computer science, nor should we.

gedpeck 2y ago
What false assumption did I make? I just pointed out a fact and asked a question. How many false assumptions could I have made with just one statement of fact and two questions? If you don’t have a valid answer to the question then don’t respond. I’m a mathematician and not a computer scientist. The first order PA axioms are recursively enumerable. Hence it’s clearly something of interest to computer scientists. The second order PA axioms aren’t so…are they part of computer science? What do computer scientists think about proofs in second order PA? There are no computable models of ZFC so wouldn’t it be the case that while computer scientists deal with ZFC that ZFC isn’t part of computer science? what is your definition of computer science? Physicists deal with a vast amount of mathematics but math isn’t physics. In the same way mathematics isn’t computer science. Overall I think most mathematicians would not consider mathematics as part of computer science.
- immibis 2y ago
  why should computer science be limited to things that are first order PA?
  - gedpeck 2y ago
    It shouldn’t and I didn’t say it should. I gave a fact and asked a question. Why is PA_2 computer science? Computer science ought to be about computation, right? There are non-computable objects that mathematicians study. Is that part of computer science?
    - naasking 2y ago
      > There are non-computable objects that mathematicians study. What's an example of such a non-computable object? Constructionism is based on the fact that every proof is a construction, which corresponds to a program, so you're claiming that there are proofs that do not correspond to any construction/program, and I'm curious what that might look like.
      - gedpeck 2y ago
        The set of statements about natural numbers that are true.
        naasking 2y ago
        Using the law of the excluded middle is definitely a shortcut in such proofs, but there is no proof I'm aware of that shows no comparable constructive proof is possible. We reason with non-computable objects all of the time, such constructions are simply never fully materialized, and the need to materialize them are typically eliminated in later stages to prove concrete results. It's a good example but I don't think it's sufficient to exclude math from computer science.
      - Tainnor 2y ago
        Constructivism is not mainstream mathematics. The theorem that every vector space has a basis, something that is used fairly often, is actually equivalent to the axiom of choice, something that isn't valid in constructive logic. For many vector spaces you won't be able to write down a basis. And there are other examples, e.g. almost none of the automorphisms of C can be written down (only the identity and the conjugate map).
- hughesjj 2y ago
  To be fair I've heard gripes about statistics, and sometimes even probability being considered as part of mathematics. The lines between (academic) fields are blurry -- academic fields do not form a set theoretic partitioning over areas of study.
- semolinapudding 2y ago
  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...
Vt71fcAqt7 2y ago
>it would take far longer to unpack them than it took you to type them Why is this a barometer for whether to answer a question or unpack assumptions?
justincredible 2y ago
Would it take too long or is it just that the margin is too small?