16
$\begingroup$

As discussed in another MO question, Sergei Artemov has proposed that the standard formalization Con(PA) of "PA is consistent" is flawed, and has proposed a different way to formalize "proving that PA is consistent" (which he claims is closer to Hilbert's original intention).

Setting aside the debates over the "correctness" of Artemov's formalization, we can ask a technical question:

Can PA prove that ZF is consistent (in Artemov's sense)?

Artemov shows that, according to his definitions, PA proves that PA is consistent, and suggests that Hilbert's program is not yet dead. But what Hilbert wanted wasn't an arithmetic proof that arithmetic is consistent; he wanted a finitary proof that set theory is consistent. If we provisionally accept Artemov's definitions, can Hilbert's desire for a finitary proof of the consistency of set theory be realized?

REMARK: Arguably, the present question is a duplicate of Does PA prove (Artemov-style) the consistency of a stronger system? and the present question was indeed, at one point in time, closed as a duplicate. However, the community subsequently decided to reopen the present question, perhaps in part because Artemov himself has posted an answer that clarifies some things.

Improve this question
$\endgroup$
26
  • 5
    $\begingroup$ 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. $\endgroup$
    – Noah Schweber
    Commented Jul 27 at 17:29
  • 2
    $\begingroup$ 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. $\endgroup$
    – Joel David Hamkins
    Commented Jul 27 at 17:33
  • 3
    $\begingroup$ @Joel David Hamkins. This is correct: ZF selector proves its consistency; see my JLC paper. $\endgroup$
    – Sergei Artemov
    Commented Jul 28 at 0:00
  • 5
    $\begingroup$ 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? $\endgroup$
    – Joel David Hamkins
    Commented Jul 28 at 2:28
  • 2
    $\begingroup$ @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? $\endgroup$
    – Joel David Hamkins
    Commented Jul 30 at 20:54

1 Answer 1

Reset to default
3
$\begingroup$

Thank you for your interest and for advertising my work.

The answer to this specific question (as well as to most of the questions asked on my work in this venue) is given in 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.)

Here is the answer (a quote from the paper):

Whereas our methods allow proving the consistency of a theory in itself, we don’t know how to prove in T the consistency of a theory S, which is strictly stronger than T. 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.

This paper refutes the Unprovability of Consistency thesis, and these findings have their foundational value. Though this does not reach the goals of Hilbert’s consistency program, it removes a principal roadblock on its way.

So, my humble contribution to Hilbert’s program is mostly moral

  1. It removes the widely accepted misconception that G2 killed Hilbert’s program.

  2. Moreover, it shows that this misconception was unwarranted from the very beginning, the 1930s. The unprovability of consistency argument was based on the assumption that any PA-consistency proof in PA should be PA provably equivalent to Con(PA), which had no justification then (cf. the JLC paper for the details) and now is proven false.

BTW, we don't need Hilbert's authority to show that Con(PA) is not equivalent to "PA is consistent" over PA. Here is a clean math argument with some obvious technical assumptions like "PA derivations are finite syntactic objects", "Goedel numbers of PA-derivations are numerals," "Godel numbering preserves the elementary computational structure of PA-derivations, e.g., D is not a proof of 0=1 iff the code of D is not a code of a sequence containing the line 0=1," etc.

Here is the argument

  1. Consistency of PA is a property "no formal derivation in PA proves 0=1." This is a canonical textbook definition.

  2. Godel numbering transliterates this property in its equivalent form (*): "for any numeral n, n is not a code of a PA-derivation containing the line 0=1."

  3. Since quantification over numerals is not expressible in PA, we have to use some other means to equivalently represent "for any numeral n ... ". An obvious way to do this is by a p.r. string of sentences (which we call the consistency scheme Con^S(PA): "0 is not a code of a PA-derivation containing the line 0=1," "1 is not a code of a PA-derivation containing the line 0=1," "2 is not a code of a PA-derivation containing the line 0=1," etc. It is immediate that (*) is mathematically equivalent to Con^S(PA) without any meta-assumptions about PA.

  4. Con(PA) is strictly stronger than Con^S(PA) in PA (an easy exercise), hence Con(PA) is strictly stronger than (*).

Improve this answer
$\endgroup$
27
  • 6
    $\begingroup$ 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? $\endgroup$
    – Noah Schweber
    Commented Jul 27 at 18:55
  • 10
    $\begingroup$ -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$. $\endgroup$
    – Alex Kruckman
    Commented Jul 27 at 23:16
  • 6
    $\begingroup$ 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 $\endgroup$
    – Alex Kruckman
    Commented Jul 27 at 23:27
  • 5
    $\begingroup$ @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. $\endgroup$
    – Noah Schweber
    Commented Jul 28 at 0:12
  • 8
    $\begingroup$ 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. $\endgroup$
    – Noah Schweber
    Commented Jul 28 at 0:16

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .