Phase semantics for Classical Linear Logic

This file develops the phase semantics for Classical Linear Logic (CLL), providing an algebraic interpretation of linear logic propositions in terms of phase spaces.

Phase semantics is a denotational semantics for linear logic where propositions are interpreted as subsets of a commutative monoid, and logical operations correspond to specific set-theoretic operations.

Main definitions

• PhaseSpace: A commutative monoid equipped with a distinguished subset ⊥
• PhaseSpace.imp: Linear implication X ⊸ Y between sets in a phase space
• PhaseSpace.orthogonal: The orthogonal X⫠ of a set X
• PhaseSpace.isFact: A fact is a set that equals its biorthogonal closure
• Fact: The type of facts in a phase space
• PhaseSpace.FactExpr: Inductive type for representing operations on facts
• PhaseSpace.interpret: Interpretation of the connectives on facts
• PhaseSpace.interpProp: Interpretation of CLL propositions as facts in a phase space

Main results

• PhaseSpace.biorthogonalClosure: The biorthogonal operation forms a closure operator
• PhaseSpace.orth_iUnion: Orthogonal of union equals intersection of orthogonals
• PhaseSpace.sInf_isFact and PhaseSpace.inter_isFact_of_isFact: Facts are closed under intersections
• PhaseSpace.biorth_least_fact: The biorthogonal closure gives the smallest fact containing a set

Several lemmas about facts and orthogonality useful in the proof of soundness are proven here.

TODO

• Soundness theorem
• Completeness theorem

References

• J.-Y. Girard, Linear logic
• J.-Y. Girard, Linear Logic: its syntax and semantics

class Cslib.Logic.CLL.PhaseSpace (M : Type u) extends CommMonoid M : Type u

A phase space is a commutative monoid M equipped with a distinguished subset ⊥. This forms the algebraic foundation for interpreting linear logic propositions.

• mul : M → M → M
• mul_assoc (a b c : M) : a * b * c = a * (b * c)
• one : M
• one_mul (a : M) : 1 * a = a
• mul_one (a : M) : a * 1 = a
• npow : ℕ → M → M
• npow_zero (x : M) : Monoid.npow 0 x = 1
• npow_succ (n : ℕ) (x : M) : Monoid.npow (n + 1) x = Monoid.npow n x * x
• mul_comm (a b : M) : a * b = b * a
• bot : Set M

  The distinguished subset ⊥ used to define orthogonality

Basic operations

def Cslib.Logic.CLL.PhaseSpace.imp {M : Type u_2} [PhaseSpace M] (X Y : Set M) : Set M

Implication between two setsin a phase space: the set of elements m such that for all x ∈ X, we have m * x ∈ Y.

Equations

• Cslib.Logic.CLL.PhaseSpace.imp X Y = {m : M | ∀ x ∈ X, m * x ∈ Y}

def Cslib.Logic.CLL.PhaseSpace.orthogonal {P : Type u_1} [PhaseSpace P] (G : Set P) : Set P

The orthogonal X⫠ of a set X: the set of elements that map X into ⊥ under multiplication.

Equations

• Cslib.Logic.CLL.PhaseSpace.orthogonal G = Cslib.Logic.CLL.PhaseSpace.imp G Cslib.Logic.CLL.PhaseSpace.bot

def Cslib.Logic.CLL.PhaseSpace.«term_⫠» : Lean.TrailingParserDescr

The orthogonal X⫠ of a set X: the set of elements that map X into ⊥ under multiplication.

Equations

