31
$\begingroup$

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

$\endgroup$
17
  • 3
    $\begingroup$ I voted to close, because MO is not the right venue for discussing correctness of preprints. $\endgroup$ Apr 17 at 6:02
  • 40
    $\begingroup$ I think MO is the right venue for questions like this. $\endgroup$
    – Alec Rhea
    Apr 17 at 9:31
  • 7
    $\begingroup$ @MikhailKatz I think there’s precedence for asking questions about specific parts or claims in a preprint, but not “is this preprint correct or not?”, regardless of the strength of the mathematician. Cf. the recent questions on abc, which I think was handled well. $\endgroup$ Apr 17 at 10:22
  • 12
    $\begingroup$ I think this question is ok for MO, but could be improved by saying exactly what you are looking for in terms of answers, rather than just request users to "comment on the upshot" of the paper. As is, together with the focus on the publication status of the paper in the first paragraph, it sort of comes across as though you are most interested in whether the paper will be published. $\endgroup$ Apr 17 at 11:47
  • 6
    $\begingroup$ What "FoM" means? (I hate acronyms). $\endgroup$ Apr 18 at 19:01

4 Answers 4

59
$\begingroup$

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$.

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.

$\endgroup$
16
  • 8
    $\begingroup$ @ChristianRemling: Consistency is a technically simple definition, but it’s an empirical fact that people often get very confused about it (even before its formal coding into arithmetic). Maybe it shouldn’t be so confusing, but in practice it is. $\endgroup$ Apr 16 at 23:49
  • 9
    $\begingroup$ What a great answer. I realize this comment adds nothing, but my upvote seemed insufficient to express my thanks. $\endgroup$ Apr 16 at 23:52
  • 16
    $\begingroup$ @MikhailKatz "Denialist" is in no way a "snide remark" or an "inference", it is a descriptive term. Artemov denies (hence denialist) that the formal sentence Con(PA) captures the whole mathematical concept of "consistency of arithmetics". $\endgroup$ Apr 17 at 10:21
  • 12
    $\begingroup$ @MikhailKatz I agree with Marco Capitani. In his paper, Artemov himself emphasizes that he is taking a contrarian position, as you can see from his exhortations to the community to change their minds about a conventionally accepted belief. And what is contrarian about his view? Precisely that he denies the Claim. Someone who denies is a denialist. It would be misleading to suggest that Artemov is just doing math as usual and not making any controversial claims. $\endgroup$ Apr 17 at 12:06
  • 8
    $\begingroup$ "for any finite subset of the axioms of PA, PA can prove that that finite set of axioms is consistent." A very important caveat is that PA can't prove the statement "every finite subset of PA is consistent". Rather, you need a different proof for each finite subset, and in particular this requires doing meta-mathematics over infinitely many statements, not just working in PA. $\endgroup$ Apr 17 at 14:02
36
$\begingroup$

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.

$\endgroup$
10
  • 4
    $\begingroup$ Unless I'm missing something, there's no need to appeal to reflection in Artemov's claim. Consider the function $p$ which on input $n$ behaves as follows. First, we check whether $n$ is a PA-proof of $\perp$. If it is not, then $p$ outputs a formal proof verifying this. If it is, though, then we can explicitly find a slightly larger number $m$ which is a PA-proof of "$n$ is not a PA-proof of $\perp$," using the proof coded by $n$ together with ex falso, and $p$ outputs that $m$. This $p$ is primitive recursive, and all of the above is verifiable in PA. Or have I made a mistake here? $\endgroup$ Apr 17 at 0:15
  • 1
    $\begingroup$ Certainly the appeal to reflection is a "better" schematic proof, but I see no reason why what I've described doesn't fit Artemov's criteria for a schematic proof. And this seems to weaken his claim that schematic provability of consistency of PA inside PA has some foundational value, irrespective of his concerns about the second incompleteness theorem. $\endgroup$ Apr 17 at 0:16
  • $\begingroup$ @NoahSchweber: I completely agree; have edited to reflect that point. $\endgroup$ Apr 17 at 9:14
  • 3
    $\begingroup$ @PeterLeFanuLumsdaine You have misstated Artemov's definition; the key property of the p.r. function in (2) should itself be PA-provable. This leads to a less trivial situation. See Definition 1 on page 9 of Artemov's paper. $\endgroup$ Apr 17 at 14:23
  • 1
    $\begingroup$ Since the definition in Artemov's paper is apparently different, I deleted my comments above so as not to proliferate the confusion. $\endgroup$ Apr 17 at 16:37
14
$\begingroup$

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.

$\endgroup$
1
  • 1
    $\begingroup$ 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$. $\endgroup$ Apr 17 at 23:22
10
$\begingroup$

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

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.