Phase Semantics

CS 358, Spring 1995 April 26 Lecture John Mitchell

1 Phase Space and Multiplicatives

A monoid M consists of a set M, associative binary operation · and unit 1 ∈ M with 1·x = x·1 = x for all x ∈ M. We generally omit the binary operation · and write xy for x · y.

A phase space consists of a commutative monoid M = ⟨M, · , 1⟩ and a chosen subset ⊥ ⊆ M. We interpret formulas of linear logic as particular subsets of M called “facts,” identified below, using the following operations

XY  = { xy | x ∈ X and y ∈ Y }
X−∘Y = { z ∈ M | zx ∈ Y all x ∈ X }
X^{⊥}  = X−∘⊥
X⊗Y = (XY)^{⊥⊥}
X℘Y = (X^{⊥}⊗Y^{⊥})^{⊥} = (X^{⊥}Y^{⊥})^{⊥}  (see below)

A subset X ⊆ M is a fact if X^{⊥⊥} = X. We say a fact X is valid if 1 ∈ X.

Straightforward properties:

1. For any X, Y ⊆ M, if X ⊆ Y , then Y^{⊥} ⊆ X^{⊥}.

2. For any X ⊆ M,we have X ⊆ X^{⊥⊥}.

3. Any X^{⊥} is a fact since X^{⊥⊥⊥} = X^{⊥}.

4. ⊥ is a fact since ⊥ = {1}^{⊥}.

5. The intersection of any collection of facts is a fact.

6. X^{⊥⊥} is the smallest fact containing X.

Associativity and commutativity of the connectives (other than −∘) follows from the associativity and commutativity of the underlying monoid. For associativity of ⊗, we use (X ⊗Y)⊗Z = (X ⊗Y ⊗Z)^{⊥⊥}. This follows from the following lemma.

Lemma: For any X, Y ⊆ M, we have X^{⊥⊥}Y^{⊥⊥} ⊆ (XY)^{⊥⊥}.

Proof: Suppose a ∈ X^{⊥⊥}, b ∈ Y^{⊥⊥} and c ∈ (XY)^{⊥}. We must show that abc = cba ∈ ⊥. Since c ∈ (XY)^{⊥}, we know that if x ∈ X and y ∈ Y , then cxy ∈ ⊥. It follows that cx ∈ Y^{⊥} = Y^{⊥⊥⊥} and therefore cxb ∈ ⊥. By similar reasoning, we can use cxb ∈ ⊥ and commutativity to show cb ∈ X^{⊥} = X^{⊥⊥⊥} and therefore conclude cba ∈ ⊥.

The remaining constants of linear logic are interpreted as the following facts:

\begin{aligned}1 & = & ⊥^{⊥} \\ ⊤ & = & ∅^{⊥} (= M) \\ 0 & = & ⊤^{⊥} \end{aligned}

A number of expected identities are relatively easy to check for all facts X, Y, Z ⊆ M.

\begin{matrix}X⊗Y = (X^{⊥}℘Y^{⊥})^{⊥} & X−∘Y = X^{⊥}℘Y \\ X℘Y = (X^{⊥}⊗Y^{⊥})^{⊥} & X−∘Y = (X⊗Y^{⊥})^{⊥} \\ X℘Y = X^{⊥}−∘Y & X⊗Y = (X−∘Y^{⊥})^{⊥} \\ ⊥℘X = X & 1⊗X = X \\ 1−∘X = X & X−∘⊥ = X^{⊥} \end{matrix}

Exercise

1. Show that if ⊢ Γ, then the interpretation of Γ in any phase space is a valid fact. A propositional letter may be assigned any fact, and a sequent Γ = A_{1}, …, A_{k} is interpreted as the par of its formulas, A_{1} ℘ … ℘A_{k}.

2 Examples

2.1 Integer phase space

An easy phase space is the monoid ⟨Z, +, 0⟩ of integers with addition with ⊥ = {0}. Here we have

\begin{aligned}XY & = & \{ x + y | x ∈ X and y ∈ Y \} \\ X−∘Y & = & \{ z ∈ M | z + x ∈ Y all x ∈ X \} \\ X^{⊥} & = & X−∘⊥ = \{ y | ∀x ∈ X. x + y = 0 \} \end{aligned}

In many cases, X −∘Y is empty. For example,

\begin{aligned}\{1, 2\}−∘\{2, 4\} & = & \{ x | x + 1 = 2 and x + 2 = 4 \} = ∅ \\ \{1, 2\}−∘\{0\} & = & \{ x | x + 1 = 0 and x + 2 = 0 \} = ∅ \end{aligned}

More generally, if X has more than one element, then X^{⊥} is empty and the smallest fact X^{⊥⊥} containing X is Z. Therefore, the only facts are ∅, singletons, and Z, with

∅^{⊥} = Z  {x}^{⊥} = {−x}^{⊥}  Z^{⊥} = ∅

For the other connectives, we have

X⊗Y = (XY)^{⊥⊥} = \{ \begin{matrix}Z & if X = Z and Y ≠ ∅ \\ \{x + y\} & if X = \{x\} and Y = \{y\} \\ ∅ & if X = ∅ or Y = ∅ \end{matrix}
X℘Y = (X^{⊥}⊗Y^{⊥})^{⊥} = X⊗Y

This is therefore a largely degenerate phase space.

2.2 Phase space of sequents

We can construct a phase space of sequents using the free commutative monoid M = ⟨M, ·, ϵ⟩ where M is the set of multisets of formulas (or, sequences modulo commutativity), · is concatenation and ϵ is the empty multiset. We let ⊥ = { Γ | ⊢ Γ }.

If Γ is a multiset, then

Pr(Γ) = { Σ | ⊢ Γ, Σ }

is a fact.

If we associate each propositional symbol P with the fact Pr(P), then we can show by induction that the meaning of a formula A is Pr(A).

Since ϵ ∈ Pr(A) means ⊢ A, we can prove completeness using this phase space.

Exercises

2. Show that each Pr(Γ) is a fact.

3. Complete the induction that the meaning of any formula A is Pr(A).

3 Additives

We can extend the interpretation of formulas, soundness and completeness to additive connectives using

\begin{aligned}X & Y & = & X ∩ Y \\ X ⊕ Y & = & (X ∪ Y)^{⊥⊥} \end{aligned}

Exercise

4. Check your favorite laws involving additives. For example, X & Y = (X^{⊥} ⊕ Y^{⊥})^{⊥} and X ⊕ Y = (X^{⊥} & Y^{⊥})^{⊥}, or maybe commutativity, associativity or units ⊤ & X = X and 0 ⊕ X = X.

4 Modalities (Exponentials)

A topolinear space P = ⟨M, ⊥, F⟩ consists of a phase space M, ⊥ and a set F of facts of the phase space satisfying the following conditions:

(i) F is closed under arbitrary with ( & ) (ii) F is closed under finite par ( ℘) (iii) ⊥ is the smallest fact in F (under the subset order) (iv) ℘ is idempotent on F, i.e., F ℘F = F for all F ∈ F.

The elements of F are called the closed facts of P. If X ∈ F, then X^{⊥} is called an open fact. The modal operators are interpreted in a topolinear space by

!X = the largest open fact F ⊆ X
?X = the smallest closed fact F ⊇ X

5 Quantifiers

See Lafont and Scedrov, The undecidability of second-order multiplicative linear logic.