Abstract.
Carrying out a suggestion by Kreisel, we adapt Gödel’s functional interpretation to ordinary first-order predicate logic(PL) and thus devise an algorithm to extract Herbrand terms from PL-proofs. The extraction is carried out in an extension of PL to higher types. The algorithm consists of two main steps: first we extract a functional realizer, next we compute the β-normal-form of the realizer from which the Herbrand terms can be read off. Even though the extraction is carried out in the extended language, the terms are ordinary PL-terms. In contrast to approaches to Herbrand’s theorem based on cut elimination orɛ-elimination this extraction technique is, except for the normalization step, of low polynomial complexity, fully modular and furthermore allows an analysis of the structure of the Herbrand terms, in the spirit of Kreisel ([13]), already prior to the normalization step. It is expected that the implementation of functional interpretation in Schwichtenberg’s MINLOG system can be adapted to yield an efficient Herbrand-term extraction tool.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
Beckmann, A.: Exact bounds for lengths of reductions in typed λ-calculus. J. Symbolic Logic 66, 1277–1285 (2001)
Berger, U., Schwichtenberg, H.: An inverse of the evaluation functional for typed lambda-calculus. In: R. Vemuri (ed.), Proceedings of the 6. Annual IEEE Symposium on Logic in Computer Sciences(LICS), IEEE Press Los Alamitos, Los Alamitos, 1991, pp. 203–211
Buss, S.R.: An Introduction to Proof Theory. In: S.R. Buss (ed.), Handbook of Proof Theory, Elsevier Science B.V., 1998, pp. 2–78
Diller, J.: Logical problems of functional interpretations. Annals of Pure and Applied Logic 114, 27–42 (2002)
Diller, J., Nahm, W.: Eine Variante zur Dialectica-Interpretation der Heyting- Arithmetik Endlicher Typen. Arch. Math. Logik 16, 49–66 (1974)
Gerhardy, P.: Improved Complexity Analysis of Cut Elimination and Herbrand’s Theorem. Master’s thesis, Aarhus, 2003
Gerhardy, P.: Refined Complexity Analysis of Cut Elimination. In: M. Baaz, J. Makovsky, Proceedings of the 17th International Workshop CSL 2003, Volume 2803 of LNCS, Springer-Verlag, Berlin, 2003, pp. 212–225
Gödel, K.: Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes. Dialectica, 12, 280–287 (1958)
Hernest, M.-D.: A comparison between two techniques of program extraction from classical proofs. In: M. Baaz, J. Makobsky, A. Voronkov (eds.), LPAR 2002: Short Contributions and CSL 2003: Extended Posters, volume VIII Kurt Gödel Society’s Collegium Logicum, Springer-Verlag, Berlin, 2004, pp. 99–102
Hernest, M.-D., Kohlenbach, U.: A Complexity Analysis of Functional Interpretations. To appear in: Theoretical Computer Science
Kohlenbach, U.: A note on Spector’s quantifier-free rule of extensionality. Arch. Math. Logic 40, 89–92 (2001)
Kreisel, G.: Review of [20]. in Mathematical Reviews 1967. 37 #1224
Kreisel, G.: Finiteness Theorems in Arithmetic: An Application of Herbrand’s Theorem for Σ2-formulas. In: J. Stern (eds.), Logic Colloquium ‘81, North-Holland Publishing Company, 1982, pp. 39–55
Luckhardt, H.: Herbrand-Analysen zweier Beweise des Satzes von Roth: Polynomiale Anzahlsschranken. J. Symbolic Logic 54, 234–263 (1989)
Orevkov, V.P.: Lower bounds on the increase in complexity of deductions in cut elimination. Zap. Nauchn. Sem. Leningrad. Otdel. Mat. Inst. Steklov 88, 137–162 (1979); English transl. J. Soviet Math. 20 (4), 1982
Orevkov, V.P.: Complexity of Proofs and Their Transformations in Axiomatic Theories, volume 128 of Translations of Mathematical Monographs. AMS Providence R.I., 1993
Pudlak, P.: The Length of Proofs. In: S.R. Buss (ed.), Handbook of Proof Theory, Elsevier Science B.V., 1998, pp. 548–637
Schwichtenberg, H.: Complexity of normalization in the pure typed lambda-calculus. In: A. Troelstra, D. van Dalen, The L.E.J. Brouwer Centenary Symposium, North-Holland Publishing Company, 1982, pp. 453–457
Schwichtenberg, H.: An upper bound for reduction sequences in the typed λ-calculus. Arch. Math. Logic 30, 405–408 (1991)
Shoenfield, J.R.: Mathematical Logic. Addison-Wesley, Reading, Mass., 1967
Spector, C.: Provably recursive functionals of analysis : a consistency proof of analysis by an extension of principles formulated in current intuitionistic mathematics. In: J. Dekker (ed.), Proceedings of Symposia in Pure Mathematics, Vol 5, AMS, Providence, R.I., 1962, pp. 1–27
Statman, R.: Lower Bounds on Herbrand’s Theorem. Proc. Am. Math. Soc. 75, 104–107 (1979)
Troelstra, A.S. (ed.): Metamathematical investigation of intuitionistic arithmetic and analysis, volume 344 of Springer LNM. Springer-Verlag, Berlin, 1973
Zhang, W.: Cut elimination and automatic proof procedures. Theoretical Computer Science 91, 265–284 (1991)
Zhang, W.: Depth of proofs, depth of cut-formulas and complexity of cut formulas. Theoretical Computer Science 129, 193–206 (1994)
Author information
Authors and Affiliations
Additional information
BRICS, Basic Research in Computer Science, funded by the Danish National Research Foundation
Ulrich Kohlenbach’s research was partially supported by the Danish National Research Council, Grant no. 21-02-0474.
Rights and permissions
About this article
Cite this article
Gerhardy, P., Kohlenbach, U. Extracting Herbrand disjunctions by functional interpretation. Arch. Math. Logic 44, 633–644 (2005). https://doi.org/10.1007/s00153-005-0275-1
Received:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00153-005-0275-1