×

Unified semantics for modality and \(\lambda\)-terms via proof polynomials. (English) Zbl 1080.03037

Vermeulen, Kees (ed.) et al., Algebras, diagrams and decisions in language, logic and computation. Stanford, CA: CSLI Publications (ISBN 1-57586-372-3/pbk; 1-57586-371-5/pbk). CSLI Lecture Notes 144, 89-118 (2001).
Summary: It is shown that the modal logic S4, simple \(\lambda\)-calculus and modal \(\lambda\)-calculus admit a realization in a very simple propositional logical system, \({\mathcal L}{\mathcal P}\), which has an exact provability semantics. In \({\mathcal L}{\mathcal P}\) both modality and \(\lambda\)-terms become objects of the same nature, namely, proof polynomials. The provability interpretation of modal \(\lambda\)-terms presented here may be regarded as a system-independent generalization of the Curry-Howard isomorphism of proofs and \(\lambda\)-terms.
For the entire collection see [Zbl 1063.03004].

MSC:

03F45 Provability logics and related algebras (e.g., diagonalizable algebras)
03B45 Modal logic (including the logic of norms)
03B40 Combinatory logic and lambda calculus
PDFBibTeX XMLCite