• Cslib.Logic.CLL.PhaseSpace.«term_⫠» = Lean.ParserDescr.trailingNode `Cslib.Logic.CLL.PhaseSpace.«term_⫠» 1024 1024 (Lean.ParserDescr.symbol "⫠")

Properties of orthogonality

@[simp]

theorem Cslib.Logic.CLL.PhaseSpace.orthogonal_def {P : Type u_1} [PhaseSpace P] (X : Set P) : orthogonal X = {m : P | ∀ x ∈ X, m * x ∈ bot}

theorem Cslib.Logic.CLL.PhaseSpace.orth_antitone {P : Type u_1} [PhaseSpace P] {X Y : Set P} (hXY : X ⊆ Y) : orthogonal Y ⊆ orthogonal X

The orthogonal operation is antitone: if X ⊆ Y then Y⫠ ⊆ X⫠.

theorem Cslib.Logic.CLL.PhaseSpace.orth_extensive {P : Type u_1} [PhaseSpace P] (X : Set P) : X ⊆ orthogonal (orthogonal X)

The biorthogonal operation is extensive: X ⊆ X⫠⫠ for any set X.

theorem Cslib.Logic.CLL.PhaseSpace.triple_orth {P : Type u_1} [PhaseSpace P] (X : Set P) : orthogonal (orthogonal (orthogonal X)) = orthogonal X

The triple orthogonal equals the orthogonal: X⫠⫠⫠ = X⫠.

theorem Cslib.Logic.CLL.PhaseSpace.triple_dual {P : Type u_1} [PhaseSpace P] {G : Set P} : orthogonal (orthogonal (orthogonal (orthogonal (orthogonal G)))) = orthogonal (orthogonal (orthogonal G))

def Cslib.Logic.CLL.PhaseSpace.biorthogonalClosure {P : Type u_1} [PhaseSpace P] : ClosureOperator (Set P)

The biorthogonal closure operator on sets in a phase space.

Equations

• One or more equations did not get rendered due to their size.

Basic theory of phase spaces

theorem Cslib.Logic.CLL.PhaseSpace.orth_iUnion {P : Type u_1} [PhaseSpace P] {ι : Sort u_2} (G : ι → Set P) : orthogonal (⋃ (i : ι), G i) = ⋂ (i : ι), orthogonal (G i)

Given a phase space (P, ⊥) and a set of subsets (Gᵢ)_{i ∈ I} of P, we have that (⋃ᵢ Gᵢ)⫠ = ⋂ᵢ Gᵢ⫠.

theorem Cslib.Logic.CLL.PhaseSpace.iInter_biorth_eq_orth_iUnion_orth {P : Type u_1} [PhaseSpace P] {ι : Sort u_2} (G : ι → Set P) : ⋂ (i : ι), orthogonal (orthogonal (G i)) = orthogonal (⋃ (i : ι), orthogonal (G i))

Given a phase space (P, ⊥) and a set of subsets (Gᵢ)_{i ∈ I} of P, we have that ∩ᵢ Gᵢ⫠⫠ = (∪ᵢ Gᵢ⫠)⫠.

Facts

def Cslib.Logic.CLL.PhaseSpace.isFact {P : Type u_1} [PhaseSpace P] (X : Set P) : Prop

A fact is a subset of a phase space that equals its biorthogonal closure.

Equations

• Cslib.Logic.CLL.PhaseSpace.isFact X = (X = Cslib.Logic.CLL.PhaseSpace.orthogonal (Cslib.Logic.CLL.PhaseSpace.orthogonal X))

structure Cslib.Logic.CLL.PhaseSpace.Fact (P : Type u_2) [PhaseSpace P] : Type u_2

The type of facts in a phase space.

• carrier : Set P

  The underlying set that is a fact

• property : isFact self.carrier

@[implicit_reducible]

instance Cslib.Logic.CLL.PhaseSpace.instSetLikeFact {P : Type u_1} [PhaseSpace P] : SetLike (Fact P) P

Equations

• Cslib.Logic.CLL.PhaseSpace.instSetLikeFact = { coe := Cslib.Logic.CLL.PhaseSpace.Fact.carrier, coe_injective' := ⋯ }

@[implicit_reducible]

instance Cslib.Logic.CLL.PhaseSpace.instPartialOrderFact {P : Type u_1} [PhaseSpace P] : PartialOrder (Fact P)

Equations

• Cslib.Logic.CLL.PhaseSpace.instPartialOrderFact = PartialOrder.ofSetLike (Cslib.Logic.CLL.PhaseSpace.Fact P) P

@[implicit_reducible]

instance Cslib.Logic.CLL.PhaseSpace.instHasSubsetFact {P : Type u_1} [PhaseSpace P] : HasSubset (Fact P)

Equations

• Cslib.Logic.CLL.PhaseSpace.instHasSubsetFact = { Subset := fun (A B : Cslib.Logic.CLL.PhaseSpace.Fact P) => ↑A ⊆ ↑B }

@[implicit_reducible]

instance Cslib.Logic.CLL.PhaseSpace.instCoeFactSet {M : Type u_2} [PhaseSpace M] : Coe (Fact M) (Set M)

Equations

• Cslib.Logic.CLL.PhaseSpace.instCoeFactSet = { coe := Cslib.Logic.CLL.PhaseSpace.Fact.carrier }

theorem Cslib.Logic.CLL.PhaseSpace.Fact.eq {P : Type u_1} [PhaseSpace P] (G : Fact P) : ↑G = orthogonal (orthogonal ↑G)

theorem Cslib.Logic.CLL.PhaseSpace.subset_dual_dual {P : Type u_1} [PhaseSpace P] {G : Set P} : G ⊆ orthogonal (orthogonal G)

theorem Cslib.Logic.CLL.PhaseSpace.mem_dual {P : Type u_1} [PhaseSpace P] {p : P} {G : Fact P} : p ∈ orthogonal ↑G ↔ ∀ q ∈ G, p * q ∈ bot

theorem Cslib.Logic.CLL.PhaseSpace.of_Fact {P : Type u_1} [PhaseSpace P] {G : Fact P} {p : P} (hp : ∀ (q : P), (∀ r ∈ G, q * r ∈ bot) → p * q ∈ bot) : p ∈ G

@[simp]

theorem Cslib.Logic.CLL.PhaseSpace.mem_carrier {P : Type u_1} [PhaseSpace P] (G : Fact P) : G.carrier = ↑G

def Cslib.Logic.CLL.PhaseSpace.Fact.mk_subset {P : Type u_1} [PhaseSpace P] (G : Set P) (h : orthogonal (orthogonal G) ⊆ G) : Fact P

Construct a fact from a set G and a proof that its biorthogonal closure is contained in G.

Equations

• Cslib.Logic.CLL.PhaseSpace.Fact.mk_subset G h = { carrier := G, property := ⋯ }

@[simp]

theorem Cslib.Logic.CLL.PhaseSpace.Fact.mk_subset_coe {P : Type u_1} [PhaseSpace P] (G : Set P) (h : orthogonal (orthogonal G) ⊆ G) : ↑(mk_subset G h) = G

theorem Cslib.Logic.CLL.PhaseSpace.dual_subset_dual {P : Type u_1} [PhaseSpace P] {G H : Set P} (h : G ⊆ H) : orthogonal H ⊆ orthogonal G

def Cslib.Logic.CLL.PhaseSpace.Fact.mk_dual {P : Type u_1} [PhaseSpace P] (G H : Set P) (h : G = orthogonal H) : Fact P

Construct a fact from a set G and a proof that G equals the orthogonal of some set H.

Equations

• Cslib.Logic.CLL.PhaseSpace.Fact.mk_dual G H h = Cslib.Logic.CLL.PhaseSpace.Fact.mk_subset G ⋯

@[simp]

theorem Cslib.Logic.CLL.PhaseSpace.Fact.mk_dual_coe {P : Type u_1} [PhaseSpace P] (G H : Set P) (h : G = orthogonal H) : ↑(mk_dual G H h) = G

theorem Cslib.Logic.CLL.PhaseSpace.coe_mk {P : Type u_1} [PhaseSpace P] {X : Set P} {h : isFact X} : ↑{ carrier := X, property := h } = X

@[simp]

theorem Cslib.Logic.CLL.PhaseSpace.closed {P : Type u_1} [PhaseSpace P] (F : Fact P) : isFact ↑F

theorem Cslib.Logic.CLL.PhaseSpace.orth_one_eq_bot {P : Type u_1} [PhaseSpace P] : orthogonal {1} = bot

In any phase space, {1}⫠ = ⊥.

def Cslib.Logic.CLL.PhaseSpace.dualFact {P : Type u_1} [PhaseSpace P] (G : Set P) : Fact P

The fact given by the dual of G.

Equations

• Cslib.Logic.CLL.PhaseSpace.dualFact G = Cslib.Logic.CLL.PhaseSpace.Fact.mk_dual (Cslib.Logic.CLL.PhaseSpace.orthogonal G) G ⋯

@[simp]

theorem Cslib.Logic.CLL.PhaseSpace.dualFact_coe {P : Type u_1} [PhaseSpace P] (G : Set P) : ↑(dualFact G) = {m : P | ∀ x ∈ G, m * x ∈ bot}

theorem Cslib.Logic.CLL.PhaseSpace.dual_dual_subset_Fact_iff {P : Type u_1} [PhaseSpace P] {G : Set P} {H : Fact P} : orthogonal (orthogonal G) ⊆ ↑H ↔ G ⊆ ↑H

theorem Cslib.Logic.CLL.PhaseSpace.dual_dual_subset_dual_iff {P : Type u_1} [PhaseSpace P] {G H : Set P} : orthogonal (orthogonal G) ⊆ orthogonal H ↔ G ⊆ orthogonal H

@[implicit_reducible]

instance Cslib.Logic.CLL.PhaseSpace.instOneFact {P : Type u_1} [PhaseSpace P] : One (Fact P)

Equations

• Cslib.Logic.CLL.PhaseSpace.instOneFact = { one := Cslib.Logic.CLL.PhaseSpace.dualFact Cslib.Logic.CLL.PhaseSpace.bot }

@[simp]

theorem Cslib.Logic.CLL.PhaseSpace.coe_one {P : Type u_1} [PhaseSpace P] : ↑1 = orthogonal bot

@[simp]

theorem Cslib.Logic.CLL.PhaseSpace.mem_one {P : Type u_1} [PhaseSpace P] {p : P} : p ∈ 1 ↔ ∀ q ∈ bot, p * q ∈ bot

theorem Cslib.Logic.CLL.PhaseSpace.one_mem_one {P : Type u_1} [PhaseSpace P] : 1 ∈ 1

theorem Cslib.Logic.CLL.PhaseSpace.mul_mem_one {P : Type u_1} [PhaseSpace P] {p q : P} (hp : p ∈ 1) (hq : q ∈ 1) : p * q ∈ 1

@[implicit_reducible]

instance Cslib.Logic.CLL.PhaseSpace.instTopFact {P : Type u_1} [PhaseSpace P] : Top (Fact P)

Equations

• Cslib.Logic.CLL.PhaseSpace.instTopFact = { top := Cslib.Logic.CLL.PhaseSpace.Fact.mk_subset Set.univ ⋯ }

@[simp]

theorem Cslib.Logic.CLL.PhaseSpace.coe_top {P : Type u_1} [PhaseSpace P] : ↑⊤ = Set.univ

@[simp]

theorem Cslib.Logic.CLL.PhaseSpace.mem_top {P : Type u_1} [PhaseSpace P] {x : P} : x ∈ ⊤

theorem Cslib.Logic.CLL.PhaseSpace.dual_empty {P : Type u_1} [PhaseSpace P] : orthogonal ∅ = Set.univ

@[simp]

theorem Cslib.Logic.CLL.PhaseSpace.dualFact_empty {P : Type u_1} [PhaseSpace P] : dualFact ∅ = ⊤

@[implicit_reducible]

instance Cslib.Logic.CLL.PhaseSpace.instZeroFact {P : Type u_1} [PhaseSpace P] : Zero (Fact P)

Equations

• Cslib.Logic.CLL.PhaseSpace.instZeroFact = { zero := Cslib.Logic.CLL.PhaseSpace.dualFact ⊤ }

@[simp]

theorem Cslib.Logic.CLL.PhaseSpace.coe_zero {P : Type u_1} [PhaseSpace P] : ↑0 = orthogonal Set.univ

theorem Cslib.Logic.CLL.PhaseSpace.mem_zero {P : Type u_1} [PhaseSpace P] {p : P} : p ∈ 0 ↔ ∀ (q : P), p * q ∈ bot

@[implicit_reducible]

instance Cslib.Logic.CLL.PhaseSpace.instBotFact {P : Type u_1} [PhaseSpace P] : Bot (Fact P)

Equations

• Cslib.Logic.CLL.PhaseSpace.instBotFact = { bot := Cslib.Logic.CLL.PhaseSpace.Fact.mk_dual Cslib.Logic.CLL.PhaseSpace.bot {1} ⋯ }

theorem Cslib.Logic.CLL.PhaseSpace.biorth_least_fact {P : Type u_1} [PhaseSpace P] (G : Set P) {F : Set P} : isFact F → G ⊆ F → orthogonal (orthogonal G) ⊆ F

In a phase space, G⫠⫠ is the smallest fact containing G.

theorem Cslib.Logic.CLL.PhaseSpace.zero_least_fact {P : Type u_1} [PhaseSpace P] {F : Set P} : isFact F → Fact.carrier 0 ⊆ F

0 is the least fact (w.r.t. inclusion).

theorem Cslib.Logic.CLL.PhaseSpace.isFact_iff_closed {P : Type u_1} [PhaseSpace P] (X : Set P) : isFact X ↔ biorthogonalClosure.IsClosed X

theorem Cslib.Logic.CLL.PhaseSpace.sInf_isFact {P : Type u_1} [PhaseSpace P] {S : Set (Fact P)} : isFact (sInf ((fun (F : Fact P) => ↑F) '' S))

Arbitrary intersections of facts are facts.

def Cslib.Logic.CLL.PhaseSpace.carriersInf {P : Type u_1} [PhaseSpace P] (S : Set (Fact P)) : Set P

Intersection of the carriers of a set of facts.

Equations

• Cslib.Logic.CLL.PhaseSpace.carriersInf S = sInf ((fun (F : Cslib.Logic.CLL.PhaseSpace.Fact P) => ↑F) '' S)

theorem Cslib.Logic.CLL.PhaseSpace.inter_isFact_of_isFact {P : Type u_1} [PhaseSpace P] {A B : Set P} (hA : isFact A) (hB : isFact B) : isFact (A ∩ B)

Binary intersections of facts are facts.

@[implicit_reducible]

instance Cslib.Logic.CLL.PhaseSpace.instInfSetFact {P : Type u_1} [PhaseSpace P] : InfSet (Fact P)

Equations

• Cslib.Logic.CLL.PhaseSpace.instInfSetFact = { sInf := fun (S : Set (Cslib.Logic.CLL.PhaseSpace.Fact P)) => { carrier := Cslib.Logic.CLL.PhaseSpace.carriersInf S, property := ⋯ } }

theorem Cslib.Logic.CLL.PhaseSpace.iInter_eq_sInf_image {P : Type u_1} {α : Type u_2} (S : Set α) (f : α → Set P) : ⋂ x ∈ S, f x = sInf (f '' S)

@[simp]

theorem Cslib.Logic.CLL.PhaseSpace.inter_eq_orth_union_orth {P : Type u_1} [PhaseSpace P] (G H : Fact P) : ↑G ∩ ↑H = orthogonal (orthogonal ↑G ∪ orthogonal ↑H)

@[implicit_reducible]

instance Cslib.Logic.CLL.PhaseSpace.instMinFact {P : Type u_1} [PhaseSpace P] : Min (Fact P)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Cslib.Logic.CLL.PhaseSpace.coe_min {P : Type u_1} [PhaseSpace P] {G H : Fact P} : ↑(G ⊓ H) = ↑G ∩ ↑H

def Cslib.Logic.CLL.PhaseSpace.idempotentsIn {M : Type u_2} [Monoid M] (X : Set M) : Set M

The idempotent elements within a given set X.

Equations

• Cslib.Logic.CLL.PhaseSpace.idempotentsIn X = {m : M | IsIdempotentElem m ∧ m ∈ X}

def Cslib.Logic.CLL.PhaseSpace.I {P : Type u_1} [PhaseSpace P] : Set P

The set I of idempotents that "belong to 1" in the phase semantics.

Equations

• Cslib.Logic.CLL.PhaseSpace.I = Cslib.Logic.CLL.PhaseSpace.idempotentsIn 1

Interpretation of the connectives

def Cslib.Logic.CLL.PhaseSpace.Fact.neg {P : Type u_1} [PhaseSpace P] (G : Fact P) : Fact P

Linear negation of a fact, given by taking its orthogonal.

Equations

• Gᗮ = Cslib.Logic.CLL.PhaseSpace.dualFact ↑G

def Cslib.Logic.CLL.PhaseSpace.Fact.«term_ᗮ» : Lean.TrailingParserDescr

Linear negation of a fact, given by taking its orthogonal.

Equations

• Cslib.Logic.CLL.PhaseSpace.Fact.«term_ᗮ» = Lean.ParserDescr.trailingNode `Cslib.Logic.CLL.PhaseSpace.Fact.«term_ᗮ» 1024 1024 (Lean.ParserDescr.symbol "ᗮ")

