Ein Syntaktischer Beweis für die Zulässigkeit der Schnittregel im Kalkül von Schütte für die Intuitionistische Typenlogik |
| |
Authors: | Horst Osswald |
| |
Institution: | (1) Mathematisches Institut der Universität München, Theresienstraße 39, 8 München 2 |
| |
Abstract: | In 1] Girard gives a procedure, by which all derivations in the calculus of natural deductions of Prawitz 4] are transformed into normal derivations. Exploiting his idea we give a syntactical proof of the admissibility of the cut rule in Schütte's formal system of intuitionistic type theory. We obtain a normal form theorem but not a normalization theorem. Our Berechnungsprädikate are different from the candidats de reductibilite of Girard. In the case of second order logic Berechnungsprädikate für Terme t(O) are not defined for derivations ending with rO e t(O) which are normalizable, but for finite formula sets with the property, that ![Gamma](/content/l777484888n91173/xxlarge915.gif) rO e t(O) is derivable without cut. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|