|
Descripción
|
|
|---|---|
| We give a fully constructive semantic proof of cut elimination for intuitionistic type theory with axioms. The problem here, as with the original Takeuti conjecture, is that the impredicativity of the formal system involved makes it impossible to define a semantics along conventional lines, in the absence, a priori, of cut, or to prove completeness by induction on subformula structure. In addition, unlike semantic proofs by Tait, Takahashi, and Andrews of variants of the Takeuti conjecture, our arguments are constructive. Our techniques offer also an easier approach than Girard’s strong normalization techniques to the problem of extending the cut-elimination result in the presence of axioms. We need only to relativize the Heyting algebras involved in a straightforward way. | |
|
Internacional
|
Si |
|
Nombre congreso
|
22nd International Workshop, CSL 2008. |
|
Tipo de participación
|
960 |
|
Lugar del congreso
|
|
|
Revisores
|
No |
|
ISBN o ISSN
|
978-3-540-87530-7 |
|
DOI
|
10.1007/978-3-540-87531-4 |
|
Fecha inicio congreso
|
16/09/2008 |
|
Fecha fin congreso
|
19/09/2008 |
|
Desde la página
|
169 |
|
Hasta la página
|
183 |
|
Título de las actas
|
22nd International Workshop, CSL 2008, 17th Annual Conference of the EACSL, Bertinoro, Italy, September 16-19, 2008. Proceedings. |