Hostname: page-component-cd9895bd7-q99xh Total loading time: 0 Render date: 2024-12-21T08:02:48.606Z Has data issue: false hasContentIssue false
  • English
  • Français

A lambda proof of the P-W theorem

Published online by Cambridge University Press:  12 March 2014

Sachio Hirokawa ,
Yuichi Komori  and
Misao Nagayama
Sachio Hirokawa
Affiliation:
Computer Center, Kyushu University, Hakozaki 6-10-1, Fukuoka 812-8581, Japan, E-mail:hirokawa@cc.kyushu-u.ac.jp
Yuichi Komori
Affiliation:
Department of Mathematics, Faculty of Science, Chiba University, Yayoi-Cho 1-33, Inage-Ku. CHIBA 263-8522, Japan, E-mail:komori@math.s.chiba-u.ac.jp
Misao Nagayama
Affiliation:
Department of Mathematics, Tokyo Woman's Christian University, Zempuku-JI 2-6-1, Suginami, Tokyo 167-8585, Japan, E-mail:misao@twcu.ac.jp
Get access Rights & Permissions [Opens in a new window]

Abstract

The logical system P-W is an implicational non-commutative intuitionistic logic denned by axiom schemes B − (b → c) → (a → b) → a → c. B′ = (a → b) → (b → c) → a → c. I - a → a with the rules of modus ponens and substitution. The P-W problem is a problem asking whether α - β holds if α → β and β → α are both provable in P-W. The answer is affirmative. The first to prove this was E. P. Martin by a semantical method.

In this paper, we give the first proof of Martin's theorem based on the theory of simply typed λ-calculus. This proof is obtained as a corollary to the main theorem of this paper, shown without using Martin's Theorem, that any closed hereditary right-maximal linear (HRML) λ-term of type α → α is βη-reducible to λxx. Here the HRML λ-terms correspond, via the Curry-Howard isomorphism, to the P-W proofs in natural deduction style.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 65 , Issue 4 , December 2000 , pp. 1841 - 1849
Copyright
Copyright © Association for Symbolic Logic 2000

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]Anderson, A. R. and Belnap, N. D. Jr., Entailment, vol. 1, Princeton University Press, Princeton. N.J., 1975.Google Scholar
[2]Barendregt, H., The lambda calculus, second ed., North-Holland, Amsterdam, 1984.Google Scholar
[3]Dezani-Ciancaglini, M., Characterization of normal forms possessing inverse in the λ-β-η calculus, Theoretical Computer Science, vol. 2 (1976), pp. 323–337.CrossRefGoogle Scholar
[4]Fine, K. and Martin, E. P., Progressive logic — the conjunction case, manuscript. October 13, 1994.Google Scholar
[5]Hirokawa, S., The proof of α → a in P-W, this Journal, vol. 61 (1996), pp. 195–221.Google Scholar
[6]Komori, Y., Syntactic investigations into BI logic and BB′I Logic, Studia Logica, vol. 53 (1994), pp. 397–416.CrossRefGoogle Scholar
[7]Kron, A., A constructive proof of a theorem in relevant logic, Zeitschrift fÜr Mathematische Logik und Grundlagen der Mathematik, vol. 31 (1985), pp. 423–430.CrossRefGoogle Scholar
[8]Martin, E. P. and Meyer, R. K., Solution to the P-W problem, this Journal, vol. 47 (1982), pp. 867–887.Google Scholar
[9]Nagayama, M., Normalization theorem for P-W, Bulletin of the Section of Logic, vol. 28 (1999), pp. 83–85.Google Scholar
[10]Powers, L., On P-W, The Relevance Logic Newsletter, vol. 1 (1976), pp. 131–142.Google Scholar
[11]Trigg, P., Hindley, J. R., and Bunder, M. W., Combinatory abstraction using B, B′ and friends, Theoretical Computer Science, vol. 135 (1994), pp. 405–422.CrossRefGoogle Scholar