See also the cautious enumeration idea in my paper,

• 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}$$

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.