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

Question

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

Answer 1

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.

Answer 2

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.