The finitistic consistency of Heck's predicative Fregean system (Q2345392)

Heck's theory \(\mathsf{H}\), also called \textit{predicative Fregean theory}, is: {(1)} a monadic second-order system with equality; {(2)} with a comprehension axiom-scheme (that is \(\exists F \, \forall x \, (Fx \leftrightarrow \phi(x))\)) restricted to predicative (that is without second-order quantifiers) formulas \(\phi(x)\); {(3)} with a value-range operator \(\hat{\;}\) (that is an operator that given a formula \(\phi(x)\) produces a first-order term \(\hat{x}.\phi(x)\)) with its axiom-scheme (that is \((\hat{x}.\phi(x)\) = \(\hat{x}.\psi(x)) \leftrightarrow \forall x \, (\phi(x) \leftrightarrow \psi(x))\)). We can extend \(\mathsf{H}\) in three ways: {(1)} by adding \(\Delta^1_1\)-comprehension (that is the axiom-scheme \(\forall x \, (\phi(x) \leftrightarrow \psi(x)) \rightarrow \exists F \, \forall x \, (Fx \leftrightarrow \phi(x))\) where \(\phi \in \Sigma^1_1\) and \(\psi \in \Pi^1_1\)), obtaining a theory that we will denote by \(\mathsf{H}'\); {(2)} by ramifying (that is considering the previous second-order variables \(F\), \(G\), \(\ldots\) as having type \(0\), adding new second-order variables \(F^n\), \(G^n\), \(\ldots\) for each type \(n> 0\) and adding new comprehension axiom-schemes \(\exists F^n \, \forall x \, (F^n x \leftrightarrow \phi(x))\) where the second-order bounded (free) variables in \(\phi(x)\) have type \(m < n\) (\(m \leq n\), respectively)), obtaining a theory that we will denote by \(\mathsf{H}''\); {(3)} by applying the two previous extensions simultaneously (adding \(\Delta^1_1\)-comprehension for each type \(n\)), obtaining a theory that we will denote by \(\mathsf{H}'''\). In the past, it was proved that \(\mathsf{H}\), \(\mathsf{H}'\) and \(\mathsf{H}''\) are consistent using model-theoretic arguments. The authors reprove these results, and even strengthen them by including \(\mathsf{H}'''\), with a new finitistic (that is formalisable in primitive recursive arithmetic \(\mathsf{PRA}\) and even in \(\mathsf{I}\Delta_0(\mathrm{super}^3\mathrm{exp})\)) proof. The authors' motivation is the search for upper bounds for interpretability in consistent fragments of Frege's theory, which they find by combining finitistic consistency proofs with Gödel's second incompleteness theorem: if there is a finitistic consistency proof of a theory \(\mathsf{T}\) formalisable in a theory \(\mathsf{T}'\), then \(\mathsf{T}'\) is not interpretable in \(\mathsf{T}\). This proof has three major steps: {(1)} the authors finitistically prove an extension of Shoenfield's theorem saying that if a first-order schematisation \(\mathsf{T}^s\) (obtained from of a theory \(\mathsf{T}\) with \(\Pi^1_1\)-axioms by restricting \(\mathsf{T}\) to its first-order part and replacing its \(\Pi^1_1\)-axioms by their predicative instantiations without second-order variables) is consistent, then \(\mathsf{T}'\) (obtained from \(\mathsf{T}\) by adding \(\Sigma^1_1\)-choice that implies \(\Delta^1_1\)-comprehension) is consistent, and they recall that Parsons's theory \(\mathsf{P} = \check{\mathsf{H}}^s\) (where \(\check{\mathsf{H}}\) is \(\mathsf{H}\) with \(\hat{\;}\) restricted to predicative formulas) is finitistically consistent, so \(\check{\mathsf{H}}'\) is finitistically consistent -- this step is a new contribution; {(2)} using the previous point, they prove that \(\mathsf{H}'\) is finitistically interpretable in \(\mathsf{PV}^+_\omega\) (that is Burgess's theory \(\mathsf{PV}_\omega\) together with syntax and axioms for pairing, syntax and axioms for a restriction of \(\hat{\;}\), some comprehension and some choice) and they prove that \(\mathsf{PV}^+_\omega\) is finitistically consistent, so \(\mathsf{H}'\) is finitistically consistent -- this step uses techniques by John Burgess; {(3)} using the previous points, they prove that if \(\mathsf{T}\) is a finitistically consistent theory in a first-order Parsons language with finitely many sorts, then \(\mathsf{T}^{\mathsf{H}}\) (that is the extension of \(\mathsf{T}\) to second order with \(\hat{\;}\) and its axiom-scheme and possibly \(\Delta^1_1\)-comprehension), all theories in the chain \(\mathsf{T} \subseteq \mathsf{T}^{\mathsf{H}} \subseteq (\mathsf{T}^{\mathsf{H}})^{\mathsf{H}} \subseteq \cdots\) and its union \(\mathsf{T}^\cup = \mathsf{T} \cup \mathsf{T}^{\mathsf{H}} \cup (\mathsf{T}^{\mathsf{H}})^{\mathsf{H}} \cup \cdots\) are finitistically consistent, furthermore they notice that taking \(\mathsf{T} = \mathsf{P}\) they (essentially) get \(\mathsf{T}^\cup = \mathsf{H}'''\), so \(\mathsf{H}'''\) is finitistically consistent -- this step iterates the preceding work.