The proofs of α → α in P – W

DOI10.2307/2275604zbMATH Open0853.03002OpenAlexW2579272254MaRDI QIDQ4879907FDOQ4879907

Sachio Hirokawa

Publication date: 2 June 1996

Published in: Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.2307/2275604

Recommendations

• A lambda proof of the P-W theorem
• Types of I-free hereditary right maximal terms
• Lambda terms definable as combinators
• Proof-finding algorithms for classical and subclassical propositional logics

zbMATH Keywords

\(P - W\) problemhereditary right maximal linear lambda termsimplicational logic \(P - W\)natural deduction-style proofs

Mathematics Subject Classification ID

Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Combinatory logic and lambda calculus (03B40)

Cites Work

• Combinatory abstraction using \({\mathbf B}\), \({\mathbf B}^ \prime\) and friends
• Characterization of normal forms possessing inverse in the \(\lambda\)- \(\beta\)-\(\eta\)-calculus
• BCK-combinators and linear \(\lambda\)-terms have types
• On Entailment

Cited In (2)

• Lambda terms definable as combinators
• A lambda proof of the P-W theorem

This page was built for publication: The proofs of α → α in P – W

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4879907)