@[simp]

theorem Cslib.Logic.CLL.PhaseSpace.Fact.coe_neg {P : Type u_1} [PhaseSpace P] {G : Fact P} : ↑Gᗮ = orthogonal ↑G

@[simp]

theorem Cslib.Logic.CLL.PhaseSpace.Fact.neg_neg {P : Type u_1} [PhaseSpace P] {G : Fact P} : Gᗮᗮ = G

@[simp]

theorem Cslib.Logic.CLL.PhaseSpace.Fact.neg_bot {P : Type u_1} [PhaseSpace P] : ⊥ᗮ = 1

@[simp]

theorem Cslib.Logic.CLL.PhaseSpace.Fact.neg_one {P : Type u_1} [PhaseSpace P] : 1ᗮ = ⊥

@[simp]

theorem Cslib.Logic.CLL.PhaseSpace.Fact.neg_top {P : Type u_1} [PhaseSpace P] : ⊤ᗮ = 0

@[simp]

theorem Cslib.Logic.CLL.PhaseSpace.Fact.neg_zero {P : Type u_1} [PhaseSpace P] : 0ᗮ = ⊤

theorem Cslib.Logic.CLL.PhaseSpace.Fact.neg_eq_iff {P : Type u_1} [PhaseSpace P] {G H : Fact P} : Gᗮ = H ↔ G = Hᗮ

