Cut elimination for a simple formulation of epsilon calculus

Annals of Pure and Applied Logic 152 (1):148-160 (2008)
  Copy   BIBTEX

Abstract

A simple cut elimination proof for arithmetic with the epsilon symbol is used to establish the termination of a modified epsilon substitution process. This opens a possibility of extension to much stronger systems.

Categories

Keywords

Reprint years

DOI

10.1016/j.apal.2007.11.008

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 92,168

External links

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

Through your library

My notes

Similar books and articles

Epsilon substitution for transfinite induction.Henry Towsner - 2005 - Archive for Mathematical Logic 44 (4):397-412.
Effective Cut-elimination for a Fragment of Modal mu-calculus.Grigori Mints - 2012 - Studia Logica 100 (1-2):279-287.
Cut-elimination for simple type theory with an axiom of choice.G. Mints - 1999 - Journal of Symbolic Logic 64 (2):479-485.
Definite descriptions: Language, logic, and elimination.Norbert Gratzl - 2009 - In Hieke Alexander & Leitgeb Hannes (eds.), Reduction, Abstraction, Analysis. Ontos Verlag. pp. 355.
Cut elimination for a calculus with context-dependent rules.Birgit Elbl - 2001 - Archive for Mathematical Logic 40 (3):167-188.
A propositional fragment of Le'sniewski's Ontology and its formulation by the tableau method.Arata Ishimoto & M. Kobayashi - 1982 - Studia Logica 41 (2/3):181-195.
Epsilon substitution method for theories of jump hierarchies.Toshiyasu Arai - 2002 - Archive for Mathematical Logic 41 (2):123-153.
A Simple Proof that Super-Consistency Implies Cut Elimination.Gilles Dowek & Olivier Hermant - 2012 - Notre Dame Journal of Formal Logic 53 (4):439-456.
Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents.Rajeev Goré, Linda Postniece & Alwen Tiu - 1998 - In Marcus Kracht, Maarten de Rijke, Heinrich Wansing & Michael Zakharyaschev (eds.), Advances in Modal Logic. CSLI Publications. pp. 43-66.
A cut-free Gentzen formulation of basic propositional calculus.Kentaro Kikuchi & Katsumi Sasaki - 2003 - Journal of Logic, Language and Information 12 (2):213-225.
Cut-elimination and a permutation-free sequent calculus for intuitionistic logic.Roy Dyckhoff & Luis Pinto - 1998 - Studia Logica 60 (1):107-118.
A Simple Proof of Completeness and Cut-elimination for Propositional G¨ odel Logic.Arnon Avron - unknown

Analytics

Added to PP
2013-12-26

Downloads
37 (#432,736)

6 months
17 (#150,073)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

In memoriam: Grigori E. Mints 1939–2014.Solomon Feferman & Vladimir Lifschitz - 2015 - Bulletin of Symbolic Logic 21 (1):31-33.

View all 6 citations / Add more citations

References found in this work

Notation systems for infinitary derivations.Wilfried Buchholz - 1991 - Archive for Mathematical Logic 30 (5-6):277-296.
Zur Widerspruchsfreiheit der Zahlentheorie.Wilhelm Ackermann - 1940 - Journal of Symbolic Logic 5 (3):125-127.
Epsilon substitution method for ID1.Toshiyasu Arai - 2003 - Annals of Pure and Applied Logic 121 (2-3):163-208.
Epsilon substitution method for theories of jump hierarchies.Toshiyasu Arai - 2002 - Archive for Mathematical Logic 41 (2):123-153.

View all 7 references / Add more references