Switch to: Citations

Add references

You must login to add references.
  1. Epsilon theorems in intermediate logics.Matthias Baaz & Richard Zach - 2022 - Journal of Symbolic Logic 87 (2):682-720.
    Any intermediate propositional logic can be extended to a calculus with epsilon- and tau-operators and critical formulas. For classical logic, this results in Hilbert’s $\varepsilon $ -calculus. The first and second $\varepsilon $ -theorems for classical logic establish conservativity of the $\varepsilon $ -calculus over its classical base logic. It is well known that the second $\varepsilon $ -theorem fails for the intuitionistic $\varepsilon $ -calculus, as prenexation is impossible. The paper investigates the effect of adding critical $\varepsilon $ - (...)
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  • Chapter 1: An introduction to proof theory & Chapter 2: Firstorder proof theory of arithmetic.S. Buss - 1998 - In Samuel R. Buss (ed.), Handbook of proof theory. New York: Elsevier.
    Download  
     
    Export citation  
     
    Bookmark   35 citations  
  • Unsound inferences make proofs shorter.Juan P. Aguilera & Matthias Baaz - 2019 - Journal of Symbolic Logic 84 (1):102-122.
    We give examples of calculi that extend Gentzen’s sequent calculusLKby unsound quantifier inferences in such a way that derivations lead only to true sequents, and proofs therein are nonelementarily shorter thanLK-proofs.
    Download  
     
    Export citation  
     
    Bookmark   9 citations  
  • The number of proof lines and the size of proofs in first order logic.Jan Krajíček & Pavel Pudlák - 1988 - Archive for Mathematical Logic 27 (1):69-84.
    Download  
     
    Export citation  
     
    Bookmark   21 citations  
  • Exact bounds on epsilon processes.Toshiyasu Arai - 2011 - Archive for Mathematical Logic 50 (3-4):445-458.
    In this paper we show that the lengths of the approximating processes in epsilon substitution method are calculable by ordinal recursions in an optimal way.
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • (1 other version)The logic of choice.Andreas Blass & Yuri Gurevich - 2000 - Journal of Symbolic Logic 65 (3):1264-1310.
    The choice construct (choose x: φ(x)) is useful in software specifications. We study extensions of first-order logic with the choice construct. We prove some results about Hilbert's ε operator, but in the main part of the paper we consider the case when all choices are independent.
    Download  
     
    Export citation  
     
    Bookmark   8 citations  
  • Proof Theory.Gaisi Takeuti - 1990 - Studia Logica 49 (1):160-161.
    Download  
     
    Export citation  
     
    Bookmark   166 citations  
  • (1 other version)Intuitionistic ε- and τ-calculi.David Devidi - 1995 - Mathematical Logic Quarterly 41 (4):523-546.
    There are several open problems in the study of the calculi which result from adding either of Hilbert's ϵ- or τ-operators to the first order intuitionistic predicate calculus. This paper provides answers to several of them. In particular, the first complete and sound semantics for these calculi are presented, in both a “quasi-extensional” version which uses choice functions in a straightforward way to interpret the ϵ- or τ-terms, and in a form which does not require extensionality assumptions. Unlike the classical (...)
    Download  
     
    Export citation  
     
    Bookmark   8 citations  
  • The Epsilon Calculus and Herbrand Complexity.Georg Moser & Richard Zach - 2006 - Studia Logica 82 (1):133-155.
    Hilbert's ε-calculus is based on an extension of the language of predicate logic by a term-forming operator εx. Two fundamental results about the ε-calculus, the first and second epsilon theorem, play a rôle similar to that which the cut-elimination theorem plays in sequent calculus. In particular, Herbrand's Theorem is a consequence of the epsilon theorems. The paper investigates the epsilon theorems and the complexity of the elimination procedure underlying their proof, as well as the length of Herbrand disjunctions of existential (...)
    Download  
     
    Export citation  
     
    Bookmark   14 citations  
  • (1 other version)Cut Elimination in ε‐Calculi.Mitsuru Yasuhara - 1982 - Mathematical Logic Quarterly 28 (20‐21):311-316.
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  • (1 other version)Cut Elimination in ε‐Calculi.Mitsuru Yasuhara - 1982 - Mathematical Logic Quarterly 28 (20-21):311-316.
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  • (1 other version)Theorie der Logischen Auswahlfunktionen.Günter Asser - 1957 - Mathematical Logic Quarterly 3 (1‐5):30-68.
    Download  
     
    Export citation  
     
    Bookmark   14 citations  
  • (1 other version)Theorie der Logischen Auswahlfunktionen.Günter Asser - 1957 - Mathematical Logic Quarterly 3 (1-5):30-68.
    Download  
     
    Export citation  
     
    Bookmark   13 citations  
  • Ackermann’s substitution method.Georg Moser - 2006 - Annals of Pure and Applied Logic 142 (1):1-18.
    We aim at a conceptually clear and technically smooth investigation of Ackermann’s substitution method [W. Ackermann, Zur Widerspruchsfreiheit der Zahlentheorie, Math. Ann. 117 162–194]. Our analysis provides a direct classification of the provably recursive functions of , i.e. Peano Arithmetic framed in the ε-calculus.
    Download  
     
    Export citation  
     
    Bookmark   6 citations  
  • The substitution method.W. W. Tait - 1965 - Journal of Symbolic Logic 30 (2):175-192.
    Download  
     
    Export citation  
     
    Bookmark   15 citations  
  • Lower Bounds to the size of constant-depth propositional proofs.Jan Krajíček - 1994 - Journal of Symbolic Logic 59 (1):73-86.
    LK is a natural modification of Gentzen sequent calculus for propositional logic with connectives ¬ and $\bigwedge, \bigvee$. Then for every d ≥ 0 and n ≥ 2, there is a set Td n of depth d sequents of total size O which are refutable in LK by depth d + 1 proof of size exp) but such that every depth d refutation must have the size at least exp). The sets Td n express a weaker form of the pigeonhole (...)
    Download  
     
    Export citation  
     
    Bookmark   21 citations  
  • Extracting Herbrand disjunctions by functional interpretation.Philipp Gerhardy & Ulrich Kohlenbach - 2005 - Archive for Mathematical Logic 44 (5):633-644.
    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, (...)
    Download  
     
    Export citation  
     
    Bookmark   7 citations