Title: Theory / Unimportant / Math / Logic / Linear logic - Gyrard/
Tags: fromMath mathToSee mathToDef hasSeenConjDef toBinaryFunction fromImplication closed examplesSwitchExample1 toBinaryRelation

Name: Phase space
Definition: A pair \((P,1,\bot_P)\), with \((P,1)\) a commutative monoid and \(\bot_P\subseteq P\).
Page: 18
Section: 1
Kind: Def

Name: The set of antiphase of \(P\)
Page: 18
Section: 1
Variables: \((P,\bot_P)\) a phase space
Notation: \(\bot_P\)
Kind: Def
Name2: The orthogonal phases of \(P\)

Name: Dual of \(G\)
Definition: \(\{p\in P;pG\subseteq \bot\}\).
Page: 18
Section: 1
Variables: \((P,\bot_P)\) a phase space
\(G\subseteq P\)
Notation: \(G^\bot\)
Index: 2
Kind: Def
Extra: Original is \(\{p\in P\mid \forall q(q\in G\implies pq\in\bot)\}\)

Name: The phases of \(G\)
Definition: The elements of \(G\).
Page: 18
Section: 1
Variables: \((P,\bot_P)\) a phase space
\(G\subseteq P\) a fact
Index: 3
Kind: Def

Name: A valid fact
Definition: A fact containing 1.
Page: 18
Section: 1
Variables: \((P,\bot_P)\) a phase space
\(G\subseteq P\) a fact
Index: 3
Kind: Def

Smaller0: \( G\)
Greater0: \(G^{\bot\bot}\)
Page: 18
Section: 1
Variables: \((P,\bot_P)\) a phase space
\(G\subseteq P\)
Index: 4 (i)
Kind: Prop
Smaller to greater: \(\subseteq\)
Greater to smaller: \(\supseteq\)
Extra: Proof:
Let \(p\in G\), let us prove that \(p\in G^{\bot\bot}\).
Let \(p'\in G\) such taht \(p'G\subseteq \bot\). It follows that \(pp'\in \bot\), thus \(p\in \{p\in P\mid \forall p'\in P. p'G\subseteq\bot\implies pp'\in \bot\}=G^{\bot\bot}\).

Smaller0: \(G\subseteq H\)
Greater0: \(H^\bot\subseteq G^\bot\)
Page: 18
Section: 1
Variables: \((P,\bot_P)\) a phase space
\(G,H\subseteq P\)
Index: 4 (ii)
Kind: Prop
Hide middle: yes
Extra: Proof:
Let \(G\subseteq H\), let us proof that \(H^\bot\subseteq G^\bot\).
Let \(p\in H^\bot\). Hence, \(pH\subseteq \bot\), it follows that \(pG\subseteq \bot\), and thus \(p\in G^\bot\)

Question: \(\{1\}^\bot=\)
Answer: \(\bot\).
Page: 18
Section: 1
Variables: \((P,\bot_P)\) a phase space
Index: 5 (i)
Kind: Ex

Definition: \(\bot^\bot\)
Page: 18
Section: 1
Variables: \((P,\bot_P)\) a phase space
Notation: \(\mathbf 1\)
Index: 5 (ii)
Kind: Ex
Typ: A submonoid of \(P\)

Question: \(\emptyset^\bot\) is
Answer: \(P\).
Page: 18
Section: 1
Variables: \((P,\bot_P)\) a phase space
Index: 5 (ii)
Kind: Ex

Definition: \(P\)
Page: 18
Section: 1
Variables: \((P,\bot_P)\) a phase space
Notation: \(\top\)
Index: 5 (ii)
Kind: Ex

Name: The class of facts
Page: 18
Section: 1
Index: 6
Variables: \((P,\bot_P)\) a phase space
Kind: Prop
Under: abritrary intersections

Name: nil
Page: 19
Section: 1
Notation: \(\bot\)
Index: 7
Kind: Def

