Completeness of second-order intuitionistic propositional logic with respect to phase semantics for proof-terms

DOI10.1007/S10992-018-9484-ZMaRDI QIDQ2000674zbMATH OpenOpenAlexFDO

Authors Yuta Takahashi, Ryo Takemura

Publication date 28 June 2019

Published in Journal of Philosophical Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10992-018-9484-z

zbMATH Keywords

completenesstype theorystrong normalizationphase semanticssecond-order intuitionistic propositional logic

Mathematics Subject Classification ID

Classical propositional logic (03B05) Higher-order logic (03B16) Subsystems of classical logic (including intuitionistic logic) (03B20)

Recommendations

• scientific article; zbMATH DE number 1231526
• A secondary semantics for Second Order Intuitionistic Propositional Logic
• Une Preuve Formelle et Intuitionniste du Théorème de Complétude de la Logique Classique
• Remarks on Semantic Completeness for Proof-Terms with Laird’s Dual Affine/Intuitionistic λ-Calculus
• Phase semantic cut-elimination and normalization proofs of first- and higher-order linear logic

Cites work

• scientific article; zbMATH DE number 3358455 (Why is no real title available?)
• A uniform semantic proof for cut-elimination and completeness of various first and higher order logics.
• Advances in proof-theoretic semantics
• Game semantics and linear CPS interpretation
• Lectures on the Curry-Howard isomorphism
• Linear logic
• Rewriting, computation and proof. Essays dedicated to Jean-Pierre Jouannaud on the occasion of his 60th birthday.
• Union of Reducibility Candidates for Orthogonal Constructor Rewriting
• Validity concepts in proof-theoretic semantics

Cited in

(2)

• A phase semantics for polarized linear logic and second order conservativity
• Simple proof of the completeness theorem for second-order classical and intuitionistic logic by reduction to first-order mono-sorted logic

This page was built for publication: Completeness of second-order intuitionistic propositional logic with respect to phase semantics for proof-terms

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