Timeline for Defining the standard model of PA so that a space alien could understand
Current License: CC BY-SA 4.0
14 events
when toggle format | what | by | license | comment | |
---|---|---|---|---|---|
Nov 16, 2023 at 10:12 | comment | added | Mikhail Katz | "Then you have to accept that 'what statements can be proven from the Peano axioms' is itself indefinite. Because the length of a valid proof in PA is a natural number, so if we don't know what the natural numbers are then we don't know what are the possible lengths of proofs. There could be 'proofs in PA' which are valid on one version of N but not on another." This seems incorrect. The length of an actual proof in PA is not an object-language natural number. It is a metalanguage natural number. These can be thought of as corresponding to a sorites-like subcollection of $\mathbb N$. | |
Jan 14, 2022 at 8:17 | comment | added | user76284 | @TommyR.Jensen Encodings are not intrinsic to the numerals themselves. | |
Sep 22, 2019 at 21:36 | comment | added | Tommy R. Jensen | We absolutely cannot have a more clear conception of $\mathbb{N}$ than of $10^{100}$. After all, some single element of $\mathbb{N}$ allows for an encoding of the entire bible. It probably even exists in some editor's desktop. | |
May 29, 2019 at 11:27 | comment | added | user44143 | @NikWeaver, I think the aliens from the first-order land of $PA+\neg Con(PA)$ say to us "you've agreed to accept arbitrarily long proofs, so you must accept this proof which you call non-standardly long; you have not articulated any criterion of length by which to reject it." In any case, I like this version of the question; "do you accept a non-standardly long proof of $0=1$?" feels much sharper than "do you accept non-standard numbers?" | |
May 27, 2019 at 18:46 | comment | added | Nik Weaver | @AndreasBlass: what makes me uncomfortable is the idea that one can "intuitively" understand something but not be able to express that understanding through language. Maybe there's no problem here, but I'm not sure there's no problem. | |
May 27, 2019 at 17:45 | comment | added | Andreas Blass | When I read the question "if axioms cannot capture the 'intuitive notion of a natural number', what possibly could?" I thought that the question contains its own answer: intuition. (Of course, there may be a question about what "capture" should mean here.) | |
May 27, 2019 at 17:41 | comment | added | Andreas Blass | Your observation (item 2) that people accept the definiteness of $\mathbb N$ until they see the incompleteness theorems is probably correct, but they could reasonably entertain doubts just on the basis of the upward Löwenheim-Skolem-Tarski theorem. That theorem won't cause doubts about the (first-order) theory of $\mathbb N$, but it can cause doubts about $\mathbb N$ itself. | |
May 26, 2019 at 4:32 | comment | added | user76284 | Point 4 is obvious in retrospect, given the second incompleteness theorem, but I hadn't quite looked at it that way. And it applies not just to PA but to any reasonably powerful theory T. Thus it seems to really drive home the limitations of the axiomatic method. | |
May 24, 2019 at 11:13 | comment | added | Nik Weaver | @Matt F: in a model for PA + $\neg$ Con(PA) there exists a non-standard number which is the Godel number of a proof of $0=1$. So there is a proof of $0=1$ of nonstandard length. | |
May 24, 2019 at 10:35 | comment | added | user44143 | I’m not worried about proofs of non-standard length if there are shorter proofs of standard length. Can someone here show that this always holds, by cut elimination? | |
May 23, 2019 at 18:43 | comment | added | Nik Weaver | Could we be sure that the supertask machines are really getting the natural numbers? Well, if we ask a question that we know the answer to and they give us the wrong answer, or if two of their answers contradict each other, then we know something is wrong. If it repeatedly passes tests of this sort then we can gain confidence but we will never "be sure" it's right. You could say the same thing about computers as they exist today. How can you be sure any massive computation is correct? | |
May 23, 2019 at 18:40 | comment | added | Nik Weaver | Could you elaborate on "our conception of consistency is not reflected in reality"? | |
May 23, 2019 at 16:34 | comment | added | Pace Nielsen | I appreciate these ideas. For beings with access to an oracle of a model where Con(PA) is false, they would argue (presumably) that our conception of consistency is not reflected in reality. So to them, #4 might be question-begging. To them, #3 is moot because $\mathbb{N}$ is not captured by the axioms, but is captured by their machines. But even assuming their machines did say that Con(PA) is true (and Con(PA+Con(PA)), and so on as far as we tested) could we be sure that the supertask machines are really getting the natural numbers? I'd argue no. | |
May 23, 2019 at 5:26 | history | answered | Nik Weaver | CC BY-SA 4.0 |