A lambda proof of the P-W theorem

DOI10.2307/2695080zbMath0970.03019OpenAlexW1975531498MaRDI QIDQ2710612

Misao Nagayama, Sachio Hirokawa, Yuichi Komori

Publication date: 21 October 2001

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

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

zbMATH Keywords

intuitionistic logicsimply typed \(\lambda\)-calculusP-W problem

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Combinatory logic and lambda calculus (03B40)

Cites Work

• Characterization of normal forms possessing inverse in the \(\lambda\)- \(\beta\)-\(\eta\)-calculus
• Syntactical investigations into \(BI\) logic and \(BB^ \prime I\) logic
• Combinatory abstraction using \({\mathbf B}\), \({\mathbf B}^ \prime\) and friends
• A Constructive Proof of a Theorem in Relevance Logic
• On Entailment

This page was built for publication: A lambda proof of the P-W theorem