A lambda proof of the P-W theorem

Sachio Hirokawa, Yuichi Komori, Misao Nagayama

Research output: Contribution to journalArticle

Abstract

The logical system P-W is an implicational non-commutative intuitionistic logic defined 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 λx.x. Here the HRML λ-terms correspond, via the Curry-Howard isomorphism, to the P-W proofs in natural deduction style.

Original languageEnglish
Pages (from-to)1841-1849
Number of pages9
JournalJournal of Symbolic Logic
Volume65
Issue number4
DOIs
Publication statusPublished - Jan 1 2000

Fingerprint

Theorem
Natural Deduction
P Systems
Intuitionistic Logic
Term
Axiom
Substitution
Isomorphism
Corollary
Calculus
Closed
Style
Calculi
Logic
Modus Ponens

All Science Journal Classification (ASJC) codes

  • Philosophy
  • Logic

Cite this

A lambda proof of the P-W theorem. / Hirokawa, Sachio; Komori, Yuichi; Nagayama, Misao.

In: Journal of Symbolic Logic, Vol. 65, No. 4, 01.01.2000, p. 1841-1849.

Research output: Contribution to journalArticle

Hirokawa, S, Komori, Y & Nagayama, M 2000, 'A lambda proof of the P-W theorem', Journal of Symbolic Logic, vol. 65, no. 4, pp. 1841-1849. https://doi.org/10.2307/2695080
Hirokawa, Sachio ; Komori, Yuichi ; Nagayama, Misao. / A lambda proof of the P-W theorem. In: Journal of Symbolic Logic. 2000 ; Vol. 65, No. 4. pp. 1841-1849.
@article{7dcda9bd2bb5436893d0ef6b7f7b6bc8,
title = "A lambda proof of the P-W theorem",
abstract = "The logical system P-W is an implicational non-commutative intuitionistic logic defined 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 λx.x. Here the HRML λ-terms correspond, via the Curry-Howard isomorphism, to the P-W proofs in natural deduction style.",
author = "Sachio Hirokawa and Yuichi Komori and Misao Nagayama",
year = "2000",
month = "1",
day = "1",
doi = "10.2307/2695080",
language = "English",
volume = "65",
pages = "1841--1849",
journal = "Journal of Symbolic Logic",
issn = "0022-4812",
publisher = "Association for Symbolic Logic",
number = "4",

}

TY - JOUR

T1 - A lambda proof of the P-W theorem

AU - Hirokawa, Sachio

AU - Komori, Yuichi

AU - Nagayama, Misao

PY - 2000/1/1

Y1 - 2000/1/1

N2 - The logical system P-W is an implicational non-commutative intuitionistic logic defined 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 λx.x. Here the HRML λ-terms correspond, via the Curry-Howard isomorphism, to the P-W proofs in natural deduction style.

AB - The logical system P-W is an implicational non-commutative intuitionistic logic defined 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 λx.x. Here the HRML λ-terms correspond, via the Curry-Howard isomorphism, to the P-W proofs in natural deduction style.

UR - http://www.scopus.com/inward/record.url?scp=0034561959&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0034561959&partnerID=8YFLogxK

U2 - 10.2307/2695080

DO - 10.2307/2695080

M3 - Article

VL - 65

SP - 1841

EP - 1849

JO - Journal of Symbolic Logic

JF - Journal of Symbolic Logic

SN - 0022-4812

IS - 4

ER -