@[simp]

theorem Cslib.Logic.CLL.PhaseSpace.Fact.neg_involutive {P : Type u_1} [PhaseSpace P] : Function.Involutive neg

@[simp]

theorem Cslib.Logic.CLL.PhaseSpace.Fact.neg_surjective {P : Type u_1} [PhaseSpace P] : Function.Surjective neg

theorem Cslib.Logic.CLL.PhaseSpace.Fact.neg_injective {P : Type u_1} [PhaseSpace P] : Function.Injective neg

@[simp]

theorem Cslib.Logic.CLL.PhaseSpace.Fact.neg_inj {P : Type u_1} [PhaseSpace P] {G H : Fact P} : Gᗮ = Hᗮ ↔ G = H

def Cslib.Logic.CLL.PhaseSpace.Fact.tensor {P : Type u_1} [PhaseSpace P] (X Y : Fact P) : Fact P

The tensor product X ⊗ Y of two facts, defined as the dual of the orthogonal of the pointwise product.

Equations

• X ⊗ Y = Cslib.Logic.CLL.PhaseSpace.dualFact (Cslib.Logic.CLL.PhaseSpace.orthogonal (↑X * ↑Y))

def Cslib.Logic.CLL.PhaseSpace.Fact.«term_⊗_» : Lean.TrailingParserDescr