Page: 19
Section: 1
Notation: [$]G\parr H[/$]
Variables: \((P,\bot_P)\) a phase space
\(G,H\subseteq P\) facts
Name: Their parallelization
Definition: \((G^\bot .H^\bot)^\bot\).
Kind: Def
Index: 8 (i)
Commutative: Commutative
Associative: associative

Page: 19
Definition: \((G,H)\mapsto (G.H)^{\bot\bot}\).
Section: 1
Variables: \((P,\bot_P)\) a phase space,
Notation: \(\otimes\)
Name: The tensorization of facts
Kind: Def
Index: 8 (ii)
Transitive: Associative, commutative

Smaller0: \(G\times H\)
Greater0: [$](G^\bot\parr H^\bot)^\bot[/$]
Page: 19
Section: 1
Variables: \((P,\bot_P)\) a phase space,
\(G,H\subseteq P\).
Index: 9 (i)
Smaller to greater: =
Hide middle: yes

Smaller0: [$]G\parr H[/$]
Greater0: \((G^\bot\times H^\bot)^\bot\)
Page: 19
Section: 1
Variables: \((P,\bot_P)\) a phase space, \(G,H\subseteq P\).
Index: 9 (i)
Smaller to greater: =
Hide middle: yes

Smaller0: [$]G\parr H[/$]
Greater0: \(G^\bot\multimap H\)
Page: 19
Section: 1
Variables: \((P,\bot_P)\) a phase space,
\(G,H\subseteq P\).
Index: 9 (i)
Smaller to greater: =
Hide middle: yes

Smaller0: \(G\times H\)
Greater0: \((G\multimap H^\bot)^\bot\)
Page: 19
Section: 1
Variables: \((P,\bot_P)\) a phase space
\(G,H\subseteq P\).
Index: 9 (i)
Smaller to greater: =
Hide middle: yes

Smaller0: \(G\multimap H\)
Greater0: [$]G^\bot\parr H[/$]
Page: 19
Section: 1
Variables: \((P,\bot_P)\) a phase space, \(G,H\subseteq P\).
Index: 9 (i)
Smaller to greater: =
Hide middle: yes

Smaller0: \(G\multimap H\)
Greater0: \((G\otimes H^\bot)^\bot\)
Page: 19
Section: 1
Variables: \((P,\bot_P)\) a phase space, \(G,H\subseteq P\).
Index: 9 (i)
Smaller to greater: =
Hide middle: yes

Q: [...] of [...] is [...].
A: The identity; [$]\parr[/$]; \(\bot\)
Page: 19
Section: 1
Index: 9 (ii)

Q: [...] of [...] is [...].
A: The identity; \(\otimes\); \(1\)
Page: 19
Section: 1
Index: 9 (ii)

Q: [...] of [...] is [...].
A: The left identity; \(\multimap\); \(1\)
Page: 19
Section: 1
Index: 9 (iii)

Smaller0: \(\multimap\)
Greater0: \(G^\bot\)
Page: 19
Section: 1
Variables: \((P,\bot_P)\) a phase space,
\(G\subseteq P\).
Index: 9 (iii)
Smaller to greater: =
Hide middle: yes
Smaller1: \(\bot\)
Prefix Smaller: \(G\)
Connect Smaller0: .

Definition: \(G\multimap H\)\(=H^\bot\multimap G^\bot\)
Page: 19
Section: 1
Variables: \((P,\bot_P)\) a phase space, let \(G,H\subseteq P\).
Index: 9 (iii)

Smaller0: \((G\otimes H)\multimap K\)
Greater0: \(G\multimap (H\multimap K)\)
Page: 19
Section: 1
Variables: \((P,\bot_P)\) a phase space, let \(G,H,K\subseteq P\).
Index: 9 (iii)
Smaller to greater: =
Hide middle: yes

Smaller0: [$]G\multimap(H\parr K)[/$]
Greater0: [$](G\multimap H)\parr K[/$]
Page: 19
Section: 1
Variables: \((P,\bot_P)\) a phase space
\(G,H,K\subseteq P\).
Index: 9 (iii)
Smaller to greater: =
Hide middle: yes

