×

A herbrandized functional interpretation of classical first-order logic. (English) Zbl 1417.03290

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.

MSC:

03F10 Functionals in proof theory
03B10 Classical first-order logic
03B40 Combinatory logic and lambda calculus
03B15 Higher-order logic; type theory (MSC2010)
PDFBibTeX XMLCite
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.