Cut-Elimination for Simple Type Theory with an Axiom of Choice
Mints, G.
J. Symbolic Logic, Tome 64 (1999) no. 1, p. 479-485 / Harvested from Project Euclid
Text on Project Euclid
PDF
Alt PDF
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.
Publié le : 1999-06-14
Classification:  
@article{1183745789,
     author = {Mints, G.},
     title = {Cut-Elimination for Simple Type Theory with an Axiom of Choice},
     journal = {J. Symbolic Logic},
     volume = {64},
     number = {1},
     year = {1999},
     pages = { 479-485},
     language = {en},
     url = {http://dml.mathdoc.fr/item/1183745789}
}

Mints, G. Cut-Elimination for Simple Type Theory with an Axiom of Choice. J. Symbolic Logic, Tome 64 (1999) no. 1, pp.  479-485. http://gdmltest.u-ga.fr/item/1183745789/