We found a match
Your institution may have access to this item. Find your institution then sign in to continue.
- Title
Completeness of Second-Order Intuitionistic Propositional Logic with Respect to Phase Semantics for Proof-Terms.
- Authors
Takahashi, Yuta; Takemura, Ryo
- Abstract
Girard introduced phase semantics as a complete set-theoretic semantics of linear logic, and Okada modified phase-semantic completeness proofs to obtain normal-form theorems. On the basis of these works, Okada and Takemura reformulated Girard's phase semantics so that it became phase semantics for proof-terms, i.e., lambda-terms. They formulated phase semantics for proof-terms of Laird's dual affine/intuitionistic lambda-calculus and proved the normal-form theorem for Laird's calculus via a completeness theorem. Their semantics was obtained by an application of computability predicates. In this paper, we first formulate phase semantics for proof-terms of second-order intuitionistic propositional logic by modifying Tait-Girard's saturated sets method. Next, we prove the completeness theorem with respect to this semantics, which implies a strong normalization theorem.
- Subjects
SEMANTICS; COMPLETENESS theorem; TYPE theory; SYNTAX (Grammar); MATHEMATICS theorems
- Publication
Journal of Philosophical Logic, 2019, Vol 48, Issue 3, p553
- ISSN
0022-3611
- Publication type
Article
- DOI
10.1007/s10992-018-9484-z