Timeline for Proving that ZF is Artemov-consistent
Current License: CC BY-SA 4.0
33 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 11 at 21:20 | history | edited | Timothy Chow | CC BY-SA 4.0 |
Added a remark to explain that there is another MO question that is close to a duplicate
|
| Aug 2 at 3:17 | comment | added | Pace Nielsen | Let us continue this discussion in chat. | |
| Aug 1 at 23:00 | comment | added | Sergei Artemov | @PaceNielsen. "ii) expand your meta-notion of "prove" to accept serial proofs as a valid means of meta-verification" - this is the option I am suggesting in the JLC_2024 paper. Selector proofs are embedded into mathematical practice: induction principle, product of polynomials, tautologies. Here is a quote: "If we don’t accept selector proofs, we have to admit that such basic mathematical facts as induction, propositional tautologies, product of polynomials, etc., are not provable in arithmetic. Moreover, that consistency is unprovable for the same reason: selector proofs are not included." | |
| Aug 1 at 21:55 | comment | added | Sergei Artemov | @PaceNielsen. "PA+Con(PA) in your metatheory" - I do not use PA+Con(PA) in my metatheory. Using sets of formulas in metatheory is common practice: cf. the textbook deduction theorem: "for a given set of formulas $\Gamma$, ... ." My metatheory is standard for PA. We only need numeral quantifiers "for any numeral n..." to transit from "PA is consistent," which, modulo to Goedel numbering, uses numeral quantifiers to its faithful PA form. Picking Con(PA) as "PA is consistent" was a hack job: we naively replaced numeral quantifiers with PA quantifiers. So, we must work with Con^S(PA). | |
| Aug 1 at 16:39 | history | reopened |
Sam Sanders Pace Nielsen Joel David Hamkins lo.logic Users with the lo.logic badge or a synonym can single-handedly close lo.logic questions as duplicates and reopen them as needed. |
||
| Aug 1 at 15:30 | comment | added | Pace Nielsen | @SergeiArtemov Thanks for the clarifications! Accepting that selector proofs are a native PA tool, then they only "prove serial properties" when you either (i) expand your sense of formal derivation (as Noah did) or (ii) expand your meta-notion of "prove" to accept serial proofs as a valid means of meta-verification. Sure, this can be like a feature in your car that you never used before. But so is using PA+Con(PA) in your metatheory, which runs counter to not assuming PA is consistent to begin with. (BTW, writing {F(0),F(1),...} starts introducing second order logic into metatheory.) | |
| Aug 1 at 14:10 | review | Reopen votes | |||
| Aug 1 at 16:41 | |||||
| Jul 31 at 23:20 | comment | added | Sergei Artemov | "But we have assumed stronger (non-PA) metatheoretical tools (by allowing selector proofs)." Selector proofs are not metatheoretical tools; they are native PA tools that prove serial properties that are totally consistent with all other PA tools. This is like you have never used reverse in your car, but this feature has always been available. Somebody brings this to your attention, and you begin using the reverse in the same old car. | |
| Jul 31 at 23:00 | comment | added | Sergei Artemov | "We can encode "PA is consistent" as the arithmetic sentence Con(PA)." This also requires reasoning in a metatheory with numeral quantifiers but with a dubious and false assumption that PA-quantifiers are equivalent to numeral quantifiers. You have to assume that "for all numerals n, F(n)" is not logically equivalent to the set of sentences {F(0), F(1), F(2), ...}. This is why I strongly prefer Con^S(PA) to Con(PA). The tension between "PA is consistent" and Con(PA) is that the former uses numeric quantifiers (or their equivalents) whereas Con(PA) uses non-equivalent PA-quantifiers. | |
| Jul 31 at 22:58 | comment | added | Sergei Artemov | @PaceNielsen. Your analysis is pretty good, but some principal comments/suggestions can be made, with your kind permission. "There is a metamathematical statement Z that is equivalent to the metamathematical statement "PA is consistent", but the proof of that equivalence uses the idea of selector proofs." No it does not, just a logic reasoning in some metatheory with quantifiers over numerals (hence extending PA). It boils down to accepting that "for all numerals n, F(n)" is logically equivalent to the set of sentences {F(0), F(1), F(2), ...}. This is more basic than selector proofs. | |
| Jul 31 at 21:01 | comment | added | Sergei Artemov | @PaceNielsen. PA proves a formula $F$ has been rigorous, and PA proves a serial property ${F}$ is equally rigorous. "PA proves the consistency of PA" has not been rigorous in the old von Neumann sense because it relies on a specific formalization of PA consistency (as Con(PA), as Rosser Con(PA), etc). "PA selector proves the consistency of PA" is equally not rigorous for similar reasons. Proving consistency is easier since it suffices to come up with one convincing case, whereas proving unprovability is impossible because of this lack of rigor in the definitions. Such is life. | |
| Jul 31 at 18:30 | comment | added | Sergei Artemov | @PaceNielsen. I will reply with corrections, but I'm too busy with other replies. | |
| Jul 31 at 17:36 | comment | added | Pace Nielsen | We have not affected what PA proves or does not prove. We have not changed formal entailment. But we have assumed stronger (non-PA) metatheoretic tools (by allowing selector proofs). Thus, in Artemov's abstract, when he writes "PA proves its own consistency", I believe this means "PA proves a statement that is equivalent (under a stronger theory than PA, but weak in some relevant ways) to consistency". | |
| Jul 31 at 17:36 | comment | added | Pace Nielsen | @AlexKruckman I think the problem is as follows. (Sergei, feel free to correct me if I get something wrong.) There is a metamathematical statement Z that is equivalent to the metamathematical statement "PA is consistent", but the proof of that equivalence uses the idea of selector proofs. This equivalence is not provable in PA, only in a strictly stronger metatheory. We can encode "PA is consistent" as the arithmetic sentence Con(PA), which PA does not prove. We can encode Z as Con^S(PA), which PA does prove. (continued...) | |
| Jul 31 at 17:02 | comment | added | Sergei Artemov | @AlexKruckman. I see this unfortunate misconception still alive despite my short clarifying replies on MO and precise formulations and examples in the paper. I need to craft a real-size comment to Noah Schweber's attempted exposition of my construction. More time is needed for this. I hope to do this today. | |
| Jul 31 at 16:40 | comment | added | Sergei Artemov | @PaceNielsen. A perfect question. Thank you. In fact, selector proofs do not extend the proving power of PA w.r.t. formulas, it remains the same good old PA. Specifically, Proposition 5.3.ii in the JLC_2024 paper (Proposition 2(ii) in the arXiv preprint) states that whenever a serial property is (selector) provable in PA, each of its instances is provable as a formula. The proof is constructive and formalizable in PA. So, no special new consistency proof is needed: since PA does not prove 0=1, none of the provable serial properties contains 0=1 as its member. | |
| Jul 31 at 16:02 | comment | added | Alex Kruckman | @SergeiArtemov What precisely is Noah Schweber's misunderstanding in his answer here? Noah's answer actually corrects a misunderstanding of your paper that originated in a different answer to the question. I have read your paper, Noah's answer, and the many comments below it, and I still don't see anything wrong with Noah's answer. | |
| Jul 31 at 6:01 | comment | added | Pace Nielsen | @SergeiArtemov If we allow selector proofs as an additional tool in our toolkit, then doesn't Con^S(PA) fail to capture consistency because it fails to capture that selector proofs provide a possible additional avenue to a contradiction? | |
| Jul 30 at 22:24 | comment | added | Sergei Artemov | @PaceNielsen. Noah Schweber's first analysis of my version of "entailment" has been based of misunderstanding. So, I am not responsible for what you call $P\! A ^\ast$, let alone for proving Con$(P\! A ^\ast)$ in $P\! A ^\ast$. Proving consistency is a delicate matter, and suggesting themselves simplifications do not necessarily work. I would advise reading the corresponding JLC_2024 paper. | |
| Jul 30 at 22:23 | comment | added | Sergei Artemov | @Joel David Hamkins. Well, perhaps elevating the coding theory to the almighty ZF could indeed work for different reasons. However, this still smells like begging the question since the ZF selector proves ZF. Anyway, thank you for the cute observation that the power of the coding theory can compensate for other weaknesses. | |
| Jul 30 at 20:54 | comment | added | Joel David Hamkins | @SergeiArtemov But it does work, if I understand things correctly, if in that case we take $v:$ as the ZF proof predicate, right? This is what I had meant by having ZF in the meta theory. That is, ZF proves of every numeral $n$ that PA proves of it that it is not the proof of a contradiction in ZF. Those are the three instances of proof predicates, in this natural language way of saying it, right? | |
| Jul 30 at 20:36 | comment | added | Sergei Artemov | @Joel David Hamkins. When formalized, a selector consistency proof has three occurrences of proof predicates ":," $v:s(x):\neg x:\bot$ where $s(x)$ is a selector, v is a verifier, and $\neg x:\bot$ comes from the object theory. For ZF consistency in ZF, both $\neg x:\bot$ and $s(x):$ should be ZF proof predicates, whereas $v:$ is just a coding bookkeeping, usually performed by PA or its appropriate fragment. In this sense, we both agree that ZF proves its consistency. When we try to formalize the claim that PA proves ZF, then $s(x):$ should be the PA proof predicate, which does not work. | |
| Jul 29 at 18:07 | history | closed |
Christopher King CommunityBot |
Duplicate of Does PA prove (Artemov-style) the consistency of a stronger system? | |
| Jul 29 at 18:06 | comment | added | Timothy Chow | @ChristopherKing I forgot about that question. But in that question, there was a misreading of Artemov's definition. Still, I would be okay with closing the current question as a duplicate. I wouldn't want to delete the current question, though, since it elicited a response from Artemov himself. | |
| Jul 29 at 18:01 | comment | added | Christopher King | Essentially a duplicate of Does PA prove (Artemov-style) the consistency of a stronger system? I think? | |
| Jul 28 at 2:28 | comment | added | Joel David Hamkins | I had thought I was claiming more, namely, that ZF proves that PA proves the consistency (in your sense) of ZF. Specifically, ZF proves of every metatheoretic numeral $n$ that PA proves that it is not the proof of a contradiction in ZF. Perhaps I've misunderstood, but I had thought you were claiming that PA doesn't prove these things? I am unsure whether I am allowed to assume ZF in the metatheory when discussing these issues about what PA proves or not. If I do have ZF in the metatheory, then isn't it correct that PA prove the consistency of ZF in your sense? Or is this a misunderstanding? | |
| Jul 28 at 0:00 | comment | added | Sergei Artemov | @Joel David Hamkins. This is correct: ZF selector proves its consistency; see my JLC paper. | |
| Jul 27 at 18:38 | answer | added | Sergei Artemov | timeline score: 3 | |
| Jul 27 at 17:33 | comment | added | Joel David Hamkins | So it seems that if we have ZF as the meta theory, then we can prove that PA proves ZF is Artemov consistent, based on the observation of my comment. | |
| Jul 27 at 17:29 | comment | added | Noah Schweber | I recommend looking at the comment thread below my answer to the linked question; at least one of the relevant "proof" notions does not in fact (according to Artemov) have a formal definition. | |
| Jul 27 at 17:21 | comment | added | Joel David Hamkins | If ZF is actually consistent, then PA proves of each standard $n$ that it is not the proof of a contradiction in ZF. And since ZF proves of each of its finite fragments that that fragment is consistent, what we have is that ZF proves, of every particular $n$, that PA proves that it is not the proof of a contradiction in ZF. Can you say what more would be required for Artemov consistency? | |
| Jul 27 at 17:11 | history | edited | Timothy Chow | CC BY-SA 4.0 |
added 9 characters in body
|
| Jul 27 at 17:00 | history | asked | Timothy Chow | CC BY-SA 4.0 |