Ferreira, Fernando; Ferreira, Gilda A herbrandized functional interpretation of classical first-order logic. (English) Zbl 1417.03290 Arch. Math. Logic 56, No. 5-6, 523-539 (2017). Summary: We introduce a new typed combinatory calculus with a type constructor that, to each type \(\sigma \), associates the star type \(\sigma ^*\) of the nonempty finite subsets of elements of type \(\sigma \). We prove that this calculus enjoys the properties of strong normalization and confluence. With the aid of this star combinatory calculus, we define a functional interpretation of first-order predicate logic and prove a corresponding soundness theorem. It is seen that each theorem of classical first-order logic is connected with certain formulas which are tautological in character. As a corollary, we reprove Herbrand’s theorem on the extraction of terms from classically provable existential statements. Cited in 1 ReviewCited in 5 Documents MSC: 03F10 Functionals in proof theory 03B10 Classical first-order logic 03B40 Combinatory logic and lambda calculus 03B15 Higher-order logic; type theory (MSC2010) Keywords:functional interpretations; first-order logic; star combinatory calculus; finite sets; tautologies; Herbrand’s theorem PDFBibTeX XMLCite \textit{F. Ferreira} and \textit{G. Ferreira}, Arch. Math. Logic 56, No. 5--6, 523--539 (2017; Zbl 1417.03290) Full Text: DOI Link References: [1] Avigad, J.; Feferman, S.; Buss, SR (ed.), Gödel’s functional (“Dialectica”) interpretation, No. 137, 337-405 (1998), Amsterdam · Zbl 0913.03053 · doi:10.1016/S0049-237X(98)80020-7 [2] Avigad, J., Towsner, H.: Functional interpretation and inductive definitions. J. Symb. Log. 74(4), 1100-1120 (2009) · Zbl 1193.03082 · doi:10.2178/jsl/1254748682 [3] Borges, A.: On the herbrandised interpretation for nonstandard arithmetic. Master’s thesis, Universidade de Lisboa (2016) [4] Diller, J.: Logical problems of functional interpretations. Ann. Pure Appl. Log. 114, 27-42 (2002) · Zbl 0992.03071 · doi:10.1016/S0168-0072(01)00074-4 [5] Diller, J., Nahm, W.: Eine Variante zur Dialectica-Interpretation der Heyting-Arithmetik endlicher Typen. Archive für mathematische Logik und Grundlagenforschung 16, 49-66 (1974) · Zbl 0277.02006 · doi:10.1007/BF02025118 [6] Ferreira, F., Nunes, A.: Bounded modified realizability. J. Symb. Log. 71, 329-346 (2006) · Zbl 1100.03050 · doi:10.2178/jsl/1140641178 [7] Ferreira, F., Oliva, P.: Bounded functional interpretation. Ann. Pure Appl. Log. 135, 73-112 (2005) · Zbl 1095.03060 · doi:10.1016/j.apal.2004.11.001 [8] Gerhardy, P., Kohlenbach, U.: Extracting Herbrand disjunctions by functional interpretation. Arch. Math. Log. 44, 633-644 (2005) · Zbl 1081.03056 · doi:10.1007/s00153-005-0275-1 [9] Gödel, K.: Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes. dialectica 12, 280-287 (1958). Reprinted with an English translation in [10], pp. 240-251 · Zbl 0090.01003 [10] Gödel, K.: On a hitherto unutilized extension of the finitary standpoint. In: Feferman, S., et al. (eds.) Collected Works, vol. II. Oxford University Press, Oxford (1990) · Zbl 0433.03040 [11] Shoenfield, J.R.: Mathematical Logic. Addison-Wesley Publishing Company, Boston (1967). Republished in 2001 by AK Peters · Zbl 0155.01102 [12] Statman, R.: Lower bounds on Herbrand’s theorem. Proc. Am. Math. Soc. 75(1), 104-107 (1979) · Zbl 0411.03048 [13] Tait, W.: Intentional interpretations of functionals of finite type I. J. Symb. Log. 32, 198-212 (1967) · Zbl 0174.01202 · doi:10.2307/2271658 [14] Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory. Cambridge University Press, Cambridge (1996) · Zbl 0868.03024 [15] Troelstra, A.S. (ed.): Metamathematical Investigation of Intuitionistic Arithmetic and Analysis. Lecture Notes in Mathematics, vol. 344. Springer, Berlin (1973) · Zbl 0275.02025 [16] van den Berg, B., Briseid, E., Safarik, P.: A functional interpretation for nonstandard arithmetic. Ann. Pure Appl. Log. 163(12), 1962-1994 (2012) · Zbl 1270.03121 · doi:10.1016/j.apal.2012.07.003 This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.