The semantics given by phase spaces is a kind of "formula and provability semantics", and is thus quite different in spirit from the more usual denotational semantics of linear logic. (Those are rather some "formulas and proofs semantics".)
--- probably a whole lot more of blabla to put here... ---
Preliminaries: relation and closure operators
Part of the structure obtained from phase semantics works in a very general framework and relies solely on the notion of relation between two sets.
Relations and operators on subsets
The starting point of phase semantics is the notion of duality. The structure needed to talk about duality is very simple: one just needs a relation R between two sets X and Y. Using standard mathematical practice, we can write either or to say that and are related.
Such a relation yields three interesting operators sending subsets of X to subsets of Y:
The operator is usually called the direct image of the relation, [R] is sometimes called the universal image of the relation.
It is trivial to check that and [R] are covariant (increasing for the relation) while _R is contravariant (decreasing for the relation). More interesting:
Lemma (Galois Connections)
This implies directly that commutes with arbitrary unions and [R] commutes with arbitrary intersections. (And in fact, any operator commuting with arbitrary unions (resp. intersections) is of the form (resp. [R]).
Remark: the operator _R sends unions to intersections because is right adjoint to ...
Closure operators are quite common in mathematics and computer science. They correspond exactly to the notion of monad on a preorder...
It follows directly from the definition that for any closure operator P, the image P(x) is a fixed point of P. Moreover:
One other important property is the following:
A closure operator is in fact determined by its set of fixed points: we have
Since any complete inf-lattice is automatically a complete sup-lattice, is also a complete sup-lattice. However, the sup operation isn't given by plain union:
A rather direct consequence of the Galois connections of the previous section is:
A last trivial lemma:
Remark: everything gets a little simpler when R is a symmetric relation on X.
Definition (Phase space)
Thanks to the preliminary work, we have:
The previous corollary makes the following definition correct:
Definition (additive connectives)
Once again, the next lemma follows from previous observations:
Lemma (additive de Morgan laws)
In order to define the multiplicative connectives, we actually need to use the monoid structure of our phase space. One interpretation that is reminiscent in phase semantics is that our spaces are collections of tests / programs / proofs / strategies that can interact with each other. The result of the interaction between a and b is simply .
The set can be thought of as the set of "good" things, and we thus have iff "a interacts correctly with all the elements of x".
Thus contains all the possible interactions between one element of x and one element of y.
The tensor connective of linear logic is now defined as:
Definition (multiplicative connectives)
Note that by unfolding the definition of , we have the following, "intuitive" definition of :
Readers familiar with realisability will appreciate...
Some people say that this idea of orthogonality was implicitly present in Tait's proof of strong normalisation. More recently, Jean-Louis Krivine and Alexandre Miquel have used the idea explicitly to do realisability...
All the expected properties hold:
This definition captures precisely the intuition behind the exponentials:
- we need to have contraction, hence we restrict to indempotents in x,
- and weakening, hence we restrict to .
Since I isn't necessarily a fact, we then take the biorthogonal to get a fact...
Phase semantics is complete w.r.t. linear logic. In order to prove this, we need to build a particular commutative monoid.
The equivalence relation intuitively means that we do not care about the multiplicity of -formulae.
We instantiate the pole as .
Actually, the completeness result is stronger, as the proof does not use the cut-rule in the reconstruction of . By refining the pole as the set of cut-free provable formulae, we get:
From soundness, one can retrieve the cut-elimination theorem.