Smaller0: \(F^{\bot\bot}G^{\bot\bot} \)
Greater0: \((FG)^{\bot\bot}\)
Page: 20
Section: 1
Variables: \((P,\bot_P)\) a phase space
\(F,G\subseteq P\)
Kind: Def
Greater to smaller: \(\supseteq\)

Name: The multiplicative connectives
Definition: [$]\parr, \otimes,\multimap[/$].
Page: 19
Section: 1
Index: 8
Kind: Def

Name: par
Page: 19
Section: 1
Notation: [$]\parr[/$]
Index: 8
Kind: Def

Name: times
Page: 19
Section: 1
Notation: \(\otimes\)
Index: 8
Kind: Def

Name: entails
Page: 19
Section: 1
Notation: \(\multimap\)
Index: 8
Kind: Def

Name: with
Page: 20
Section: 1
Context: linear logic
Notation: \(\&\)
Index: 11
Kind: Def

Name: plus
Page: 20
Section: 1
Notation: \(\oplus\)
Index: 11
Kind: Def

Page: 20
Section: 1
Notation: \(\oplus\)
Variables: \((P,\bot_P)\) a phase space,
Name: Direct sum of facts
Definition: \((G,H)\mapsto (G\cup H)^{\bot\bot}\)
Kind: Def,
Index: 11, 12
Commutative: Commutative
Associative: associative

Page: 20
Section: 1
Notation: \(\&\)
Variables: \((P,\bot_P)\) a phase space,
Name: Direct product of facts
Definition: \((G,H)\mapsto (G\cap H)\)
Kind: Def,
Index: 11, 12
Commutative: Commutative
Associative: associative
Extra: No nil are required to transform this into a fact.
While the name is product, the symbol is not product.

Name: The additive connectives
Definition: \(\oplus, \&\)
Page: 20
Section: 1
Variables: \((P,\bot_P)\) a phase space,
\(G,H\subseteq P\), facts
Index: 11
Kind: Def,

Definition: \(G\& H\)\(=(G^\bot\oplus H^\bot)^\bot\).
Page: 20
Section: 1
Variables: \((P,\bot_P)\) a phase space,
\(G,H\subseteq P\), facts
Index: 12

Definition: \(G\oplus H\)\(=(G^\bot\& H^\bot)^\bot\).
Page: 20
Section: 1
Variables: \((P,\bot_P)\) a phase space,
\(G,H\subseteq P\), facts
Index: 12

Q: [...] of [...] is [...]
A: The identity; \(\&\); \(\top\)
Page: 20
Section: 1
Index: 12 (ii)

Q: [...] of [...] is [...]
A: The identity; \(\oplus\); 0
Page: 20
Section: 1
Index: 12 (ii)

Q: [...] is distributive wrt [...].
A: \(\otimes\); \(\oplus\)
Page: 20
Section: 1
Index: 13

[$]\parr[/$] is distributive wrt \(\&\).
[$]G\parr (H\&K)=(G\parr H)\&(G\parr K)[/$]
Page: 20
Section: 1
Index: 13

Q: The [...] of [...] is [...].
A: zero; \(\otimes\); \(0\)
Page: 20
Section: 1
Variables: \((P,\bot_P)\) a phase space
Index: 13 (i)

Q: [...] of [...] is [...].
A: The zero; [$]\parr[/$]; \(\top\)
Page: 20
Section: 1
Variables: \((P,\bot_P)\) a phase space,
Index: 13 (i)

Smaller0: \((G\oplus H)\multimap K\)
Greater0: \((G\multimap K)\&(H\multimap K)\)
Page: 20
Section: 1
Variables: \((P,\bot_P)\) a phase space,
\(G\) a fact
Index: 13 (i)
Smaller to greater: =
Hide middle: yes

