| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 10118848 | Annals of Pure and Applied Logic | 2005 | 22 Pages |
Abstract
A simple and complete proof of strong normalization for first-Â and second-order intuitionistic natural deduction including disjunction, first-order existence and permutative conversions is given. The paper follows the Tait-Girard approach via computability predicates (reducibility) and saturated sets. Strong normalization is first established for a set of conversions of a new kind, then deduced for the standard conversions. Difficulties arising for disjunction are resolved using a new logic where disjunction is restricted to atomic formulas.
Keywords
Related Topics
Physical Sciences and Engineering
Mathematics
Logic
Authors
Makoto Tatsuta, Grigori Mints,