The FAN principle and weak König's lemma in Herbrandized second-order arithmetic (Q2195636)

The work developed in this paper can be seen as an extension of the star calculus from [\textit{F. Ferreira} and \textit{ G. Ferreira}, Arch. Math. Logic 56, No. 5--6, 523--539 (2017; Zbl 1417.03290)] to Heyting arithmetic. The star calculus is a typed combinatory calculus with a type constructor that, to each type \(\tau\), associates the star type \(\tau^*\) corresponding to the nonempty finite subsets of elements of type \(\tau\). The Herbrandization relies on the fact that formulas are considered in a \textit{bounded mixed language} that includes bounded arithmetical quantifiers and bounded structural quantifications of the form \(\forall x^{\tau} \in t^{\tau^*}\,(\dots)\) or of the form \(\exists x^{\tau} \in t^{\tau^*}\,(\dots)\), where \(x\) is a variable of type \(\tau\) and \(t\) is a term of the star type \(\tau^*\). The present paper introduces a sound functional interpretation of a first-order extension of Heyting arithmetic. This functional interpretation is able to interpret certain principles such as Markov's principle, the bounded independence of the premises principle, the lesser limited principle of omniscience, and the principle of bounded contra-collection, and is therefore considered ``semi-intuitionistic''. The interpretation is indeed ``Herbrandized'' since the witnesses need not to be exact but only contained in a finite set. The interpretation also allows for an extension to second-order arithmetic, interpreting second-order variables as finite sets of natural numbers, which includes a (classically false) formulation of the FAN principle and weak König's lemma. Herbrandized interpretations were first given in the context of nonstandard arithmetic [\textit{B. van den Berg} et al., Ann. Pure Appl. Logic 163, No. 12, 1962--1994 (2012; Zbl 1270.03121)], which also allows for a treatment of weak König's lemma [\textit{B. Dinis} and \textit{F. Ferreira}, Math. Log. Q. 63, No. 1--2, 114--123 (2017; Zbl 1469.03177)]. However, according to the author ``It is a quirk of the history of the subject that Herbrandization was first discovered in the nonstandard setting!''. Moreover, the approach using the start calculus is more structural in the sense that it can be used even in theories that are not theories of arithmetic.