I have waited for Noah Schweber to correct his above presentation of my work after we had a meaningful exchange in which Noah seemed to understand (does not mean to accept) my definitions and constructions. Now, the time is up, and, whereas Noah himself stopped producing his arguments and conclusions, his comment still stands unaltered and, unfortunately, spreads misunderstanding.
In my work, there are several interrelated but different constructions involved in the consistency proof.
- A selector proof of a serial property ${F_0,F_1,F_2,...}$ in $T$, reasonably well presented by Noah Schweber: it is a pair of
(i) a selector $s(n)$ such that for each $n$, $s(n)$ is a $T$-proof of $F_n$ and
(ii) a proof in $T$ that (i) always works.
This notion applies to both formal and contentual theories. Noah Schweber's comment duly mentions the necessity of (ii).
- A consistency proof (in ${\sf PA}$, for short) is
A. a mathematical selector proof of consistency of ${\sf PA}$ such that each $s(n)$ yields a contextual (mathematical) proof that $n$ is not a proof of $0=1$ in ${\sf PA}$;
B. a formalization of (A) in ${\sf PA}$.
This corresponds to Hilbert's approach: a consistency proof in $T$ is a mathematical proof of consistency, and this proof is formalized in $T$.
The difference between a selector proof of the consistency scheme and a selector proof of consistency property was explicitly discussed in both arXiv preprint 2024 and JLC_2024 paper, section 5.2, with exactly the same example as given by Noah Schweber. I am puzzled how, after all these materials, somebody could publicly claim a "more general and much easier" proof of the consistency property by just repeating the example given in Section 5.2 with a warning to avoid it.
A friendly piece of advice: this work is quite subtle, and many "obvious" versions of it are plain wrong. Read the paper by yourself: https://doi.org/10.1093/logcom/exae034,