A lambda proof of the P-W theorem

DOI10.2307/2695080MaRDI QIDQ2710612zbMATH OpenOpenAlexFDO

Authors Sachio Hirokawa, Misao Nagayama, Yuichi Komori

Publication date 21 October 2001

Published in The 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)

Recommendations

• The proofs of α → α in P – W
• Types of I-free hereditary right maximal terms
• Publication:4489072
• Logical relations and the typed λ-calculus
• scientific article; zbMATH DE number 806614

Cites work

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

Cited in

(3)

• New(ish) foundations for theories of entailment
• scientific article; zbMATH DE number 1471988 (Why is no real title available?)
• Progressive logic

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

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