Switch to: References

Add citations

You must login to add citations.
  1. Gentzen’s “cut rule” and quantum measurement in terms of Hilbert arithmetic. Metaphor and understanding modeled formally.Vasil Penchev - 2022 - Logic and Philosophy of Mathematics eJournal 14 (14):1-37.
    Hilbert arithmetic in a wide sense, including Hilbert arithmetic in a narrow sense consisting by two dual and anti-isometric Peano arithmetics, on the one hand, and the qubit Hilbert space (originating for the standard separable complex Hilbert space of quantum mechanics), on the other hand, allows for an arithmetic version of Gentzen’s cut elimination and quantum measurement to be described uniformy as two processes occurring accordingly in those two branches. A philosophical reflection also justifying that unity by quantum neo-Pythagoreanism links (...)
    Download  
     
    Export citation  
     
    Bookmark  
  • A variant of the double-negation translation.Jeremy Avigad - manuscript
    An efficient variant of the double-negation translation explains the relationship between Shoenfield’s and G¨odel’s versions of the Dialectica interpretation.
    Download  
     
    Export citation  
     
    Bookmark   3 citations  
  • Forcing in proof theory.Jeremy Avigad - 2004 - Bulletin of Symbolic Logic 10 (3):305-333.
    Paul Cohen’s method of forcing, together with Saul Kripke’s related semantics for modal and intuitionistic logic, has had profound effects on a number of branches of mathematical logic, from set theory and model theory to constructive and categorical logic. Here, I argue that forcing also has a place in traditional Hilbert-style proof theory, where the goal is to formalize portions of ordinary mathematics in restricted axiomatic theories, and study those theories in constructive or syntactic terms. I will discuss the aspects (...)
    Download  
     
    Export citation  
     
    Bookmark   15 citations  
  • An ecumenical notion of entailment.Elaine Pimentel, Luiz Carlos Pereira & Valeria de Paiva - 2019 - Synthese 198 (S22):5391-5413.
    Much has been said about intuitionistic and classical logical systems since Gentzen’s seminal work. Recently, Prawitz and others have been discussing how to put together Gentzen’s systems for classical and intuitionistic logic in a single unified system. We call Prawitz’ proposal the Ecumenical System, following the terminology introduced by Pereira and Rodriguez. In this work we present an Ecumenical sequent calculus, as opposed to the original natural deduction version, and state some proof theoretical properties of the system. We reason that (...)
    Download  
     
    Export citation  
     
    Bookmark   7 citations  
  • Kripke models for classical logic.Danko Ilik, Gyesik Lee & Hugo Herbelin - 2010 - Annals of Pure and Applied Logic 161 (11):1367-1378.
    We introduce a notion of the Kripke model for classical logic for which we constructively prove the soundness and cut-free completeness. We discuss the novelty of the notion and its potential applications.
    Download  
     
    Export citation  
     
    Bookmark   3 citations  
  • (1 other version)Eliminating definitions and Skolem functions in first-order logic.Jeremy Avigad - manuscript
    From proofs in any classical first-order theory that proves the existence of at least two elements, one can eliminate definitions in polynomial time. From proofs in any classical first-order theory strong enough to code finite functions, including sequential theories, one can also eliminate Skolem functions in polynomial time.
    Download  
     
    Export citation  
     
    Bookmark   4 citations  
  • Saturated models of universal theories.Jeremy Avigad - 2002 - Annals of Pure and Applied Logic 118 (3):219-234.
    A notion called Herbrand saturation is shown to provide the model-theoretic analogue of a proof-theoretic method, Herbrand analysis, yielding uniform model-theoretic proofs of a number of important conservation theorems. A constructive, algebraic variation of the method is described, providing yet a third approach, which is finitary but retains the semantic flavor of the model-theoretic version.
    Download  
     
    Export citation  
     
    Bookmark   20 citations  
  • Algebraic aspects of cut elimination.Francesco Belardinelli, Peter Jipsen & Hiroakira Ono - 2004 - Studia Logica 77 (2):209 - 240.
    We will give here a purely algebraic proof of the cut elimination theorem for various sequent systems. Our basic idea is to introduce mathematical structures, called Gentzen structures, for a given sequent system without cut, and then to show the completeness of the sequent system without cut with respect to the class of algebras for the sequent system with cut, by using the quasi-completion of these Gentzen structures. It is shown that the quasi-completion is a generalization of the MacNeille completion. (...)
    Download  
     
    Export citation  
     
    Bookmark   22 citations  
  • Francesco Belardinelli Peter Jipsen.Hiroakira Ono - 2001 - Studia Logica 68:1-32.
    Download  
     
    Export citation  
     
    Bookmark