Phase semantics - Revision history

Remi Nollet: “absorbant” ~> “absorbing”

2020-01-22T13:55:48Z

“absorbant” ~> “absorbing”

2011-10-22T14:05:45Z

‎Completeness: typo

2011-10-22T07:06:32Z

‎Soundness: \hdots not recoginzed by texvc

2011-10-22T07:05:29Z

‎Soundness: typo

2011-10-21T15:06:19Z

2011-10-21T14:52:12Z

+ soundness & completeness

2009-05-23T13:19:38Z

‎Relations and operators on subsets: simplified definition of <R>

2009-05-13T13:09:54Z

2009-05-12T07:28:36Z

2009-03-24T13:05:15Z

‎Closure operators

@@ Line 192: / Line 192: @@
 {{Lemma|
 * The operations <math>\tens</math>, <math>\parr</math>, <math>\plus</math> and <math>\with</math> are commutative and associative,
-* They have respectively <math>\one</math>, <math>\bot</math>, <math>\zero</math> and <math>\top</math> for neutral element,
+* They have respectively <math>\one</math>, <math>\bot</math>, <math>\zero</math> and <math>\top</math> as neutral element,
-* <math>\zero</math> is absorbant for <math>\tens</math>,
+* <math>\zero</math> is absorbing for <math>\tens</math>,
-* <math>\top</math> is absorbant for <math>\parr</math>,
+* <math>\top</math> is absorbing for <math>\parr</math>,
 * <math>\tens</math> distributes over <math>\plus</math>,
 * <math>\parr</math> distributes over <math>\with</math>.

@@ Line 242: / Line 242: @@
 {{Definition|The '''syntactic assignation''' is the assignation that sends any variable <math>\alpha</math> to the fact <math>\{\alpha\}\orth</math>.}}
-We instantiate the pole as <math>\Bot</math><math> := \{\Gamma \mid \vdash\Gamma\}</math>.
+We instantiate the pole as <math>\Bot := \{\Gamma \mid \vdash\Gamma\}</math>.
 {{Theorem|If <math>\Gamma\in\sem{\Gamma}\orth</math>, then <math>\vdash\Gamma</math>.}}

@@ Line 216: / Line 216: @@
 {{Definition|Let <math>(X, 1, \cdot)</math> be a commutative monoid.
-Given a formula <math>A</math> of linear logic and an assignation <math>\rho</math> that associate a fact to any variable, we can inductively define the interpretation <math>\sem{A}_\rho</math> of <math>A</math> in <math>X</math> as one would expect. Interpretation is lifted to sequents as <math>\sem{A_1, \hdots, A_n}_\rho = \sem{A_1}_\rho \parr \hdots \parr \sem{A_n}_\rho</math>.}}
+Given a formula <math>A</math> of linear logic and an assignation <math>\rho</math> that associate a fact to any variable, we can inductively define the interpretation <math>\sem{A}_\rho</math> of <math>A</math> in <math>X</math> as one would expect. Interpretation is lifted to sequents as <math>\sem{A_1, \dots, A_n}_\rho = \sem{A_1}_\rho \parr \cdots \parr \sem{A_n}_\rho</math>.}}
 {{Theorem|Let <math>\Gamma</math> be a provable sequent in linear logic. Then <math>1_X \in \sem{\Gamma}</math>.}}

@@ Line 218: / Line 218: @@
 Given a formula <math>A</math> of linear logic and an assignation <math>\rho</math> that associate a fact to any variable, we can inductively define the interpretation <math>\sem{A}_\rho</math> of <math>A</math> in <math>X</math> as one would expect. Interpretation is lifted to sequents as <math>\sem{A_1, \hdots, A_n}_\rho = \sem{A_1}_\rho \parr \hdots \parr \sem{A_n}_\rho</math>.}}
