Cut-Elimination for Simple Type Theory with An Axiom of Choice

Paper Info

Title
Cut-Elimination for Simple Type Theory with An Axiom of Choice

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.

Authors (1 rows)

Cited by (1 rows)

References (1 rows)

Name	Order	Citations	PageRank
Grigori Mints	1	235	72.76