Cut-Elimination for Simple Type Theory with an Axiom of Choice Export

@article{citeulike:1743029, 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.}, author = {Mints, G.}, citeulike-article-id = {1743029}, citeulike-linkout-0 = {http://www.jstor.org/stable/2586480}, journal = {The Journal of Symbolic Logic}, keywords = {epsilon, proof\_theory, sequent\_calculus, type\_theory}, number = {2}, pages = {479--485}, posted-at = {2007-10-08 19:39:11}, priority = {4}, title = {Cut-Elimination for Simple Type Theory with an Axiom of Choice}, url = {http://www.jstor.org/stable/2586480}, volume = {64}, year = {1999} }

TY - JOUR ID - citeulike:1743029 L3 - citeulike-article-id:1743029 N2 - 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. IS - 2 JF - The Journal of Symbolic Logic EP - 485 TI - Cut-Elimination for Simple Type Theory with an Axiom of Choice VL - 64 SP - 479 KW - epsilon KW - proof_theory KW - sequent_calculus KW - type_theory AU - Mints, G PY - 1999/// UR - http://www.jstor.org/stable/2586480 ER -