$\Pi^0_1$ sentences modulo "schematic entailment"

Question

Let $\mathfrak{P}$ be the preorder of $\Delta^0_0$ (= only bounded quantifiers) formulas with one free variable in the language of arithmetic, under the relation $\alpha(x)\le\beta(x)$ iff there is a primitive recursive function $p$ such that $$\mathsf{PA}\vdash \forall x[\neg\alpha(x)\rightarrow\neg\beta(p(x))].$$

As top element $\mathfrak{P}$ has the class of all formulas $\varphi$ such that $\forall x\varphi(x)$ is not true; the bottom element is the class of $x=x$, and the formula "$x$ is not a $\mathsf{PA}$-proof of $\perp$" is maximal amongst formulas whose universal closure is "schematically verifiable in $\mathsf{PA}$" in a particular sense (see this answer of mine.)

I suspect this preorder is well-known in proof theory, but I haven't seen it before; my question is, what is it?

Answer 1

I've tweaked the question to be a bit more comprehensible; the language-extension issue reappears in this answer, though.

---

Let $\mathsf{Lind}(T)$ be the Lindenbaum poset of a theory $T$, and for $\Gamma$ a syntactic class let $\mathsf{Lind}_\Gamma(T)$ be the sub-poset of $\mathsf{Lind}(T)$ consisting of (classes containing) elements of $\Gamma$.

Separately, for $T\supseteq S$ c.e. sound theories in the language of arithmetic extending $\mathsf{I\Sigma_1}$, let $A(T,S)$ be the preorder of $\Pi^0_1$ sentences under the relation $\varphi\le\psi$ iff there is an $S$-provably-total computable function $f$ such that $T$ proves if $n$ is a counterexample to $\varphi$ then $f(n)$ is a counterexample to $\psi$. The specific setup in the question is $A(\mathsf{PA},\mathsf{I\Sigma_1})$.

A natural guess at this point is that $A(\mathsf{PA},\mathsf{I\Sigma_1})$ is just $\mathsf{Lind}_{\Pi^0_1}(\mathsf{I\Sigma_1}+\mathsf{PA}[\Pi^0_1])$, where $\mathsf{PA}[\Pi^0_1]$ is the set of $\Pi^0_1$ consequences of $\mathsf{PA}$; and that more generally $A(T,S)=\mathsf{Lind}_{\Pi^0_1}(S+T[\Pi^0_1])$.

However, unless I'm missing something this is not quite right. Certainly the following are true:

• The $\Pi^0_1$ theorems of $T$ are exactly the $A(T,S)$-minimal sentences.

• Suppose $S+\theta\vdash \neg\varphi\rightarrow\neg\psi$, where $\theta\in T[\Pi^0_1]$. Then the function "Check if $n$ is a counterexample to $\varphi$; if it isn't, output $7$, and if it is find and output the least $k$ which is a counterexample to $\psi\vee\theta$" is $S$-provably-total so $\varphi\le\psi$ in $A(T,S)$.

The trouble comes at the following point. Suppose $\varphi\le\psi$ in $A(T,S)$ via $f$. Let $\chi$ be the sentence "For every $n$, if $n$ is a counterexample to $\varphi$ then $f(n)$ is defined and is a counterexample to $\psi$." This is almost but not quite a $\Pi^0_1$ theorem of $T$; the issue is the clause asserting that $f(n)$ is defined.

Instead, what is true is that $A(T,S)$ is $\mathsf{Lind}_{\Pi^0_1}(S+T[\Pi^0_1/S])$, where $T[\Pi^0_1/S]$ is the set of $\Pi^0_1$ consequences of the natural expansion of $T$ to the larger language containing a symbol for each provably total function of $S$.

Summing up: $A(T,S)$ is just the $\Pi^0_1$ fragment of the Lindenbaum algebra of a particular theory built from $T$ and $S$, but it's a bit finnicky to get that theory right.