Hostname: page-component-cd9895bd7-gvvz8 Total loading time: 0 Render date: 2024-12-29T07:02:26.196Z Has data issue: false hasContentIssue false
  • English
  • Français

Uniqueness of normal proofs of minimal formulas

Published online by Cambridge University Press:  12 March 2014

Makoto Tatsuta
Makoto Tatsuta*
Affiliation:
Research Institute of Electrical Communication, Tohoku University, 2-1-1 Katahira, Sendai 980, Japan, E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

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 β-normal proof of a minimal formula of depth 2 is unique in NJ. (2) There exists a minimal formula of depth 3 whose βη-normal proof is not unique in NJ. (3) There exists a minimal formula of depth 3 whose βη-normal proof is not unique in NK.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 58 , Issue 3 , September 1993 , pp. 789 - 799
Copyright
Copyright © Association for Symbolic Logic 1993

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[1]Barendregt, H. P., The lambda calculus: Its syntax and semantics, North-Holland, Amsterdam, 1984.Google Scholar
[2]Hindley, J. R. and Seldin, J. P., Introduction to combinators and λ-calculus, Cambridge University Press, Cambridge, 1986.Google Scholar
[3]Hirokawa, S., Principal types of BCK-lambda terms, Theoretical Computer Science, vol. 107(1993), pp. 253–276.CrossRefGoogle Scholar
[4]Howard, W. A., The formulae-as-types notion of construction, To H. B. Curry: Essays on combinatory logic, lambda calculus and formalism, Academic Press, London, 1980.Google Scholar
[5]Komori, Y., BCK algebras and lambda calculus, Proceedings of the 10th symposium on semigroups, Josai University, Sakado, 1987, pp. 5–11.Google Scholar
[6]Komori, Y. and Hirokawa, S., The number of proofs for a BCK-formula, this Journal, vol. 58 (1993), pp. 626–628.Google Scholar
[7]Solov’ev, S. V., Preservation of equivalence of derivations under reduction of depth of formulas, Zapiski Nauchnykh Seminarov Leningradskogo Otdeleniya matematicheskogo Instituta im. V. A. Steklova AN SSSR, vol. 88 (1979), pp. 197–207; English translation, Journal of Soviet Mathematics, vol. 20 (1982), pp. 2370–2376.Google Scholar
[8]Troelstra, A., Metamathematical investigation of intuitionistic arithmetic and analysis, Lecture Notes in Mathematics, vol. 344, Springer-Verlag, Berlin and New York, 1973.CrossRefGoogle Scholar