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

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.
Epsilon substitution for $$\textit{ID}_1$$ ID 1 via cut-elimination.Henry Towsner - 2018 - Archive for Mathematical Logic 57 (5-6):497-531.
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.K. Schutte - 1974 - Journal of Symbolic Logic 39 (3):607-607.

Analytics

Added to PP
2009-01-28

Downloads
194 (#207,902)

6 months
39 (#219,083)

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