Situation with Artemov's paper?

Question

Artemov's paper on Goedel's theorem has been on the arxiv since 2019. There was a (less than fully friendly) discussion of this on FoM. At stackexchange, I found only a brief mention at this MSE post. Artemov's paper has apparently not yet been published in a refereed venue (which could lead to inferences that I proactively ask the users to avoid).

Could somebody knowledgeable about the material comment on the upshot with this paper, sticking to logic and expert opinion (and avoiding snide remarks)?

I just became aware of an update posted a month ago:

Artemov, Sergei. Serial Properties, Selector Proofs, and the Provability of Consistency. https://arxiv.org/abs/2403.12272v1

Answer 1

The essential issue is the same as one that has been discussed many times here on MO, for example here and here. Consider the following string $S$. $$(\exists x \exists y \exists z : xxx + yyy - zzz = 114) \vee (\exists x \exists y \exists z : xxx - yyy - zzz = 114) \vee (\exists x \exists y \exists z : xxx + yyy + zzz = 114)$$ Let me now make a claim.

Claim. If there is a valid mathematical proof, using only the mathematical assumptions that are formalized by the axioms of PA along with classical logic, that 114 is the sum of three cubes, then there exists a formal PA-proof of $S$.

(EDIT: With hindsight, I probably should have used $\neg S$ rather than $S$ as my example, because $\neg S$ is closer in flavor to Con(PA). The choice between $S$ and $\neg S$ doesn't change the point I'm making, but judging from some of the questions I've received, $\neg S$ would have made for a clearer example.)

The above Claim is not a strictly mathematical claim, because it refers to the informal notion of a "valid mathematical proof," which is not a strictly mathematical entity. By contrast, formal PA-proofs are mathematical entities. In effect, the Claim is asserting that, in a certain important sense, formal PA-proofs "capture" the informal notion of "valid mathematical proof" and $S$ "captures" the assertion that 114 is the sum of three cubes. The Claim is somewhat akin to the Church–Turing thesis, in that it asserts that a pre-existing informal concept is adequately captured by a precise mathematical concept.

I happen to believe the Claim, and so does almost everyone. Indeed, it's hard to see why one would study PA-proofs if one did not believe the Claim. But you are not compelled to believe the Claim. You are free to deny it. In particular, even if someone manages to prove that $S$ is independent of PA, you could still insist that it remains an open question whether "114 is a sum of three cubes" admits a valid mathematical proof using only the mathematical assumptions formalized by the axioms of PA along with classical logic. In effect, you would be claiming that $S$ fails in some way to be an accurate formalization of "114 is the sum of three cubes."

Because the statement that "114 is the sum of three cubes" is so simple, it is hard to imagine someone seriously arguing against the Claim. However, suppose we now replace "114 is the sum of three cubes" with "PA is consistent" and we replace $S$ with the formal string that is typically given the name "Con(PA)." Since Con(PA) is such a complicated string, and consistency is such a notoriously confusing concept, it's now easier to imagine someone denying the analogous Claim, and maintaining that Con(PA) somehow fails to "capture" the consistency of PA in the sense that the Claim asserts. The late philosopher Michael Detlefsen was perhaps the best-known denialist.

Similarly, Artemov is a denialist in this sense. Artemov, of course, does not deny the truth of Gödel's second incompleteness theorem. But Gödel's 2nd theorem tells us only that Con(PA) is formally unprovable in PA. Artemov denies that we can infer that the consistency of PA cannot be proved from the mathematical assumptions that are formalized by the axioms of PA. To defend this contrarian position, Artemov shows that PA can prove some things that seem awfully close to asserting the consistency of PA. I won't go into the details of Artemov's paper, but here is a classical fact: for any finite subset of the axioms of PA (remember that PA contains an axiom schema and hence has infinitely many axioms), PA can prove that that finite set of axioms is consistent. That sure seems close to proving consistency, doesn't it? After all, if there is an inconsistency in PA, only finitely many axioms will be needed to derive that inconsistency. Whichever specific list of finitely many axioms you might single out on suspicion of yielding an inconsistency, PA proves that that particular list of axioms is consistent. Maybe you feel that's close enough to "PA proves its own consistency"? Or if not, maybe the results that Artemov proves will strike you as convincing.

In short, I would say that there's nothing particularly novel about Artemov's results. It has been clear to experts from the very beginning that this type of denialism is a philosophical option you can take, so certainly that's not new. Personally, I don't find Con(PA) to be an inadequate expression of the consistency of PA any more than I find $S$ to be an inadequate expression of "114 is the sum of three cubes," and neither do most people. But your mileage may vary.

Answer 2

Disclaimer: I am not an expert in the proof theory of arithmetic. However, I don’t think one needs to be to assess this paper. It is admirably clear, well-written, and well-referenced, so it’s not onerous to verify that its precise mathematical claims and proofs all seem perfectly correct, and not particularly controversial. However, its main extra-mathematical claim, that these results can be viewed of a proof of consistency of PA, formalisable in PA, seems unconvincing, and its arguments for this claim are not I think particularly novel (though Artemov presents them unusually clearly).

The main precise mathematical claims are (very slightly paraphrased):

1. for each $n$, PA proves the statement “$n$ does not code a proof of $\bot$ in PA” (which we abbreviate as “$\lnot (n \colon \bot)$”);
2. moreover, this is witnessed by a primitive recursive function taking each $n$ to the proof of “$\lnot (n \colon \bot)$”;
3. these two facts can themselves be proven in PA.

The first two facts are fairly straightforwardly provable using standard techniques from the proof theory of arithmetic, in several ways (Artemov uses truth-definitions for $\Sigma_n$ formulas); and the fact that PA is a sufficient metatheory for them (indeed, small fragments such as PRA suffice) is also standard, as discussed in e.g. the answers of this old MO question. There is nothing controversial or questionable about any of this.

The tenuous step is when Artemov argues that this can be seen a proof of consistency of PA, within PA. The stretch becomes clear when we carefully break the claim down to definitions. “PA is consistent” means “there is no proof of contradiction in PA”, i.e. “there is no $n$ which codes a proof of $\bot$ in PA”, or equivalently “for each $n$, $n$ does not code a PA-proof of $\bot$”. So just taking things to mean what they’re defined to, a proof of “PA is consistent” in PA should be a proof of “for all $n$, $\lnot (n \colon \bot)$” in PA.

Artemov argues that since for each $n$ we can prove “$\lnot (n \colon \bot)$” in PA, and we can prove that schematic-provability using PA as metatheory, we can view this overall as a proof of the consistency of PA in PA. But note that the quantifier “for each $n$” has been moved to between provability claim. So we have proved in the inner-PA a schema of statements, and then in the outer-PA, we can assert the provability of that schema as a single statement. But we have not presented a proof in either copy of PA of a single statement that can be read as “PA is consistent”. In the inner PA, we have proven a schema of statments about specific finite derivations in PA. In the outer PA, we’ve proven a fact about PA which certainly can’t be read as “PA is consistent”, since we could prove the same schema for an inconsistent theory of arithmetic. Artemov’s argument that this can be called a proof in PA of consistency of PA reminds me of an old joke: “If you call a dog’s tail a leg, how many legs does a dog have?” “Four — calling the tail a leg doesn’t mean it is one.”

The parametric proof of this scheme certainly shows that PA comes very close to proving its own consistency. A similar argument for ZF can be given by for instance the reflection theorem — that for any finite list of axioms of ZF, ZF proves there’s some $V_\alpha$ which models them (and hence that they’re consistent). Most textbook presentations of these reflection principles that I’ve seen discuss this point explicitly — they note that these results bring the theory very close to proving its own consistency, but on close inspection, don’t quite prove it.

A piece of background worth noting here (a point which iirc I learned from Timothy Chow on this site) is that Hilbert’s consistency programme was not just to prove consistency of arithmetic within arithmetic — that would prima facie be a rather weak result, since an inconsistent theory would still prove its own consistency. Hilbert’s hope was to prove the consistency of some kind of set theory from some theory of arithmetic — justifying a more abstract theory by means of a more self-evident one, which would be a genuinely valuable result. The point of Gödel’s theorem was showing that not even the much weaker result was attainable — let alone the stronger result Hilbert had hoped for. So while reflection-principle arguments show that PA and ZF come tantalisingly close to proving their own consistency — close enough that a little good rhetoric can stretch tenuously across the gap — they don’t come at all so close to Hilbert’s actual dream, of proving consistency of set theory from arithmetic; and by Gödel they can’t, since finite fragments of set theory suffice to prove consistency of PA.

Answer 3

I'm primarily giving this answer to prevent a technical misconception from spreading further:

Artemov's notion of entailment, which I'll call "$\vdash_A$" here, is a bit more subtle than it may first appear. In order to say $T\vdash_A\varphi(x)$ (I'm adopting something between my preferred and Artemov's notation here), we need two things:

• A primitive recursive function $p$ such that for each $n$, $p(n)$ is a (code for a) $T$-proof that $\varphi(n)$ holds.

• A $T$-proof $\pi$ of the previous bulletpoint.

There are a couple natural ways we could weaken this - in particular, replace "p.r." with "$T$-provably total" or drop the requirement on $\pi$ - but either choice significantly alters the resulting notion. See in particular my vs. Emil Jerabek's answers at a recent question: if we drop the second bulletpoint then $\vdash_A$ for $\Pi^0_1$ consequents is just truth due to $\Sigma_1$-completeness, but if we keep it we wind up with $$\mathsf{PA}+Con(\mathsf{PA})\vdash Con(T)\quad\iff\quad \mathsf{PA}\vdash_A\chi_T(x)$$ (where $\chi_T$ is defined below).

Foundational concerns aside - and I personally am unconvinced by Artemov's arguments here - the precise definition of $\vdash_A$ he uses is carefully chosen and is not trivial.

That said ...

For $T$ "appropriate" let $\chi_T(x)$ be the (standardly-arithmetized) formula "$x$ is not a (code for a) proof of $\perp$ in $T$." Artemov's argument for $$\mathsf{PA}\vdash_A\chi_{\mathsf{PA}}(x)$$ uses a nontrivial fact about $\mathsf{PA}$, namely that it proves the consistency of each of its finite fragments. But this is completely unnecessary to the point of being misleading: in fact, any $T$ extending $\mathsf{I\Sigma_1}$ has the analogous property $$T\vdash_A\chi_T(x).$$ The argument for this is quite simple:

• On input $n$, first check whether $n$ is in fact a code for a $T$-proof of $\perp$.

• If it is not, output the code $m$ for the verification of this.

• If it is, we can find a slightly-longer $T$-proof of $\chi(n)$ by combining the proof coded by $n$ with ex falso. In this case we output the code $m'$ of that proof.

Since $\Delta_0$ facts can $\mathsf{I\Sigma_1}$-provably be checked "quickly," the above can be bundled together into an appropriate $(p,\pi)$-pair, and at no point have we used any reflection-type assumption on $T$.

Now I suspect that Artemov would at this point object as follows (quoting from page 7 of his above-linked paper, emphasis mine):

This is a rigorous contentual proof of the consistency of PA. Constructions and required properties used in this argument are formalizable in PA: partial truth definitions, compliance of truth definitions with PA-derivation rules, etc.

I suspect that Artemov would - correctly, in my opinion - claim that my argument above is non-contentual (due to the garbageness of the possible "second-case" proofs) but the reflection-based argument has real content. But I don't think this actually helps: we're still left with a situation where a new formal definition ($\vdash_A$) intended to capture some piece of mathematical intuition behaves trivially in a wide class of cases of interest. To me this is pretty fatal.

Of course this is not to say that $\vdash_A$ is not mathematically interesting or that Artemov's claims are technically false; I don't think either is the case. But I do think that the use of a higher-powered and less-broadly-applicable argument here makes $\vdash_A$ appear more significant than warranted.

Answer 4

I appreciate your interest in this work. The paper Serial properties, selector proofs and the provability of consistency passed a rigorous refereeing and has been accepted to JLC. I have just approved the proofs, and the paper will appear on the JLC website shortly. I promised not to publish the full text before that (though I am open to answering questions about Arxiv preprints).

July 27 addition: The paper published in JLC: Sergei Artemov. Serial properties, selector proofs and the provability of consistency. Journal of Logic and Computation, https://doi.org/10.1093/logcom/exae034, Published: 26 July 2024. (Ask me if you have trouble downloading the paper from JLC.)

Abstract. The consistency of a theory means that each of its formal derivations $D_0, D_1, D_2,\ldots$ is free of contradictions. For Peano Arithmetic $\textsf{PA}$, after the standard coding of derivations by numerals, $\textsf{PA}$-consistency is directly represented by the consistency scheme $\mathrm{Con}^S(\textsf{PA})$, which is a series of arithmetical statements "$n$ is not a code of a derivation of $(0=1)$" for numerals $n = 0,1,2,\ldots$ . We note that the consistency formula $\mathrm{Con}(\textsf{PA})$, $\forall x$ "$x$ is not a code of a derivation of $(0=1)$" is strictly stronger in $\textsf{PA}$ than $\textsf{PA}$-consistency and corresponds to some other property which we call "uniform consistency." When studying the provability of consistency in $\textsf{PA}$, we should work not with the consistency formula $\mathrm{Con}(\textsf{PA})$ but with the consistency scheme $\mathrm{Con}^S(\textsf{PA})$, which adequately represents $\textsf{PA}$ consistency.

This paper introduces the Hilbert-inspired notion of proof of an infinite series of formulas in a theory and proves $\textsf{PA}$-consistency in the form $\mathrm{Con}^S(\textsf{PA})$ in $\textsf{PA}$. These findings show that $\textsf{PA}$ proves its consistency, whereas, by Goedel's second incompleteness theorem, $\textsf{PA}$ cannot prove its uniform consistency.

Comments for the OF readers.

1. Picking $\mathrm{Con}(\textsf{PA})$ to represent the consistency of $\textsf{PA}$ has been a strengthening fallacy. $\textsf{PA}$-consistency as a property of formal derivations is fairly represented by the scheme $\mathrm{Con}^S(\textsf{PA})$, which is a property of numerals. The formula $\mathrm{Con}(\textsf{PA})$ is strictly stronger in $\textsf{PA}$ than the $\textsf{PA}$-consistency. So, the (un)provability of consistency analysis based on $\mathrm{Con}(\textsf{PA})$ is void, and we ought to consider $\mathrm{Con}^S(\textsf{PA})$ instead. This is not a matter of taste or aesthetic preferences but rather a solid mathematical necessity.

2. To analyze the provability of consistency, we need to agree on what counts as proof of a serial property, here $\mathrm{Con}^S(\textsf{PA})$, in $\textsf{PA}$. The paper offers a complete account of the choices and argues in favor of the one endorsed by Hilbert in the 1920s, which we call selector proofs. There is not much freedom here, either: selector proofs have been tacitly used in mathematics, and the time is ripe to formalize them officially.

3. The rest is a standard proof theoretical treatment of $\mathrm{Con}^S(\textsf{PA})$ with a modest technical contribution that the selector based on partial truth definitions an easily formalizable p.r. function.

A special comment for people who believe in $\mathrm{Con}(\textsf{PA})$ in the context of provability in $\textsf{PA}$: $\mathrm{Con}(\textsf{PA})$ is the wrong way to represent $\textsf{PA}$ consistency. If you try to check why $\mathrm{Con}(\textsf{PA})$ is equivalent to $\textsf{PA}$ consistency, you would need to refer to the standard model of $\textsf{PA}$ or similar notions requiring strong meta-assumptions that defeat the purpose of analyzing the provability of consistency in $\textsf{PA}$.

The right way to represent consistency property (which is a property of finite derivation strings) arithmetically is by a serial property/scheme $\mathrm{Con}^S(\textsf{PA})$, which is a series of claims "$n$ is consistent" for numerals $n = 0,1,2,\ldots$. It is immediate that "$\textsf{PA}$ is consistent" is equivalent to $\mathrm{Con}^S(\textsf{PA})$ without any metamathematical assumptions about $\textsf{PA}$. Furthermore, it is easy to check that $\mathrm{Con}(\textsf{PA})$ is strictly stronger than $\mathrm{Con}^S(\textsf{PA})$ in $\textsf{PA}$ which makes Goedel's result about the unprovability of $\mathrm{Con}(\textsf{PA})$ not directly applicable to $\textsf{PA}$ consistency (which is equivalent to $\mathrm{Con}^S(\textsf{PA})$ in $\textsf{PA}$).

Answer 5

Santos, Sieg, and Kahle have a published paper building on Artemov's paper. They argue for a similar position and discuss its relation with Hilbert's program.

Paulo Guilherme Santos, Wilfried Sieg, Reinhard Kahle, A new perspective on completeness and finitist consistency, Journal of Logic and Computation, 2023;, exad021, https://doi.org/10.1093/logcom/exad021

Answer 6

I have waited for Noah Schweber to correct his above presentation of my work after we had a meaningful exchange in which Noah seemed to understand (does not mean to accept) my definitions and constructions. Now, the time is up, and, whereas Noah himself stopped producing his arguments and conclusions, his comment still stands unaltered and, unfortunately, spreads misunderstanding.

In my work, there are several interrelated but different constructions involved in the consistency proof.

1. A selector proof of a serial property ${F_0,F_1,F_2,...}$ in $T$, reasonably well presented by Noah Schweber: it is a pair of

(i) a selector $s(n)$ such that for each $n$, $s(n)$ is a $T$-proof of $F_n$ and

(ii) a proof in $T$ that (i) always works.

This notion applies to both formal and contentual theories. Noah Schweber's comment duly mentions the necessity of (ii).

2. A consistency proof (in ${\sf PA}$, for short) is

A. a mathematical selector proof of consistency of ${\sf PA}$ such that each $s(n)$ yields a contextual (mathematical) proof that $n$ is not a proof of $0=1$ in ${\sf PA}$;

B. a formalization of (A) in ${\sf PA}$.

This corresponds to Hilbert's approach: a consistency proof in $T$ is a mathematical proof of consistency, and this proof is formalized in $T$.

The difference between a selector proof of the consistency scheme and a selector proof of consistency property was explicitly discussed in both arXiv preprint 2024 and JLC_2024 paper, section 5.2, with exactly the same example as given by Noah Schweber. I am puzzled how, after all these materials, somebody could publicly claim a "more general and much easier" proof of the consistency property by just repeating the example given in Section 5.2 with a warning to avoid it.

Here is a specific misrepresentation. I am applying a traditional (and nontrivial) proof-theoretical technique to prove the $\sf PA$ consistency in $\sf PA$ (which is much more than just proving consistency scheme ${\sf Con}^S({\sf PA})$ in $\sf PA$ formally). Noah Schweber instead presents a well-known solution of a different and much easier task of proving ${\sf Con}^S({\sf PA})$ in $\sf PA$ formally. This trick has nothing to do with my results of proving consistency at all.

A friendly piece of advice: this work is quite subtle, and many "obvious" versions of it are plain wrong. Read the paper by yourself: https://doi.org/10.1093/logcom/exae034,