-{{Theorem|Let <math>\Gamma</math> be a provable sequent in linear logic. Then <math>1_X \in \sem{\Gamma}.}}
+{{Theorem|Let <math>\Gamma</math> be a provable sequent in linear logic. Then <math>1_X \in \sem{\Gamma}</math>.}}
 {{Proof|By induction on <math>\vdash\Gamma</math>.}}

@@ Line 241: / Line 241: @@
 {{Definition|The '''syntactic assignation''' is the assignation that sends any variable <math>\alpha</math> to the fact <math>\{\alpha\}\orth</math>.}}
 {{Theorem|If <math>\Gamma\in\sem{\Gamma}\orth</math>, then <math>\vdash\Gamma</math>.}}
@@ Line 246: / Line 248: @@
 {{Proof|By induction on <math>\Gamma</math>.}}
-Actually, this result is stronger, as the proof does not use the cut-rule in the reconstruction of <math>\vdash\Gamma</math>.
+== Cut elimination ==
 {{Theorem|If <math>\Gamma\in\sem{\Gamma}\orth</math>, then <math>\Gamma</math> is cut-free provable.}}

@@ Line 95: / Line 95: @@
 ==Phase Semantics==
 ===Phase spaces===
@@ Line 169: / Line 168: @@
 * the tensor <math>x\tens y</math> to be the fact <math>(x\cdot y)\biorth</math>;
 * the par connective is the de Morgan dual of the tensor: <math>x\parr y = (x\orth \tens y\orth)\orth</math>;
-* the linear arrow is just <math>x\limp y = (x\tens y\orth)\orth</math>.
+* the linear arrow is just <math>x\limp y = x\orth\parr y = (x\tens y\orth)\orth</math>.
 }}
@@ Line 213: / Line 212: @@
 Since <math>I</math> isn't necessarily a fact, we then take the biorthogonal to get a fact...
-==Completeness==
+== Soundness ==
 ==The Rest==

@@ Line 22: / Line 22: @@
 {{Definition|
 Let <math>R\subseteq X\times Y</math> be a relation, define the operators <math>\langle R\rangle</math>, <math>[R]</math> and <math>\_^R</math> taking subsets of <math>X</math> to subsets of <math>Y</math> as follows:
-# <math>b\in\langle R\rangle(x)</math> iff <math>\exists a\in X,\ (a,b)\in R \land a\in x</math>
+# <math>b\in\langle R\rangle(x)</math> iff <math>\exists a\in x,\ (a,b)\in R</math>
 # <math>b\in[R](x)</math> iff <math>\forall a\in X,\ (a,b)\in R \implies a\in x</math>
 # <math>b\in x^R</math> iff <math>\forall a\in x, (a,b)\in R</math>

@@ Line 165: / Line 165: @@
 {{Definition| title=multiplicative connectives|
 If <math>x</math> and <math>y</math> are facts in a phase space, we define
-* <math>\one = \{1\}\orth</math>;
+* <math>\one = \{1\}\biorth</math>;
 * <math>\bot = \one\orth</math>;
 * the tensor <math>x\tens y</math> to be the fact <math>(x\cdot y)\biorth</math>;

@@ Line 43: / Line 43: @@
 {{Definition|
-A closure operator on <math>\mathcal{P}(X)</math> is an monotonic increasing operator <math>P</math> on the subsets of <math>X</math> which satisfies:
+A closure operator on <math>\mathcal{P}(X)</math> is a monotonic operator <math>P</math> on the subsets of <math>X</math> which satisfies:
 # for all <math>x\subseteq X</math>, we have <math>x\subseteq P(x)</math>
 # for all <math>x\subseteq X</math>, we have <math>P(P(x))\subseteq P(x)</math>

@@ Line 51: / Line 51: @@
 It follows directly from the definition that for any closure operator <math>P</math>, the image <math>P(x)</math> is a fixed point of <math>P</math>. Moreover:
 {{Lemma|
 <math>P(x)</math> is the smallest fixed point of <math>P</math> containing <math>x</math>.