Timeline for Situation with Artemov's paper?
Current License: CC BY-SA 4.0
16 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 25 at 20:08 | comment | added | Sergei Artemov | @NoahSchweber. Foundations are full of ill-defined notions, and we have to deal with this fact: finitistic methods (Hilbert), the so-called 24th Hilbert Problem, etc. There has not been a formal criterion of the right consistency formalization (cf. Rosser's consistency and others), and logicians have lived in this situation for decades. There is no criterion for what formal proof of a not-yet-formalized property is. The consistency proofs are in this category: you know it when you see it. However, the core examples may be convincing despite the absence of a complete umbrella formalization. | |
| Jul 23 at 21:41 | comment | added | Noah Schweber | Ultimately I'm not interested in results about/in ill-defined systems, so I'm trying to pin down how your results can be made formal (or if you prefer, "symbolic"). That's my specific question: can you phrase "$PA$ can selector-prove (or whatever) its own consistency but $\mathsf{I\Sigma_1}$ cannot" in a computer-understandable way? | |
| Jul 23 at 21:37 | comment | added | Noah Schweber | @SergeiArtemov "Generally, people find elementary arithmetic easier to accept than ZFC." This conflates accepts as true (or consistent or similar) with understands precisely what it means. ZFC is less likely to be true(/etc.), but is vastly more precisely defined (read: is actually precisely defined) than $\widehat{\mathsf{PA}}$ = elementary number theory. | |
| Jul 23 at 20:59 | comment | added | Sergei Artemov | This is quite unusual. Generally, people find elementary arithmetic easier to accept than ZFC. An old and useful advice is to try to work with it, and then you'll get used to it. Please focus on the points you understand and do not try to grasp them all simultaneously. Having some study groups helps, especially if you are the instructor. I will be glad to answer specific questions. | |
| Jul 23 at 20:17 | comment | added | Noah Schweber | E.g. my doppelganger in the previous comment has no trouble interpreting (say) Martin's proof of Borel determinacy in ZFC; he just says "OK, you have (made a compelling argument that there is) a formal derivation in ZFC of (the formalization of) Borel determinacy." My doppelganger suspects that this result will eventually be trivialized (by the realization that ZFC is in fact inconsistent), but doesn't doubt that a deduction has been produced (modulo formalization details :P). But I don't see how to similarly interpret anything that refers to $\widehat{PA}$. | |
| Jul 23 at 20:14 | comment | added | Noah Schweber | @SergeiArtemov OK, so suppose I didn't accept all of elementary number theory, and in particular were already suspicious about the formal consistency of $\mathsf{I\Sigma_2}$. How should I interpret your results? (In fact I'm not so skeptical, but I am extremely suspicious of hard-to-remove informalities.) | |
| Jul 23 at 20:12 | comment | added | Sergei Artemov | $\widehat{PA}$ is what mathematicians call "elementary number theory," i.e., informal but rigorous reasoning based on FO logic, recursive definitions of p.r. operations, and the simple induction principle. I believe advanced high school kids (e.g., my Californian granddaughters) have a good grasp of it. $\widehat{PA}$ is related to $\textsf{PA}$ by the formalization principle (similar to the Church Thesis) that any rigorous reasoning in $\widehat{PA}$ can be internalized as a derivation in $\textsf{PA}$. | |
| Jul 23 at 19:51 | comment | added | Noah Schweber | @SergeiArtemov OK. I suspect then that you do agree with my claims (i) and (ii) from a couple comments prior, but would say that that $f$ (+ its attendant data) is merely a $T$-"proof of the scheme" rather than a "selector proof in $\widehat{T}$" or similar. If that's right, my next question is: what exactly is $\widehat{PA}$? | |
| Jul 23 at 19:21 | comment | added | Sergei Artemov | I am using "formalized" to represent "internalized," i.e., represented by a completely formal arithmetical object, like a formula or a term. I sense that your use of "formalized" is close to what I call "rigorous" with existing standards of mathematical rigor. This is a general observation. Shall we try to answer specific questions? | |
| Jul 23 at 18:44 | comment | added | Noah Schweber | @SergeiArtemov I have read section 5.2 (and skimmed the whole text); my questions stand. I am rather confused by the extent to which informal reasoning is leaned on. E.g. is "formalized selector proof" an informal notion? | |
| Jul 23 at 18:42 | comment | added | Sergei Artemov | May I humbly ask you to read section 5.2 of my 2024 arxiv preprint arxiv.org/abs/2403.12272v1 and, better yet, the whole text (about 20 pages of easy reading)? If you still have these questions standing, I will be more than happy to elaborate. In the informal arithmetic 𝑃𝐴ˆ, there are some properties of reasonings - simple, natural, similar, etc. - which are not yet formalized and are used on a case-by-case basis. The notion of "proof of consistency" is one of them, and we have to apply our informal math judgments. | |
| Jul 23 at 18:25 | comment | added | Noah Schweber | (Maybe it will help to assume that I'm an extreme formalist, and moreover am dubious even of the consistency of $\mathsf{I\Sigma_2}$ or similar. Of course I'm not, but I think that will help clarify the definitions here.) | |
| Jul 23 at 18:24 | comment | added | Noah Schweber | @SergeiArtemov At this point I'm confused by your notion of $\widehat{PA}$ (and "contentual counterparts" in general - I don't find reference to "mathematical proof" any more clarifying). The only thing I am confident of right now is that for every c.e. theory $T$ extending $\mathsf{I\Sigma_1}$, there is a p.r. function $f$ such that $(i)$ for each $n$, $f(n)$ is a $T$-proof of "$n$ is not a $T$-proof of $\perp$" and $(ii)$ $T$ proves that fact $(i)$. So my first question is: do you agree with my claims (i) and (ii)? My second question is: if so, what exactly is $\widehat{PA}$? | |
| Jul 23 at 2:47 | comment | added | Sergei Artemov | Your repeated example of a "simple consistency proof" above has been covered in section 5.2 of Artemov, Sergei. Serial Properties, Selector Proofs, and the Provability of Consistency. arxiv.org/abs/2403.12272v1. A consistency proof in PA is (1) a mathematical proof of consistency, which is (2) formalizable in PA. What you offer does not respect (1) since it is not proof of consistency (but something else); see the arxiv preprint. | |
| Apr 17 at 23:22 | comment | added | Peter LeFanu Lumsdaine | This is a nice analysis of Artemov’s sense of “proving” a schema. One thing I think usefully clarifies it further is to differentiate the outer and inner theories — to a notion one might notate as say $T_1 \vdash^{T_0} \varphi(x)$, to mean that there’s a p.r. function $f$ such that $T_0$ (the meta-theory) proves “$f$ provides proofs in $T_1$ (the object theory) of $\varphi(n)$, for each $n$”. This in particular helps see that with the meta-theory $T_0$ fixed, the statement proven in $T_0$ cannot reasonably be read as “$T_1$ is consistent”, since it holds trivially for inconsistent $T_1$. | |
| Apr 17 at 21:07 | history | answered | Noah Schweber | CC BY-SA 4.0 |