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

DOI10.1007/S10992-018-9484-ZzbMath1457.03023OpenAlexW2889815034MaRDI QIDQ2000674

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

completenessphase semanticstype theorystrong normalizationsecond-order intuitionistic propositional logic

Mathematics Subject Classification ID

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

Cites Work

• Unnamed Item
• Advances in proof-theoretic semantics
• Linear logic
• Lectures on the Curry-Howard isomorphism
• 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.
• Validity concepts in proof-theoretic semantics
• Union of Reducibility Candidates for Orthogonal Constructor Rewriting

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