Artemov, Sergei N. 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]. Cited in 7 Documents 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 Keywords:Logic of Proofs; modal logic; simple \(\lambda\)-calculus; modal \(\lambda\)-calculus; provability semantics; proof polynomials; provability interpretation PDFBibTeX XMLCite \textit{S. N. Artemov}, CSLI Lect. Notes 144, 89--118 (2001; Zbl 1080.03037)