Smaller0: \(G\multimap (H\& K)\)
Greater0: \((G\multimap H)\& (G\multimap K)\)
Page: 20
Section: 1
Variables: \((P,\bot_P)\) a phase space,
\(G\) a fact
Index: 13 (i)
Smaller to greater: =
Hide middle: yes

Q: \([...][...] G=[...]\).
A: 0; \multimap; \top
Page: 20
Section: 1
Variables: \((P,\bot_P)\) a phase space,
\(G\) a fact
Index: 13 (i)

Q: [...] of \(\multimap\) is [...].
A: The right zero; \(\top\)
Page: 20
Section: 1
Index: 13 (i)

\(G\otimes (H\& K)\subseteq(G\otimes H)\&(G\otimes K)\).
Page: 20
Section: 1
Variables: \((P,\bot_P)\) a phase space,
\(G\) a fact
Index: 13 (ii)

[$]G\parr (H\oplus K)\supseteq(G\parr H)\oplus(G\parr K)[/$].
Page: 20
Section: 1
Variables: \((P,\bot_P)\) a phase space,
\(G\) a fact
Index: 13 (ii)

Question: \((A\otimes B)^\bot=\)
Answer: [$] A^\bot\parr B^\bot[/$]
Page: 21
Section: 1
Variables: \((P,\bot_P)\) a phase space,
\(A,B\subseteq P\)

Question: [$](A\parr B)^\bot=[/$]
Answer: \( A^\bot\otimes B^\bot\)
Page: 21
Section: 1
Variables: \((P,\bot_P)\) a phase space,
\(A,B\subseteq P\)

Question: \((A\oplus B)^\bot=\)
Answer: \( A^\bot\& B^\bot\)
Page: 21
Section: 1
Variables: \((P,\bot_P)\) a phase space,
\(A,B\subseteq P\)

Question: \((A\& B)^\bot=\)
Answer: \( A^\bot\oplus B^\bot\)
Page: 21
Section: 1
Variables: \((P,\bot_P)\) a phase space,
\(A,B\subseteq P\)

Name: A phase structure for the propositional language
Definition: Given \((P,\bot)\) some phase space. For each propositional letter \(a\), a fact of \(P\).
Page: 22
Section: 1
Variables: \(L\) a set of propositional letters
Index: 14 (i)
Kind: def

Name: A proposition valid in \(S\)
Definition: A proposition \(P\) such that \(1\in S(P)\).
Page: 22
Section: 1
Variables: \(L\) a set of propositional letters,
\(S\) a structure
Context: Linear logic
Index: 14 (ii)
Kind: def

Name: A linear tautology
Definition: A proposition \(P\) such that \(1\in S(P)\) for each phase structure \(S\).
Page: 22
Section: 1
Index: 14 (iv)
Kind: Def

Name: The logical axiom
Definition: \(\vdash A, A^\bot\).
Page: 22
Section: 1
Variables: in proof tree
Index: 15
Kind: Def

[latex]
\begin{prooftree}
\AxiomC{ $\vdash A,B$ }
\AxiomC{ $\vdash A^\bot, C$ }
\RightLabel{ CUT }
\BinaryInfC{ $\vdash B,C$ }
\end{prooftree}
[/latex].
Page: 22
Section: 1
Index: 15
Kind: Def
Name: Cut rule

Q: [latex]
\begin{prooftree}
\AxiomC{ $\vdash [...]$ }
\RightLabel{ [...] }
\UnaryInfC{ $\vdash$ [...] }
\end{prooftree}
[/latex].
A: A; EXCH; permutation of the elements of $A$
Page: 22
Section: 1
Index: 15
Kind: Def
Name: Exchange rule

Name: Axiom of \(\top\)
Definition: \(\vdash \top, A\)
Page: 22
Section: 1
Context: Linear logic
Index: 15
Kind: def

[latex]
\begin{prooftree}
\AxiomC{ $\vdash A,C$ }
\AxiomC{ $\vdash B,C$ }
\RightLabel{ $\&$ }
\BinaryInfC{ $\vdash A\&B,C$ }
\end{prooftree}
[/latex].
Page: 22
Section: 1
Kind: 15
Name: \(\&\)-rule
Example: Def

