From Phase Semantics to Base-extension Semantics (and back)
For logicians working on semantics of linear logic, this paper provides a theoretical bridge between two distinct semantic frameworks.
The paper establishes an equivalence between phase semantics and base-extension semantics for linear logic by constructing bidirectional maps between bases and phase spaces, and defines base-extension semantics for the exponentials of linear logic.
Linear logic admits a wide range of semantic presentations reflecting its resource-sensitive notion of consequence. One well-known example is phase semantics: an algebraic semantics in which formulas are interpreted in phase spaces, consisting of a commutative monoid and a fixed subset, with respect to which an orthogonality relation is defined. A rather different and much more recent approach is given by base-extension semantics, which defines validity by inductively extending a provability relation on a base -- a set of inference rules over atomic propositions. We establish an equivalence between the two semantics by first defining bidirectional maps between bases and phase spaces, and then constructing an isomorphism between a phase space (resp. base) and its image under the composition of these maps. As a further contribution, we define the base-extension semantics clauses for the exponentials of linear logic.