A herbrandized functional interpretation of classical first-order logic

Archive for Mathematical Logic 56 (5-6):523-539 (2017)
  Copy   BIBTEX

Abstract

We introduce a new typed combinatory calculus with a type constructor that, to each type σ\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\sigma $$\end{document}, associates the star type σ∗\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\sigma ^*$$\end{document} of the nonempty finite subsets of elements of type σ\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\sigma $$\end{document}. 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.

Other Versions

No versions found

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 98,353

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Hard Provability Logics.Mojtaba Mojtahedi - 2021 - In Mojtaba Mojtahedi, Shahid Rahman & MohammadSaleh Zarepour (eds.), Mathematics, Logic, and their Philosophies: Essays in Honour of Mohammad Ardeshir. Springer. pp. 253-312.
Minimal elementary end extensions.James H. Schmerl - 2017 - Archive for Mathematical Logic 56 (5-6):541-553.

Analytics

Added to PP
2017-08-04

Downloads
21 (#871,918)

6 months
2 (#1,688,548)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Citations of this work

Herbrand's theorem as higher order recursion.Bahareh Afshari, Stefan Hetzl & Graham E. Leigh - 2020 - Annals of Pure and Applied Logic 171 (6):102792.
Herbrandized modified realizability.Gilda Ferreira & Paulo Firmino - 2024 - Archive for Mathematical Logic 63 (5):703-721.
A parametrised functional interpretation of Heyting arithmetic.Bruno Dinis & Paulo Oliva - 2021 - Annals of Pure and Applied Logic 172 (4):102940.
On Extracting Variable Herbrand Disjunctions.Andrei Sipoş - 2022 - Studia Logica 110 (4):1115-1134.

Add more citations

References found in this work

Basic proof theory.A. S. Troelstra - 2000 - New York: Cambridge University Press. Edited by Helmut Schwichtenberg.
Intensional interpretations of functionals of finite type I.W. W. Tait - 1967 - Journal of Symbolic Logic 32 (2):198-212.
Bounded functional interpretation.Fernando Ferreira & Paulo Oliva - 2005 - Annals of Pure and Applied Logic 135 (1):73-112.

View all 12 references / Add more references