Uniqueness of Normal Proofs of Minimal Formulas
Tatsuta, Makoto
J. Symbolic Logic, Tome 58 (1993) no. 1, p. 789-799 / Harvested from Project Euclid
A minimal formula is a formula which is minimal in provable formulas with respect to the substitution relation. This paper shows the following: (1) A $\beta$-normal proof of a minimal formula of depth 2 is unique in $\mathbf{NJ}$. (2) There exists a minimal formula of depth 3 whose $\beta\eta$-normal proof is not unique in $\mathbf{NJ}$. (3) There exists a minimal formula of depth 3 whose $\beta\eta$-normal proof is not unique in $\mathbf{NK}$.
Publié le : 1993-09-14
Classification: 
@article{1183744298,
     author = {Tatsuta, Makoto},
     title = {Uniqueness of Normal Proofs of Minimal Formulas},
     journal = {J. Symbolic Logic},
     volume = {58},
     number = {1},
     year = {1993},
     pages = { 789-799},
     language = {en},
     url = {http://dml.mathdoc.fr/item/1183744298}
}
Tatsuta, Makoto. Uniqueness of Normal Proofs of Minimal Formulas. J. Symbolic Logic, Tome 58 (1993) no. 1, pp.  789-799. http://gdmltest.u-ga.fr/item/1183744298/