[latex]
\begin{prooftree}
\AxiomC{ $\vdash A,C$ }
\RightLabel{ $1\oplus $ }
\UnaryInfC{ $\vdash A\oplus B,C$ }
\end{prooftree}
[/latex].
Page: 22
Section: 1
Kind: 15
Name: \(1\oplus\)-rule
Example: Def

[latex]
\begin{prooftree}
\AxiomC{ $\vdash B,C$ }
\RightLabel{ $2\oplus $ }
\UnaryInfC{ $\vdash A\oplus B,C$ }
\end{prooftree}
[/latex].
Page: 22
Section: 1
Kind: 15
Name: \(2\oplus\)-rule
Example: Def

[latex]
\begin{prooftree}
\AxiomC{ $\vdash A,C$ }
\AxiomC{ $\vdash B,D$ }
\RightLabel{ $\otimes $ }
\BinaryInfC{ $\vdash A\otimes B,C,D$ }
\end{prooftree}
[/latex].
Page: 22
Chapter: 1
Section: 15
Kind: Def
Name: \(\otimes\)-rule

[latex]
\begin{prooftree}
\AxiomC{ $\vdash A,B,C$ }
\RightLabel{ $\parr $ }
\UnaryInfC{ $\vdash A\parr B,C$ }
\end{prooftree}
[/latex].
Page: 22
Chapter: 1
Section: 15
Kind: Def
Name: [$]\parr[/$] rule

[latex]
\begin{prooftree}
\AxiomC{ $\vdash A$ }
\RightLabel{ $\bot $ }
\UnaryInfC{ $\vdash \bot,A$ }
\end{prooftree}
[/latex].
Page: 22
Section: 15
Kind: Def
Name: \(\bot\) rule
Extra: c1 equals weakeni'g

Name: \(1\) rule
Definition: \(\vdash 1\)
Page: 22
Chapter: 1
Section: 15
Kind: def

Smaller0: \(p\in\mathbf 1\) and \(q\in G\)
Greater0: \(pq\in G^{\bot\bot}\)
Page: 18
Section: 1
Variables: \((P,\bot)\) a phase space,
\(G\subseteq P\),
\(p,q\in P\)
Index: 5(ii)
Kind: Ex
Hide middle: yes

Q: \(([...] G_i)^\bot=([...] G_i^\bot)\).
A: \bigcup_{i\in I}; \bigcap_{i\in I}
Page: 18
Section: 1
Variables: \((P,\bot)\) a phase space,
\(I\) an indexing set
\((G_i)_{i\in I}\subseteq P\)
Index: 6
Kind: Prop
Extra: Let us prove \(\subseteq\). Let \(p\in (G_0\cup G_1)^\bot\) and let us prove \(p\in G_0^\bot\cap G_1^\bot\). Let \(q\in G_i\), it suffices to show that \(pq\in \bot\).
Since \(p\in (G_0\cup G_1)^\bot\), \(p(G_0\cup G_1)\subseteq \bot\). Since \(g\in G_i\), \(q\in G_0\cup G_1\), therefore, \(pq\in \bot\).
Let us prove \(\supseteq\). Let \(p\in G_0^\bot\cap G_1^\bot\) and let us prove that \(p\in (G_0\cup G_1)^\bot\). Let \(q\in G_i\), it suffices to prove that \(pq\in \bot\). Since \(p\in G_i^\bot\), \(pG_i\subseteq\bot\), hence \(pq\in \bot\).

Name: Positive connective
Definition: \(\oplus, 0, \otimes, 1, !\).
Page: wp
Intuition: Author of the anki card intuition is: their derivation rules does not like its neighbors. It sends as little as possible from bottom to top, and must be alone to be a top. At worst, everthing else is a wh not ?.

Question: \(\vdash A_1,\dots,A_n\) should be understood as
Answer: [$]\vdash A_1\parr \dots\parr A_n[/$] if \(n\ge1\) and \(\bot\) otherwise
Page: 23
Chapter: 1
Section: 16

