Does PA prove (Artemov-style) the consistency of a stronger system?

There was a recent question on Artemov's paper here on MO Situation with Artemov's paper?

In one of the answers there it was asserted (apparently incorrectly - see Noah Schweber's comments and answer) that the main mathematical claim of the paper is (where PA is 1st-order Peano Arithmetic):

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, there is a primitive recursive function taking each $$n$$ to the PA-proof of “$$\lnot (n \colon \bot)$$

My question is, are there any systems $$T$$ stronger than PA such that

1. for each $$n$$, PA proves the statement “$$n$$ does not code a proof of $$\bot$$ in $$T$$” (which we abbreviate as “$$\lnot_T (n \colon \bot)$$”)
2. moreover, there is a primitive recursive function taking each $$n$$ to the PA-proof of “$$\lnot_T (n \colon \bot)$$

If so, can one give a characterisation of such $$T$$?

• This misstates 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, or the edit to my answer. Apr 17 at 14:22
• I haven't read Artemov's paper, and indicated my lack of knowledge by "Apparently.". I'm quoting an answer by Peter LeFanu Lumsdaine to the linked question, which you are aware of since you commented under it Perhaps you should put this comment there as well? Sorry for my contribution to this confusion.
– abo
Apr 17 at 14:36
• I did comment on his answer. Apr 17 at 14:37
• And I said you did comment on his answer. Perhaps I am misunderstanding what you did comment there, but I don't see you saying that he has misstated Artemov's definition.
– abo
Apr 17 at 14:39
• Look again (maybe refresh your browser?), I definitely did: mathoverflow.net/questions/469247/… Apr 17 at 14:40

This property holds more-or-less for every consistent recursively axiomatized theory $$T$$, even with Q in place of PA.

More precisely, there is a hidden parameter in the question, namely what formula $$\tau(x)$$ is used in the definition of “$$n\colon\bot$$” to define the set of axioms of $$T$$. (The same theory $$T$$ can be defined by many different axiom sets, and a single set of axioms may be defined by many different formulas that are not provably equivalent.) What I wrote literally holds when $$\tau$$ is $$\Delta_0$$, as then $$\neg(n\colon\bot)$$ is a true $$\Delta_0$$ sentence, and every true $$\Delta_0$$ sentence is provable in $$Q$$, by a proof computable in time exponential in the value of the bounds of the formula.

Note that every recursively enumerable theory is $$\Delta_0$$-axiomatizable by Craig’s trick.

But in any case, if $$\tau$$ is not necessarily $$\Delta_0$$, the statement holds in metatheory $$S$$ in place of PA if there is a primitive recursive function that takes $$n$$ to an $$S$$-proof of $$\tau(n)$$ or $$\neg\tau(n)$$, whichever is true. Thus, e.g., it holds for all primitive recursive axiomatizations $$\tau$$ if $$S$$ contains PRA.

This question misses a point in Artemov's paper, namely that the relevant property of the p.r. function in (2) should itself be PA-provable; see Definition 1 on page 9. This leads to a less trivial situation, and this is what my answer addresses:

Suppose $$\varphi(x)$$ is a $$\Delta_0$$ formula such that $$\mathbb{N}\models\forall x\varphi(x)$$. I claim the following are equivalent:

1. There is a primitive recursive function $$g$$ such that $$\mathsf{PA}$$ proves "for every $$n$$, if $$\varphi(n)$$ fails then $$g(n)$$ is a $$\mathsf{PA}$$-proof of $$\perp$$." (Note that this is prima facie stronger than $$\mathsf{PA}+Con(\mathsf{PA})\vdash\forall x\varphi(x)$$.)

2. There is some primitive recursive $$f$$ such that $$\mathsf{PA}$$ proves "for each $$n$$, $$f(n)$$ is a $$\mathsf{PA}$$-proof of $$\varphi(n)$$."

• $$1\rightarrow 2$$: Fix $$g$$ as in $$1$$, and consider the function $$f$$ defined as follows. On input $$n$$ we first check whether $$\varphi(n)$$ is actually true; the "brute force verification" proof of this fact, if indeed it is true, can be generated primitive recursively. If $$\varphi(n)$$ holds we output this brute force verificatino. If on the other hand we see that $$\varphi(n)$$ is false, then we output $$g(n)$$. This can all be bundled together as a primitive recursive function (the key point being that verifying/falsifying a $$\Delta_0$$ sentence can be done quickly), so we have $$2$$.

• $$2\rightarrow 1$$: Fix $$f$$ as in $$2$$, and consider the function $$g$$ defined as follows. On input $$n$$ we first check whether $$\varphi(n)$$ holds. If it does, we output $$17$$ (or whatever). If $$\varphi(n)$$ fails, then we output the $$\mathsf{PA}$$-proof of $$\perp$$ gotten by combining the (short) falsification of $$\varphi(n)$$ with the proof $$f(n)$$.

So what? Well, this tells us that if $$\mathsf{PA}$$ "Artemov-proves" $$Con(T)$$, then we already have $$\mathsf{PA}+Con(\mathsf{PA})\vdash Con(T)$$. So in a reasonably strong sense we get that $$\mathsf{PA}$$ can't go "past itself" in Artemov's sense.

As a digression, condition 1 does suggest something interesting. Given $$\Pi^0_1$$ sentences $$\alpha\equiv\forall x\psi(x)$$ and $$\beta\equiv\forall x\theta(x)$$ (with $$\psi,\theta\in\Delta_0$$), write "$$\alpha\le_\mathsf{PA}\beta$$" iff there is a primitive recursive function $$f$$ such that $$\mathsf{PA}\vdash\forall n[\neg\psi(n)\rightarrow\neg \theta(f(n))]$$. (Since $$\Delta_0$$ statements can be efficiently checked I don't see any value in shifting from instances to proofs here.)

This gives rise to a degree structure on the $$\Pi^0_1$$ sentences. The false $$\Pi^0_1$$ statements are appropriately maximal, while the argument above (suitably tweaked) shows that $$Con(\mathsf{PA})$$ is the $$\le_\mathsf{PA}$$-maximal element of the set of "Artemov-provable" sentences. I strongly suspect this degree structure is well-known in proof theory, but I'm not a proof theorist. Any references welcome!

Note that if we replaced "primitive recursive" with "PA-provably-total" this would just be the $$\Pi^0_1$$ part of the Lindenbaum algebra over $$\mathsf{PA}$$: if $$\mathsf{PA}\vdash\beta\rightarrow\alpha$$ then $$\mathsf{PA}$$ proves that the function sending each counterexample to $$\alpha$$ to the smallest counterexample to $$\beta$$, and sending everything else to $$17$$, is total.

• The question only requires that there is a primitive recursive function taking $n$ to a PA-proof of $\neg_T(n\colon\bot)$, not that this statement is itself verifiable in PA. Apr 17 at 8:23
• @EmilJeřábek I missed that; I thought Artemov's paper did require that statement to be PA-provable, though? Apr 17 at 14:08
• @EmilJeřábek Unless I'm having a silly moment Artemov's paper does make such a requirement; see my edit. Apr 17 at 14:24
• @EmilJeřábek Yeah, there's a bit of a game of telephone going on here. This question took Peter's summary of the paper for granted. Apr 17 at 15:33
• @EmilJeřábek True, but to avoid perpetuating this confusion the question should not reference Artemov's paper. As long as Artemov's paper is referenced here, I think it's important to have an answer which addresses that formulation too. Apr 17 at 16:39