The tensor product X ⊗ Y of two facts, defined as the dual of the orthogonal of the pointwise product.

Equations

• One or more equations did not get rendered due to their size.

def Cslib.Logic.CLL.PhaseSpace.Fact.parr {P : Type u_1} [PhaseSpace P] (X Y : Fact P) : Fact P

The par (multiplicative disjunction) X ⅋ Y of two facts, defined as the dual of the pointwise product of the orthogonals.

Equations

• X ⅋ Y = Cslib.Logic.CLL.PhaseSpace.dualFact (Cslib.Logic.CLL.PhaseSpace.orthogonal ↑X * Cslib.Logic.CLL.PhaseSpace.orthogonal ↑Y)

def Cslib.Logic.CLL.PhaseSpace.Fact.term_⅋_ : Lean.TrailingParserDescr

The par (multiplicative disjunction) X ⅋ Y of two facts, defined as the dual of the pointwise product of the orthogonals.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Cslib.Logic.CLL.PhaseSpace.Fact.one_tensor {P : Type u_1} [PhaseSpace P] {G : Fact P} : 1 ⊗ G = G

theorem Cslib.Logic.CLL.PhaseSpace.Fact.tensor_comm {P : Type u_1} [PhaseSpace P] {X Y : Fact P} : X ⊗ Y = Y ⊗ X

@[simp]

theorem Cslib.Logic.CLL.PhaseSpace.Fact.tensor_one {P : Type u_1} [PhaseSpace P] {G : Fact P} : G ⊗ 1 = G

theorem Cslib.Logic.CLL.PhaseSpace.Fact.tensor_assoc_aux {P : Type u_1} [PhaseSpace P] {F G : Set P} : orthogonal (orthogonal F) * orthogonal (orthogonal G) ⊆ orthogonal (orthogonal (F * G))

theorem Cslib.Logic.CLL.PhaseSpace.Fact.coe_tensor_assoc {P : Type u_1} [PhaseSpace P] {G H K : Fact P} : ↑((G ⊗ H) ⊗ K) = orthogonal (orthogonal (↑G * (↑H * ↑K)))

@[simp]

theorem Cslib.Logic.CLL.PhaseSpace.Fact.tensor_assoc {P : Type u_1} [PhaseSpace P] {G H K : Fact P} : (G ⊗ H) ⊗ K = G ⊗ H ⊗ K

theorem Cslib.Logic.CLL.PhaseSpace.Fact.tensor_rotate {P : Type u_1} [PhaseSpace P] {G H K : Fact P} : G ⊗ H ⊗ K = H ⊗ K ⊗ G

theorem Cslib.Logic.CLL.PhaseSpace.Fact.tensor_le_tensor {P : Type u_1} [PhaseSpace P] {G K H L : Fact P} (hGK : G ≤ K) (hHL : H ≤ L) : G ⊗ H ≤ K ⊗ L

theorem Cslib.Logic.CLL.PhaseSpace.Fact.tensor_of_par {P : Type u_1} [PhaseSpace P] {G H : Fact P} : G ⊗ H = (Gᗮ ⅋ Hᗮ)ᗮ

theorem Cslib.Logic.CLL.PhaseSpace.Fact.par_of_tensor {P : Type u_1} [PhaseSpace P] {G H : Fact P} : G ⅋ H = (Gᗮ ⊗ Hᗮ)ᗮ

theorem Cslib.Logic.CLL.PhaseSpace.Fact.par_le_par {P : Type u_1} [PhaseSpace P] {G H K L : Fact P} (hGK : G ≤ K) (hHL : H ≤ L) : G ⅋ H ≤ K ⅋ L

@[simp]

theorem Cslib.Logic.CLL.PhaseSpace.Fact.bot_par {P : Type u_1} [PhaseSpace P] {G : Fact P} : ⊥ ⅋ G = G

@[simp]

theorem Cslib.Logic.CLL.PhaseSpace.Fact.par_bot {P : Type u_1} [PhaseSpace P] {G : Fact P} : G ⅋ ⊥ = G

@[simp]

theorem Cslib.Logic.CLL.PhaseSpace.Fact.par_assoc {P : Type u_1} [PhaseSpace P] {G H K : Fact P} : (G ⅋ H) ⅋ K = G ⅋ H ⅋ K