Q: [...] [...] [...]
A: Linear sequent calculus with exponentials; is sound and complete with respect to; validity in topolinear structure
Page: 26
Chapter: 1
Section: 22
Kind: Theorem

Name: A closed fact
Definition: An element of \(\mathbb F\)
Page: 25
Chapter: 1
Section: 19
Variables: \((P,\bot,\mathbb F)\) a topolinear space
Kind: Def

Name: An open fact
Definition: A linear negation of a closed fact
Page: 25
Chapter: 1
Section: 19
Variables: \((P,\bot,\mathbb F)\) a topolinear space
Kind: Def

Name: The affirmation of \(G\)
Definition: The \(\subseteq\)-greatest open fact included in \(G\)
Page: 25
Chapter: 1
Section: 20
Variables: \((P,\bot,\mathbb F)\) a topolinear space,
\(G\) a fact
Context: linear logic
Notation: \(!G\)
Kind: Def
Name2: The interior \(G\)

Name: The consideration of \(G\)
Definition: The \(\subseteq\)-smallest fact containing \(G\)
Page: 25
Chapter: 1
Section: 20
Variables: \((P,\bot,\mathbb F)\) a topolinear space,
\(G\) a fact
Notation: \(?G\)
Kind: Def
Name2: The closure of \(G\)

Smaller0: \(?(A^\bot)\)
Greater0: \((!A)^\bot\)
Page: 25
Chapter: 1
Section: 20
Variables: \((P,\bot,\mathbb F)\) a topolinear space,
\(G\) a fact
Kind: Def
Smaller to greater: =

Smaller0: \(!(A^\bot)\)
Greater0: \((?A)^\bot\)
Page: 25
Chapter: 1
Section: 20
Variables: \((P,\bot,\mathbb F)\) a topolinear space,
\(G\) a fact
Kind: Def

Definition: \(?C_1,\dots, ?C_n\)
Page: 25
Chapter: 1
Section: 20
Variables: \((P,\bot,\mathbb F)\) a topolinear space,
\(\vec C=C_1,\dots, C_n\) a fact
Notation: \(?\vec C\)
Kind: Def

[latex]
\begin{prooftree}
\AxiomC{ $\vdash A,B$ }
\RightLabel{ $D? $ }
\UnaryInfC{ $\vdash ?A,B$ }
\end{prooftree}
[/latex].
Page: 25
Chapter: 1
Section: 21
Variables: \((P,\bot,\mathbb F)\) a topolinear space,
\(A,B\) facts
Kind: Def
Name: Dereliction

[latex]
\begin{prooftree}
\AxiomC{ $\vdash B$ }
\RightLabel{ $W? $ }
\UnaryInfC{ $\vdash ?A,B$ }
\end{prooftree}
[/latex].
Page: 25
Chapter: 1
Section: 21
Variables: \((P,\bot,\mathbb F)\) a topolinear space,
\(A,B\) facts
Kind: Def
Name: Weakening ?

[latex]
\begin{prooftree}
\AxiomC{ $\vdash ?A,?A,B$ }
\RightLabel{ $C? $ }
\UnaryInfC{ $\vdash ?A,B$ }
\end{prooftree}
[/latex].
Page: 25
Chapter: 1
Section: 21
Variables: \((P,\bot,\mathbb F)\) a topolinear space,
\(A,B\) facts
Kind: Def
Name: Contraction

[latex]
\begin{prooftree}
\AxiomC{ $\vdash A,?B$ }
\RightLabel{ $! $ }
\UnaryInfC{ $\vdash !A,B$ }
\end{prooftree}
[/latex].
Page: 25
Chapter: 1
Section: 21
Variables: \((P,\bot,\mathbb F)\) a topolinear space,
\(A,B\) facts
Kind: Def
Name: Weakening !

Q: [...] [...] [...]
A: Linear predicate calculus; is sound and complete with respect to; phase semantics
Page: 23
Chapter: 1
Section: 16, 17
Kind: Theorem

