The proofs of α → α in P – W

DOI10.2307/2275604MaRDI QIDQ4879907zbMATH OpenOpenAlexFDO

Authors 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

zbMATH Keywords

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

Mathematics Subject Classification ID

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

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

Cites work

• BCK-combinators and linear \(\lambda\)-terms have types
• Characterization of normal forms possessing inverse in the - --calculus
• Combinatory abstraction using \({\mathbf B}\), \({\mathbf B}^ \prime\) and friends
• 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)