theorem Cslib.Logic.CLL.PhaseSpace.Fact.par_comm {P : Type u_1} [PhaseSpace P] (G H : Fact P) : G ⅋ H = H ⅋ G

def Cslib.Logic.CLL.PhaseSpace.Fact.linImpl {P : Type u_1} [PhaseSpace P] (X Y : Fact P) : Fact P

Linear implication between facts, defined as the dual of the orthogonal of the pointwise product.

Equations

• X ⊸ Y = Cslib.Logic.CLL.PhaseSpace.dualFact (↑X * Cslib.Logic.CLL.PhaseSpace.orthogonal ↑Y)

def Cslib.Logic.CLL.PhaseSpace.Fact.«term_⊸_» : Lean.TrailingParserDescr

Linear implication between facts, defined as the dual of the orthogonal of the pointwise product.

Equations

• One or more equations did not get rendered due to their size.

theorem Cslib.Logic.CLL.PhaseSpace.Fact.linImpl_of_tensor {P : Type u_1} [PhaseSpace P] {G H : Fact P} : G ⊸ H = (G ⊗ Hᗮ)ᗮ

theorem Cslib.Logic.CLL.PhaseSpace.Fact.par_of_linImpl {P : Type u_1} [PhaseSpace P] {G H : Fact P} : G ⅋ H = Gᗮ ⊸ H

theorem Cslib.Logic.CLL.PhaseSpace.Fact.tensor_of_linImpl {P : Type u_1} [PhaseSpace P] {G H : Fact P} : G ⊗ H = (G ⊸ Hᗮ)ᗮ

theorem Cslib.Logic.CLL.PhaseSpace.Fact.linImpl_of_par {P : Type u_1} [PhaseSpace P] {G H : Fact P} : G ⊸ H = Gᗮ ⅋ H

theorem Cslib.Logic.CLL.PhaseSpace.Fact.neg_tensor {P : Type u_1} [PhaseSpace P] {G H : Fact P} : (G ⊗ H)ᗮ = Gᗮ ⅋ Hᗮ

theorem Cslib.Logic.CLL.PhaseSpace.Fact.neg_par {P : Type u_1} [PhaseSpace P] {G H : Fact P} : (G ⅋ H)ᗮ = Gᗮ ⊗ Hᗮ

theorem Cslib.Logic.CLL.PhaseSpace.Fact.mul_subset_tensor {P : Type u_1} [PhaseSpace P] {G H : Fact P} : ↑G * ↑H ⊆ ↑(G ⊗ H)

@[simp]

theorem Cslib.Logic.CLL.PhaseSpace.Fact.one_linImpl {P : Type u_1} [PhaseSpace P] {G : Fact P} : 1 ⊸ G = G

@[simp]

theorem Cslib.Logic.CLL.PhaseSpace.Fact.linImpl_bot {P : Type u_1} [PhaseSpace P] {G : Fact P} : G ⊸ ⊥ = Gᗮ

@[simp]

theorem Cslib.Logic.CLL.PhaseSpace.Fact.tensor_linImpl {P : Type u_1} [PhaseSpace P] {G H K : Fact P} : G ⊗ H ⊸ K = G ⊸ (H ⊸ K)

theorem Cslib.Logic.CLL.PhaseSpace.Fact.linImpl_par {P : Type u_1} [PhaseSpace P] {G H K : Fact P} : G ⊸ H ⅋ K = (G ⊸ H) ⅋ K

theorem Cslib.Logic.CLL.PhaseSpace.Fact.linImpl_par' {P : Type u_1} [PhaseSpace P] {G H K : Fact P} : G ⊸ H ⅋ K = H ⅋ (G ⊸ K)

@[simp]

theorem Cslib.Logic.CLL.PhaseSpace.Fact.neg_linImpl_neg {P : Type u_1} [PhaseSpace P] {G H : Fact P} : Gᗮ ⊸ Hᗮ = H ⊸ G

theorem Cslib.Logic.CLL.PhaseSpace.Fact.linImpl_iff_implies {P : Type u_1} [PhaseSpace P] {p : P} {G H : Fact P} : p ∈ G ⊸ H ↔ imp (↑G) (↑H) p

def Cslib.Logic.CLL.PhaseSpace.Fact.withh {P : Type u_1} [PhaseSpace P] (X Y : Fact P) : Fact P

The with (additive conjunction) X & Y of two facts, defined as the intersection of the two facts.

Equations

• X & Y = X ⊓ Y

def Cslib.Logic.CLL.PhaseSpace.Fact.«term_&_» : Lean.TrailingParserDescr

The with (additive conjunction) X & Y of two facts, defined as the intersection of the two facts.

Equations

• One or more equations did not get rendered due to their size.

def Cslib.Logic.CLL.PhaseSpace.Fact.oplus {P : Type u_1} [PhaseSpace P] (X Y : Fact P) : Fact P

The oplus (additive disjunction) X ⊕ Y of two facts, defined as the dual of the orthogonal of the union.

Equations

• X ⊕ Y = Cslib.Logic.CLL.PhaseSpace.dualFact (Cslib.Logic.CLL.PhaseSpace.orthogonal (↑X ∪ ↑Y))

def Cslib.Logic.CLL.PhaseSpace.Fact.«term_⊕_» : Lean.TrailingParserDescr

The oplus (additive disjunction) X ⊕ Y of two facts, defined as the dual of the orthogonal of the union.

Equations

• One or more equations did not get rendered due to their size.

def Cslib.Logic.CLL.PhaseSpace.Fact.bang {P : Type u_1} [PhaseSpace P] (X : Fact P) : Fact P