Q: [latex]
\begin{prooftree}
\AxiomC{ $\vdash A,B$ }
\RightLabel{ {{1::$\bigwedge $}} }
\UnaryInfC{ $\vdash [...]A,B$ }
\end{prooftree}
[/latex].
A: \bigwedge x
Page: 27
Chapter: 1
Section: 24
Kind: Def

Q: [...] [...] [...]
A: Linear sequent calculus; is sound and complete with respect to; validity in phase structure
Page: 23
Chapter: 1
Section: 16, 17
Kind: Theorem

Name: of course
Page: wp
Notation: !
Name2: bang

Name: why not
Page: wp
Notation: ?

Name: Negative connective
Definition: [$]\&, \bot, \parr, \top[/$].
Page: wp
Definition2: ?
Conjdef: all of
Intuition: Author of the anki card intuition is: their derivation rules likes its neighbor, accept them, and sends as much as possible from bottom to top

Name: A fact
Definition: A subset \(G\subseteq P\) such that \(G^{\bot\bot}=G\)
Page: 18
Section: 1
Variables: \((P,\bot_P)\) a phase space.
Index: 3, 4 (iii), 5 (i)
Kind: Def, Prop, Ex
Definition2: \(H^\bot\) for some \(H\subseteq P\)
Example: \(\bot\), \(\top\), \(\mathbf{0}\), \(\mathbf 1\).
Extra: \(G\) such that
\(G\) equals \(\{p\in P;p\{p'\in P;p'G\subseteq \bot\}\subseteq \bot\}\), that is, equal to
\(\{p\in P\mid \forall p'\in P. p'G\subseteq\bot\implies pp'\in \bot\}\)
Let \(G\subseteq P\) and let us prove that \(G^{\bot\bot\bot}=G^\bot\). \(\supseteq \) follows from \((i)\). Let us prove \(\subseteq\).
Let \(p\in G^{\bot\bot\bot}\), that is \(pG^{\bot\bot}\subseteq \bot\), we want to prove that \(pG\subseteq \bot\). Let \(s\in G\), it suffices to prove that \(ps\in \bot\). Since \(S\in G\) and \(G\subseteq G''\), it follows that \(s\in G''\), hence \(ps\in \bot\).

Name: A topolinear space
Definition: \((P,\bot)\) a phase space
Page: 25
Chapter: 1
Section: 19
Kind: Def
Definition2: \(\mathbb F\) is closed under arbitrary with, in particular \(P\in\mathbb F\)
Conjdef: A 3-tuple \((P,\bot,\mathbb F)\) with a set \(\mathbb F\) of facts such that
Definition3: \(\mathbb F\) is closed under finite [$]\parr[/$], in particular \(\bot\in\mathbb F\)
Definition4: \(\bot\subseteq F\) for all \(F\subseteq\mathbb F\)
Definition5: [$]\parr[/$] is idempotent on \(\mathbb F\)

Name: The linear implication of \(G\) and \(H\)
Definition: \((G.H^\bot)^\bot\)
Page: 19, 20
Section: 1
Variables: \((P,\bot_P)\) a phase space
\(G,H\subseteq P\).
Notation: \(G\multimap H\)
Index: 8 (iii), 10
Kind: Def, Rem
Definition2: the set of \(p\in P\) such that, for all \(g\in G\), \(pg\in H\).

Smaller0: \(G^{\bot\bot}\)
Greater0: the smallest fact containing \(G\)
Page: 20
Section: 1
Variables: \((P,\bot_P)\) a phase space,
\(G\subseteq P\)
Index: 14
Smaller to greater: is equal to
Hide middle: yes

Definition: \(\top^\bot\)
Page: 18
Section: 1
Variables: \((P,\bot_P)\) a phase space
Notation: 0
Index: 5 (iv)
Kind: Ex
Definition2: the smallest fact w.r.t. inclusion
Applied to4: yes
French2: iff