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

DOI10.1007/S10992-018-9484-ZzbMATH Open1457.03023OpenAlexW2889815034MaRDI QIDQ2000674FDOQ2000674

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

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

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)

Cites Work

• Advances in proof-theoretic semantics
• Title not available (Why is that?)
• Linear logic
• Lectures on the Curry-Howard isomorphism
• Validity concepts in proof-theoretic semantics
• A uniform semantic proof for cut-elimination and completeness of various first and higher order logics.
• Game semantics and linear CPS interpretation
• 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

Cited In (1)

• 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)