The exponential !X (of course) of a fact, defined as the dual of the orthogonal of the intersection with the idempotents.

Equations

• ! X = Cslib.Logic.CLL.PhaseSpace.dualFact (Cslib.Logic.CLL.PhaseSpace.orthogonal (↑X ∩ Cslib.Logic.CLL.PhaseSpace.I))

def Cslib.Logic.CLL.PhaseSpace.Fact.term!_ : Lean.ParserDescr

The exponential !X (of course) of a fact, defined as the dual of the orthogonal of the intersection with the idempotents.

Equations

• One or more equations did not get rendered due to their size.

def Cslib.Logic.CLL.PhaseSpace.Fact.quest {P : Type u_1} [PhaseSpace P] (X : Fact P) : Fact P

The exponential ?X (why not) of a fact, defined as the dual of the intersection of the orthogonal with the idempotents.

Equations

• ʔ X = Cslib.Logic.CLL.PhaseSpace.dualFact (Cslib.Logic.CLL.PhaseSpace.orthogonal ↑X ∩ Cslib.Logic.CLL.PhaseSpace.I)

def Cslib.Logic.CLL.PhaseSpace.Fact.«termʔ_» : Lean.ParserDescr

The exponential ?X (why not) of a fact, defined as the dual of the intersection of the orthogonal with the idempotents.

Equations

• One or more equations did not get rendered due to their size.

Properties of Additives

theorem Cslib.Logic.CLL.PhaseSpace.Fact.plus_eq_with_dual {P : Type u_1} [PhaseSpace P] {G H : Fact P} : G ⊕ H = (Gᗮ & Hᗮ)ᗮ

theorem Cslib.Logic.CLL.PhaseSpace.Fact.with_eq_plus_dual {P : Type u_1} [PhaseSpace P] {G H : Fact P} : G & H = (Gᗮ ⊕ Hᗮ)ᗮ

theorem Cslib.Logic.CLL.PhaseSpace.Fact.neg_plus {P : Type u_1} [PhaseSpace P] {G H : Fact P} : (G ⊕ H)ᗮ = Gᗮ & Hᗮ

theorem Cslib.Logic.CLL.PhaseSpace.Fact.neg_with {P : Type u_1} [PhaseSpace P] {G H : Fact P} : (G & H)ᗮ = Gᗮ ⊕ Hᗮ

theorem Cslib.Logic.CLL.PhaseSpace.Fact.with_comm {P : Type u_1} [PhaseSpace P] {G H : Fact P} : G & H = H & G

@[simp]

theorem Cslib.Logic.CLL.PhaseSpace.Fact.with_assoc {P : Type u_1} [PhaseSpace P] {G H K : Fact P} : (G & H) & K = G & (H & K)

@[simp]

theorem Cslib.Logic.CLL.PhaseSpace.Fact.top_with {P : Type u_1} [PhaseSpace P] {G : Fact P} : ⊤ & G = G

@[simp]

theorem Cslib.Logic.CLL.PhaseSpace.Fact.with_top {P : Type u_1} [PhaseSpace P] {G : Fact P} : G & ⊤ = G

theorem Cslib.Logic.CLL.PhaseSpace.Fact.plus_comm {P : Type u_1} [PhaseSpace P] {G H : Fact P} : G ⊕ H = H ⊕ G

@[simp]

theorem Cslib.Logic.CLL.PhaseSpace.Fact.plus_assoc {P : Type u_1} [PhaseSpace P] {G H K : Fact P} : (G ⊕ H) ⊕ K = G ⊕ (H ⊕ K)

@[simp]

theorem Cslib.Logic.CLL.PhaseSpace.Fact.zero_plus {P : Type u_1} [PhaseSpace P] {G : Fact P} : 0 ⊕ G = G

@[simp]

theorem Cslib.Logic.CLL.PhaseSpace.Fact.plus_zero {P : Type u_1} [PhaseSpace P] {G : Fact P} : G ⊕ 0 = G

Distributivity Properties

theorem Cslib.Logic.CLL.PhaseSpace.Fact.le_plus_left {P : Type u_1} [PhaseSpace P] {G H : Fact P} : G ≤ G ⊕ H

theorem Cslib.Logic.CLL.PhaseSpace.Fact.le_plus_right {P : Type u_1} [PhaseSpace P] {G H : Fact P} : H ≤ G ⊕ H

theorem Cslib.Logic.CLL.PhaseSpace.Fact.tensor_distrib_plus {P : Type u_1} [PhaseSpace P] {G H K : Fact P} : G ⊗ (H ⊕ K) = G ⊗ H ⊕ G ⊗ K

theorem Cslib.Logic.CLL.PhaseSpace.Fact.plus_tensor_distrib {P : Type u_1} [PhaseSpace P] {H K G : Fact P} : (H ⊕ K) ⊗ G = H ⊗ G ⊕ K ⊗ G

theorem Cslib.Logic.CLL.PhaseSpace.Fact.par_distrib_with {P : Type u_1} [PhaseSpace P] {G H K : Fact P} : G ⅋ (H & K) = G ⅋ H & G ⅋ K

theorem Cslib.Logic.CLL.PhaseSpace.Fact.with_par_distrib {P : Type u_1} [PhaseSpace P] {H K G : Fact P} : (H & K) ⅋ G = H ⅋ G & K ⅋ G

theorem Cslib.Logic.CLL.PhaseSpace.Fact.tensor_semi_distrib_with {P : Type u_1} [PhaseSpace P] {G H K : Fact P} : G ⊗ (H & K) ≤ G ⊗ H & G ⊗ K

