Is the usual enumeration of $\mathsf{PA}$ "minimal for consistency strength"?

Question

This question is about a technical imprecision which is easily avoidable but whose details I'd like to understand better. When we refer to "the consistency strength of $\mathsf{PA}$" (say) we aren't properly referring to $\mathsf{PA}$ as a set; rather, we care about the specific way in which $\mathsf{PA}$ is enumerated. "The set of sentences which $\mathsf{ZFC}$ proves are $\mathsf{PA}$-axioms" is another way to define the same (hopefully!) set, but properly speaking it is equiconsistent with $\mathsf{ZFC}$.

It occurs to me that I don't know whether the usual description of the $\mathsf{PA}$ axioms is optimal with respect to consistency strength. Below, let $(T_e)_{e\in\omega}$ be some appropriate enumeration of the c.e. theories. Suppose WLOG that $T_0$ is the usual c.e. presentation of $\mathsf{PA}$.

Question: Is there an index $e$ such that ("extensionally") $T_e=\mathsf{PA}$ but $\mathsf{PA}+\mathsf{Con}(T_e)\not\vdash \mathsf{Con}(T_0)$?

One natural way to try to get a positive answer to this question is to enumerate the axioms of $\mathsf{PA}$ very slowly, waiting for contradictions, along the following lines: given a $\mathsf{PA}$-provably-total computable function $f$, let $T_f$ be the c.e. theory which enumerates the $n$th axiom of $\mathsf{PA}$ in the usual ($T_0$) sense iff there is no contradiction in $\mathsf{PA}$ using fewer than $f(n)$-many symbols. As long as $f$ is reasonably-fast-growing (say, dominating $n\mapsto 2^n$) it seems "$\mathsf{PA}$-believable" that $T_f$ detects a contradiction before falling prey to it. On the other hand, I don't see how to show the consistency of $\mathsf{PA}+\mathsf{Con}(T_f)+\neg\mathsf{Con}(T_0)$ for any specific $f$.

(This older question seems thematically similar, but I don't actually see a concrete connection.)

Answer 1

No (to the title), yes (to the question), see

Sy-David Friedman, Michael Rathjen, and Andreas Weiermann: Slow consistency, Annals of Pure and Applied Logic 164 (2013), no. 3, pp. 382–393, doi 10.1016/j.apal.2012.11.009.

The idea is that an axiom of usual PA of Gödel number $n$ is padded to length $f(n)$, where $f$ is a recursive function growing faster than all provably total recursive functions of PA (namely, $F_{\epsilon_0}$).

Answer 2

The cautious enumeration idea in my paper has some affinity with your suggestion.

• Joel David Hamkins, Nonlinearity and illfoundedness in the hierarchy of large cardinal consistency strength, arxiv:2208.07445.

The cautious enumeration of PA, denoted $\text{PA}^\circ$, enumerates the usual axioms of PA, unless a proof is found in PA of $\neg\text{Con}(\text{PA})$, in which case the enumeration stops. This is strictly weaker than PA in consistency strength, as argued in the paper, but in fact enumerates the very same axioms, assuming Con(PA+Con(PA)).

I argue in the paper that the cautious enumerations of our favorite theories, such as PA or ZFC, are natural, in the sense that this is what we would actually do if we were enumerating the theories and encountered such a proof along the way.

The cautious enumeration construction can be iterated, to find natural instances of ill-foundedness in the hierarchy of consistency strength. $$\cdots < \text{ZFC}^{\circ\circ\circ} < \text{ZFC}^{\circ\circ} < \text{ZFC}^{\circ} <\text{ZFC}$$

Meanwhile, I prove that the stop-when-hopeless enumeration, which enumerates the usual axioms until such a point when the proof of a contradiction is observed, is equiconsistent with the original theory. The difference between this enumeration and the cautious enumeration is the difference between searching for a proof of a contradiction and searching for a proof that there is a proof of a contradiction. The latter gives lower consistency strength; the former does not.