Timeline for Proving that ZF is Artemov-consistent
Current License: CC BY-SA 4.0
32 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 1 at 16:33 | comment | added | Christopher King | FYI: here is another post arguing that G2 doesn't stop Hilbert's program (with a fairly different argument): Completing half of Hilbert's program: Foundations that are conservative over Peano Arithmetic | |
| Aug 1 at 16:31 | history | edited | Christopher King | CC BY-SA 4.0 |
added 7 characters in body
|
| Jul 29 at 20:02 | comment | added | Sergei Artemov | @ChristopherKing. This "answer" is irrelevant to my proof; Emil Jerabek himself admitted it in the comments. Loosely, Jerabek's argument is a constructive version of the consistency proof "via the standard model" considered as an example to avoid in my JLC_2024 paper (and in the 2024 arXiv preprint). Jerabek's argument uses the assumption that PA is consistent (hence $\neg n:\bot$ is true) and refers to the classical result that any true p.r. sentence is provable in PA. I am proving the consistency of PA without assuming its consistency. | |
| Jul 29 at 18:18 | comment | added | Sergei Artemov | @TimothyChow. A short answer is "F(n) is both a formal string and a metatheoretic assertion." To keep things simple, consider the following case: F(x) is a primitive recursive formula in the language of PA with p.r. terms. Then F(n) is an instance of a p.r. the formula, which makes sense as a meta-theoretic assertion, as well as for PA. Whereas F(n) is a legal sentence, the object {F(0), F(1), F(2), ... } not necessarily should be viewed as a "sentence." It is a series of sentences, normal in metamathematics, cf. the deduction theorem $\Gamma, A \vdash B$ iff $\Gamma \vdash A\rightarrow B$. | |
| Jul 29 at 18:11 | comment | added | Christopher King | @SergeiArtemov is there anything wrong with this answer? | |
| Jul 29 at 8:07 | comment | added | David Roberts♦ | @all - please note that the software has flagged this post for a large number of comments. It might be worth taking this discussion elsewhere to resolve, if it's not going to wrap up soon, and then report back if and when there is a resolution. | |
| Jul 28 at 23:02 | comment | added | Timothy Chow | @SergeiArtemov When you say "for all numerals n, F(n)", I take it that "for all numerals" is a metatheoretic phrase, but is F(n) a formal string, or a metatheoretic assertion? If it's a formal string, then "for all numerals n, F(n)" does not make any sense. If it's a metatheoretic assertion, then F(0), F(1), F(2), ... doesn't make sense because for any normal metatheory, infinitely long sentences are not allowed. | |
| Jul 28 at 17:33 | comment | added | Sergei Artemov | @AlexKruckman. As for objections (there were some, not many), they were of the sort “I don’t like it at all,” “We don’t do it this way,” “I don’t understand the informal part,” etc ., expressed before reading the final text of the article. Such comments sound like a priori rejections rather than objections. So, no reasonable objections expressed so far “at all.” I hoped that you had something specific to discuss … . | |
| Jul 28 at 14:33 | comment | added | Sergei Artemov | @AlexKruckman. Foundational work often requires a responsible formalization part, which makes rigorous but informal notions completely formal, followed by the usual symbol grinding. Think of Goedel's (First) incompleteness theorem, which is widely accepted as the top mathematical result. Let me know when you will be open to this sort of discussion; no pressure. | |
| Jul 28 at 14:17 | comment | added | Sergei Artemov | @MonroeEskew. Thank you for this question. I believe this paper outlines a proof theory of serial properties (and applies it to prove PA consistency in PA, with foundational implications). | |
| Jul 28 at 13:42 | comment | added | Alex Kruckman | I did not intend to engage in a discussion here of the question of what is the appropriate formalization of "PA is consistent" in PA - the comment section below your answer to an entirely different question is neither a convenient nor appropriate place to have such a discussion. I merely objected to the framing of your argument as a mathematical proof of the non-equivalence. | |
| Jul 28 at 10:19 | comment | added | Monroe Eskew | What is the key mathematical innovation in your work? | |
| Jul 28 at 6:05 | comment | added | Sergei Artemov | @PaceNielsen. PA quantifiers coincide with numeral quantifiers in the standard model. This does not make all quantifications in PA suspects. For most of the questions, PA quantifiers provide a good approximation to numeral quantifiers: we prove Fermat’s Little Theorem in PA and claim that it is true in the standard model. However, if a sentence is independent in PA, like Con(PA), we have to resort to special tricks to emulate numeral quantifiers faithfully. BTW, "0 is not a code of a PA-derivation containing the line 0=1” is quantifier-free in PA (with p.r. terms) and hence is immune. | |
| Jul 28 at 5:40 | comment | added | Sergei Artemov | @AlexKruckman. You are the first person who tried to be specific about your objections to my argument that Con(PA) is stronger than PA-consistency. I hoped for a meaningful discussion about mathematics, details of formalization, stability under Goedel numerations, etc. I feel disappointed: your “formalization is a philosophical question” is a step to bail out of a discussion, sorry. If you are ready to talk seriously, please answer my specific question: whether “for all numerals n, F(n)” and “F(0), F(1), F(2), … ” are equivalent or not. | |
| Jul 28 at 4:21 | comment | added | Pace Nielsen | I don't understand the phrase "quantification over numerals is not expressible in PA". I mean, it is technically true that the symbols $\forall x$ are just that, symbols. But once they are interpreted in a model, where the domain of that model is the set of numerals, than those symbols are truly interpreted as quantification over numerals. Moreover, even if we grant (3), then all quantifications in PA are suspect, including the (many!) quantifications in "0 is not a code of a PA-derivation containing the line 0=1" as well as in the induction axiom of PA. | |
| Jul 28 at 4:03 | comment | added | Alex Kruckman | So we're left with the question of the proper formalization of "PA is consistent" which is a philosophical question, not a mathematical one. That's my objection. As for where I stand on the philosophical question: I'm hardly the first person to express disagreement here! As I said, I think your argument has merits and is worthy of discussion (that's why I'm here), but I think that Timothy Chow and Noah Schweber have written coherent and convincing objections. | |
| Jul 28 at 3:57 | comment | added | Alex Kruckman | @SergeiArtemov I thought my comment above and the linked comment made my objection clear, but I'll try again. You claim to make a mathematical argument regarding the equivalence (or not) of Con(PA) and "PA is consistent". That's nonsense, of course, because these two concepts live at different levels: Con(PA) is formal, while "PA is consistent" Is informal. So we must first decide how to formalize "PA is consistent". But once we decide how to formalize "PA is consistent", the mathematical question of equivalence (or not) trivializes. (Continued in next comment) | |
| Jul 28 at 3:20 | history | edited | Sergei Artemov | CC BY-SA 4.0 |
added 497 characters in body
|
| Jul 28 at 2:43 | comment | added | Sergei Artemov | @AlexKruckman. Since you are the first person who expressed disagreement with a specific step of my (well-advertised ) argument 1-4 that Con(PA) is stronger than PA consistency, I am truly interested. I see, you disagree with (3), which converts “for all numerals n, F(n)” for a specific p.r. formula F(x) to “F(0), F(1), F(2), … .” I see them as equivalent without invoking any meta-assumptions about PA. Direction => is obvious. Direction <=: suppose for some numeral m, F(m) does not hold. Then the m-th element in the string “F(0), F(1), F(2), … ” is false. What exactly bothers you here? | |
| Jul 28 at 0:44 | comment | added | Noah Schweber | that such informality is only appropriate when it is clear what formal strings are "had in mind" so to speak. This is a principle I apply completely uniformly, and is what motivated my questions to you in the first place. | |
| Jul 28 at 0:41 | comment | added | Noah Schweber | @SergeiArtemov I do extend exactly the same demand for precision: in any context where I am not certain that I and my interlocutors all understand "PA is consistent" as being shorthand for the same string of symbols, I check that (i) they do in fact have a formal counterpart in mind and (ii) it's the same as mine before continuing on the topic. Admittedly, this doesn't come up very often. But this is what I view as the appropriate role of informal language in mathematical claims and arguments (as opposed to discussion of their import/motivation of course): | |
| Jul 28 at 0:22 | comment | added | Sergei Artemov | @NoahSchweber. Everybody is entitled to have his/her own (mis)understanding. The only thing I expect is to apply them fairly, not selectively. I can live with your understanding Goedel's Second theorem, but not understanding the Unprovability of Consistency thesis (PA cannot prove its consistency) as not formal enough for you. | |
| Jul 28 at 0:16 | comment | added | Noah Schweber | Whether or not one accepts the statement "$Con(PA)$ is an adequate formalization of 'PA is consistent,'" one can accept the purely formal statement "$[PA\not\vdash\perp]\implies [PA\not\vdash Con(PA)]$." That's what I'm looking for in your claims: a purely formal statement which, independently of whether I accept your philosophical stance, I can recognize as true. That is what I don't see so far as soon as "selector proofs" enter the picture, and I think this is a serious problem. I truly do not understand your claim that these exhibit the same degree/role of informality. But I'll bow out. | |
| Jul 28 at 0:12 | comment | added | Noah Schweber | @SergeiArtemov I genuinely don't understand how my question can be misleading. The problem with this sort of approach to presenting mathematical claims, and more generally (to quote from a previous comment of yours) the "you know it when you see it" style, is that maybe I don't know-upon-seeing the same things that you do. I think that's the case here. | |
| Jul 27 at 23:56 | history | edited | Sergei Artemov | CC BY-SA 4.0 |
added 1 character in body
|
| Jul 27 at 23:51 | comment | added | Sergei Artemov | @NoahSchweber. Your comment may sound misleading. All known notions of consistency proof contain informal components, e.g., the unprovability of consistency argument uses the informal notion of consistency formalization. My take on the consistency proof follows (as I hope) Hilbert's format that a T-consistency proof in a theory S is (A). A rigorous mathematical proof of T-consistency, and (B). A formalization of (A) in S. (A) is not necessarily formal, and its formalization depends on many previous choices that we cannot foresee. | |
| Jul 27 at 23:47 | comment | added | Sergei Artemov | @AlexKruckman. I strongly disagree. The whole story has a deep mathematical substance: quantifiers over numerals are intrinsically different from PA quantifiers. Do you want to do anything with it, or just ignore this and reduce to buying PA-quantifiers as quantifiers over numerals? If you decide to do something else instead, then what exactly? The scheme Con^S(PA) is equivalent to (*), whereas Con(PA) is not. What do you choose? | |
| Jul 27 at 23:27 | comment | added | Alex Kruckman | I think you have (in your paper on the topic) made an interesting philosophical argument about the proper way to formalize "PA is consistent" in PA. I don't buy it, but I think it's interesting and valuable. What I'm taking issue with is trying to frame this as a mathematical argument | |
| Jul 27 at 23:16 | comment | added | Alex Kruckman | -1 for the "BTW...", which adds nothing relevant to Timothy Chow's question (which grants your nonstandard views on consistency assertions). Your argument begs the question, as I pointed out in an earlier comment. It is only a proof that that Con(PA) is not equivalent to "PA is consistent" over PA if you have already decided to interpret "PA is consistent" in PA as the infinitely many statements "$n$ does not code a PA derivation of $\bot$" for each numeral $n$. | |
| Jul 27 at 21:57 | history | edited | Sergei Artemov | CC BY-SA 4.0 |
added 1469 characters in body
|
| Jul 27 at 18:55 | comment | added | Noah Schweber | I'm still confused about which statements are formal/precise and which ones are informal. When you say "In particular, Kurahashi-Sinclaire’s observation that prohibits PA from proving the consistency scheme for PA+ConPA shows also that PA cannot prove the consistency of ZF" which category is the bolded part? | |
| Jul 27 at 18:38 | history | answered | Sergei Artemov | CC BY-SA 4.0 |