theorem Cslib.Logic.CLL.PhaseSpace.Fact.with_tensor_semi_distrib {P : Type u_1} [PhaseSpace P] {G H K : Fact P} : (G & H) ⊗ K ≤ G ⊗ K & H ⊗ K

theorem Cslib.Logic.CLL.PhaseSpace.Fact.neg_le_neg_iff {P : Type u_1} [PhaseSpace P] {G H : Fact P} : Gᗮ ≤ Hᗮ ↔ H ≤ G

theorem Cslib.Logic.CLL.PhaseSpace.Fact.par_semi_distrib_plus {P : Type u_1} [PhaseSpace P] {G H K : Fact P} : G ⅋ H ⊕ G ⅋ K ≤ G ⅋ (H ⊕ K)

Absorption Properties

@[simp]

theorem Cslib.Logic.CLL.PhaseSpace.Fact.top_par {P : Type u_1} [PhaseSpace P] {G : Fact P} : ⊤ ⅋ G = ⊤

@[simp]

theorem Cslib.Logic.CLL.PhaseSpace.Fact.par_top {P : Type u_1} [PhaseSpace P] {G : Fact P} : G ⅋ ⊤ = ⊤

@[simp]

theorem Cslib.Logic.CLL.PhaseSpace.Fact.zero_tensor {P : Type u_1} [PhaseSpace P] {G : Fact P} : 0 ⊗ G = 0

@[simp]

theorem Cslib.Logic.CLL.PhaseSpace.Fact.tensor_zero {P : Type u_1} [PhaseSpace P] {G : Fact P} : G ⊗ 0 = 0

Entailment Distributivity

@[simp]

theorem Cslib.Logic.CLL.PhaseSpace.Fact.plus_entails {P : Type u_1} [PhaseSpace P] {G H K : Fact P} : G ⊕ H ⊸ K = (G ⊸ K) & (H ⊸ K)

@[simp]

theorem Cslib.Logic.CLL.PhaseSpace.Fact.entails_with {P : Type u_1} [PhaseSpace P] {G H K : Fact P} : G ⊸ H & K = (G ⊸ H) & (G ⊸ K)

@[simp]

theorem Cslib.Logic.CLL.PhaseSpace.Fact.zero_entails {P : Type u_1} [PhaseSpace P] {G : Fact P} : 0 ⊸ G = ⊤

@[simp]

theorem Cslib.Logic.CLL.PhaseSpace.Fact.entails_top {P : Type u_1} [PhaseSpace P] {G : Fact P} : G ⊸ ⊤ = ⊤

@[reducible, inline]

abbrev Cslib.Logic.CLL.PhaseSpace.Fact.IsValid {P : Type u_1} [PhaseSpace P] (G : Fact P) : Prop

A fact G is valid if the unit 1 belongs to G.

Equations

• G.IsValid = (1 ∈ G)

theorem Cslib.Logic.CLL.PhaseSpace.Fact.valid_with {P : Type u_1} [PhaseSpace P] {G H : Fact P} : (G & H).IsValid ↔ G.IsValid ∧ H.IsValid

Interpretation of propositions

def Cslib.Logic.CLL.PhaseSpace.interpProp {M : Type u_2} {Atom : Type u_3} [PhaseSpace M] (v : Atom → Fact M) : Proposition Atom → Fact M

The interpretation of a CLL proposition in a phase space, given a valuation of atoms to facts.

Equations

• Cslib.Logic.CLL.PhaseSpace.interpProp v (Cslib.Logic.CLL.Proposition.atom a) = v a
• Cslib.Logic.CLL.PhaseSpace.interpProp v (Cslib.Logic.CLL.Proposition.atomDual a) = (v a)ᗮ
• Cslib.Logic.CLL.PhaseSpace.interpProp v Cslib.Logic.CLL.Proposition.one = 1
• Cslib.Logic.CLL.PhaseSpace.interpProp v Cslib.Logic.CLL.Proposition.zero = 0
• Cslib.Logic.CLL.PhaseSpace.interpProp v Cslib.Logic.CLL.Proposition.top = ⊤
• Cslib.Logic.CLL.PhaseSpace.interpProp v Cslib.Logic.CLL.Proposition.bot = ⊥
• Cslib.Logic.CLL.PhaseSpace.interpProp v (A.tensor B) = Cslib.Logic.CLL.PhaseSpace.interpProp v A ⊗ Cslib.Logic.CLL.PhaseSpace.interpProp v B
• Cslib.Logic.CLL.PhaseSpace.interpProp v (A.parr B) = Cslib.Logic.CLL.PhaseSpace.interpProp v A ⅋ Cslib.Logic.CLL.PhaseSpace.interpProp v B
• Cslib.Logic.CLL.PhaseSpace.interpProp v (A.with B) = Cslib.Logic.CLL.PhaseSpace.interpProp v A & Cslib.Logic.CLL.PhaseSpace.interpProp v B
• Cslib.Logic.CLL.PhaseSpace.interpProp v (A.oplus B) = Cslib.Logic.CLL.PhaseSpace.interpProp v A ⊕ Cslib.Logic.CLL.PhaseSpace.interpProp v B
• Cslib.Logic.CLL.PhaseSpace.interpProp v A.bang = ! Cslib.Logic.CLL.PhaseSpace.interpProp v A
• Cslib.Logic.CLL.PhaseSpace.interpProp v A.quest = ʔ Cslib.Logic.CLL.PhaseSpace.interpProp v A

def Cslib.Logic.CLL.PhaseSpace.«term⟦_⟧_» : Lean.ParserDescr

The interpretation of a CLL proposition in a phase space, given a valuation of atoms to facts.

Equations

• One or more equations did not get rendered due to their size.