|Abstract||Algebraic proofs of the cut-elimination theorems for classical and intuitionistic logic are presented, and are used to show how one can sometimes extract a constructive proof and an algorithm from a proof that is nonconstructive. A variation of the double-negation translation is also discussed: if ϕ is provable classically, then ¬(¬ϕ)nf is provable in minimal logic, where θnf denotes the negation-normal form of θ. The translation is used to show that cut-elimination theorems for classical logic can be viewed as special cases of the cut-elimination theorems for intuitionistic logic.|
|Keywords||No keywords specified (fix it)|
|Through your library||Only published papers are available at libraries|
Similar books and articles
Henry Africk (1992). Classical Logic, Intuitionistic Logic, and the Peirce Rule. Notre Dame Journal of Formal Logic 33 (2):229-235.
George Tourlakis (2010). On the Proof-Theory of Two Formalisations of Modal First-Order Logic. Studia Logica 96 (3):349-373.
Grigori Mints (2012). Effective Cut-Elimination for a Fragment of Modal Mu-Calculus. Studia Logica 100 (1-2):279-287.
J. W. Degen (1999). Complete Infinitary Type Logics. Studia Logica 63 (1):85-119.
G. Mints (1999). Cut-Elimination for Simple Type Theory with an Axiom of Choice. Journal of Symbolic Logic 64 (2):479-485.
Rajeev Gore, Linda Postniece & Alwen Tiu, Cut-Elimination and Proof-Search for Bi-Intuitionistic Logic Using Nested Sequents.
Gilles Dowek & Benjamin Werner (2003). Proof Normalization Modulo. Journal of Symbolic Logic 68 (4):1289-1316.
Francesco Belardinelli, Peter Jipsen & Hiroakira Ono (2004). Algebraic Aspects of Cut Elimination. Studia Logica 77 (2):209 - 240.
Roy Dyckhoff & Luis Pinto (1998). Cut-Elimination and a Permutation-Free Sequent Calculus for Intuitionistic Logic. Studia Logica 60 (1):107-118.
Added to index2009-01-28
Total downloads9 ( #114,230 of 549,754 )
Recent downloads (6 months)1 ( #63,425 of 549,754 )
How can I increase my downloads?