Journal of Philosophical Logic 48 (3):553-570 (2019)

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.
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.1007/s10992-018-9484-z
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 58,903
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

Ideas and Results in Proof Theory.Dag Prawitz & J. E. Fenstad - 1975 - Journal of Symbolic Logic 40 (2):232-234.
Proof-Theoretic Semantics.Peter Schroeder-Heister - forthcoming - Stanford Encyclopedia of Philosophy.

Add more references

Citations of this work BETA

No citations found.

Add more citations

Similar books and articles

Completeness and Incompleteness for Intuitionistic Logic.Charles McCarty - 2008 - Journal of Symbolic Logic 73 (4):1315-1327.
Negationless Intuitionism.Enrico Martino - 1998 - Journal of Philosophical Logic 27 (2):165-177.
Undecidability and Intuitionistic Incompleteness.D. C. McCarty - 1996 - Journal of Philosophical Logic 25 (5):559 - 565.
Phase Semantics and Petri Net Interpretation for Resource-Sensitive Strong Negation.Norihiro Kamide - 2006 - Journal of Logic, Language and Information 15 (4):371-401.
Constructive Sheaf Semantics.Erik Palmgren - 1997 - Mathematical Logic Quarterly 43 (3):321-327.
A Game Semantics for System P.J. Marti & R. Pinosio - 2016 - Studia Logica 104 (6):1119-1144.


Added to PP index

Total views
15 ( #657,547 of 2,426,398 )

Recent downloads (6 months)
1 ( #541,589 of 2,426,398 )

How can I increase my downloads?


My notes