Cut-elimination for simple type theory with an axiom of choice

Journal of Symbolic Logic 64 (2):479-485 (1999)
  Copy   BIBTEX

Abstract

We present a cut-elimination proof for simple type theory with an axiom of choice formulated in the language with an epsilon-symbol. The proof is modeled after Takahashi's proof of cut-elimination for simple type theory with extensionality. The same proof works when types are restricted, for example for second-order classical logic with an axiom of choice.

Categories

Keywords

Reprint years

DOI

10.2307/2586480

Other Versions

No versions found

Links

PhilArchive

    This entry is not archived by us. If you are the author and have permission from the publisher, we recommend that you archive it. Many publishers automatically grant permission to authors to archive pre-prints. By uploading a copy of your work, you will enable us to better index it, making it easier to find.

    Upload a copy of this work     Papers currently archived: 106,951

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

Determinate logic and the Axiom of Choice.J. P. Aguilera - 2020 - Annals of Pure and Applied Logic 171 (2):102745.
A proof of the cut-elimination theorem in simple type theory.Satoko Titani - 1973 - Journal of Symbolic Logic 38 (2):215-226.
A Simple Proof that Super-Consistency Implies Cut Elimination.Gilles Dowek & Olivier Hermant - 2012 - Notre Dame Journal of Formal Logic 53 (4):439-456.
Proof normalization modulo.Gilles Dowek & Benjamin Werner - 2003 - Journal of Symbolic Logic 68 (4):1289-1316.
Cut elimination for a simple formulation of epsilon calculus.Grigori Mints - 2008 - Annals of Pure and Applied Logic 152 (1):148-160.
The Hauptsatz for Stratified Comprehension: A Semantic Proof.Marcel Crabbé - 1994 - Mathematical Logic Quarterly 40 (4):481-489.
Simple cut elimination proof for hybrid logic.Andrezj Indrzejczak - 2016 - Logic and Logical Philosophy 25 (2):129-141.
Simple cut elimination proof for hybrid logic.Andrzej Indrzejczak - 2016 - Logic and Logical Philosophy 25 (2):129-141.
Dag Prawitz. Hauptsatz for higher order logic. The journal of symbolic logic, Bd. 33 , S. 452–457. - Dag Prawitz. Completeness and Hauptsatz for second order logic. Theoria , Bd. 33 , S. 246–258. - Moto-o Takahashi. A proof of cut-elimination in simple type-theory. Journal of the Mathematical Society of Japan, Bd. 19 , S. 399–410. [REVIEW]K. Schutte - 1974 - Journal of Symbolic Logic 39 (3):607-607.
Epsilon substitution for ID1\textit{ID}_1 ID 1 via cut-elimination.Henry Towsner - 2018 - Archive for Mathematical Logic 57 (5-6):497-531.

Analytics

Added to PP
2009-01-28

Downloads
114 (#200,796)

6 months
15 (#217,951)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

The Higher-Order Prover LEO-II.Christoph Benzmüller, Nik Sultana, Lawrence C. Paulson & Frank Theiß - 2015 - Journal of Automated Reasoning 55 (4):389-404.
Cut-Elimination for Quantified Conditional Logic.Christoph Benzmüller - 2017 - Journal of Philosophical Logic 46 (3):333-353.

Add more citations

References found in this work

Proof Theory.Gaisi Takeuti - 1990 - Studia Logica 49 (1):160-161.

Add more references