Forcing relation

class LO.ForcingRelation (W : Type u_1) (F : outParam (Type u_2)) : Type (max u_1 u_2)

• Forces : W → F → Prop

def LO.«term_⊩_» : Lean.TrailingParserDescr

Equations

• LO.«term_⊩_» = Lean.ParserDescr.trailingNode `LO.«term_⊩_» 45 46 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊩ ") (Lean.ParserDescr.cat `term 46))

class LO.ForcingExists (W : Type u_1) (α : outParam (Type u_2)) : Type (max u_1 u_2)

• Forces : W → α → Prop

def LO.«term_⊩↓_» : Lean.TrailingParserDescr

Equations

• LO.«term_⊩↓_» = Lean.ParserDescr.trailingNode `LO.«term_⊩↓_» 45 46 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊩↓ ") (Lean.ParserDescr.cat `term 46))

@[reducible, inline]

abbrev LO.ForcingRelation.NotForces {W : Type u_1} {F : Type u_2} [ForcingRelation W F] (w : W) (φ : F) : Prop

Equations

• (w ⊮ φ) = ¬w ⊩ φ

def LO.ForcingRelation.«term_⊮_» : Lean.TrailingParserDescr

Equations

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

class LO.ForcingRelation.BasicSemantics (W : Type u_1) {F : Type u_2} [ForcingRelation W F] [LogicalConnective F] : Prop

• verum (w : W) : w ⊩ ⊤
• and {φ ψ : F} (w : W) : w ⊩ φ ⋏ ψ ↔ w ⊩ φ ∧ w ⊩ ψ
• or {φ ψ : F} (w : W) : w ⊩ φ ⋎ ψ ↔ w ⊩ φ ∨ w ⊩ ψ

class LO.ForcingRelation.Monotone (W : Type u_1) {F : Type u_2} [ForcingRelation W F] (R : outParam (W → W → Prop)) : Prop

• monotone {φ : F} {w : W} : w ⊩ φ → ∀ (v : W), R w v → v ⊩ φ

class LO.ForcingRelation.IntKripke (W : Type u_1) {F : Type u_2} [ForcingRelation W F] [LogicalConnective F] (R : outParam (W → W → Prop)) extends LO.ForcingRelation.BasicSemantics W, LO.ForcingRelation.Monotone W R : Prop

• verum (w : W) : w ⊩ ⊤
• and {φ ψ : F} (w : W) : w ⊩ φ ⋏ ψ ↔ w ⊩ φ ∧ w ⊩ ψ
• or {φ ψ : F} (w : W) : w ⊩ φ ⋎ ψ ↔ w ⊩ φ ∨ w ⊩ ψ
• monotone {φ : F} {w : W} : w ⊩ φ → ∀ (v : W), R w v → v ⊩ φ
• imply {φ ψ : F} (w : W) : w ⊩ φ 🡒 ψ ↔ ∀ (v : W), R w v → v ⊩ φ → v ⊩ ψ
• falsum (w : W) : ¬w ⊩ ⊥
• not {φ : F} (w : W) : w ⊩ ∼φ ↔ ∀ (v : W), R w v → ¬v ⊩ φ

@[simp]

theorem LO.ForcingRelation.iff {W : Type u_1} {F : Type u_2} [ForcingRelation W F] [LogicalConnective F] {w : W} {φ ψ : F} (R : W → W → Prop) [IntKripke W R] : w ⊩ φ 🡘 ψ ↔ ∀ (v : W), R w v → (v ⊩ φ ↔ v ⊩ ψ)

@[reducible, inline]

abbrev LO.ForcingRelation.AllForces (W : Type u_1) {F : Type u_2} [ForcingRelation W F] (φ : F) : Prop

Equations

• (W ∀⊩ φ) = ∀ (w : W), w ⊩ φ

def LO.ForcingRelation.«term_∀⊩_» : Lean.TrailingParserDescr

Equations

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

@[reducible, inline]

abbrev LO.ForcingRelation.AllForcesSet (W : Type u_1) {F : Type u_2} [ForcingRelation W F] {S : Type u_3} (s : S) [AdjunctiveSet F S] : Prop

Equations

• (W ∀⊩* s) = ∀ φ ∈ s, W ∀⊩ φ

def LO.ForcingRelation.«term_∀⊩*_» : Lean.TrailingParserDescr

Equations

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

@[simp]

theorem LO.ForcingRelation.AllForces.verum {W : Type u_1} {F : Type u_2} [ForcingRelation W F] [LogicalConnective F] [BasicSemantics W] : W ∀⊩ ⊤

@[simp]

theorem LO.ForcingRelation.AllForces.and {W : Type u_1} {F : Type u_2} [ForcingRelation W F] [LogicalConnective F] {φ ψ : F} [BasicSemantics W] : W ∀⊩ φ ⋏ ψ ↔ W ∀⊩ φ ∧ W ∀⊩ ψ

Forcing relation for classical logic

class LO.WeakForcingRelation (ℙ : Type u_1) (F : outParam (Type u_2)) : Type (max u_1 u_2)

• WeaklyForces : ℙ → F → Prop

def LO.«term_⊩ᶜ_» : Lean.TrailingParserDescr

Equations

• LO.«term_⊩ᶜ_» = Lean.ParserDescr.trailingNode `LO.«term_⊩ᶜ_» 45 46 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊩ᶜ ") (Lean.ParserDescr.cat `term 46))

@[reducible, inline]

abbrev LO.WeakForcingRelation.NotForces {ℙ : Type u_1} {F : Type u_2} [WeakForcingRelation ℙ F] (p : ℙ) (φ : F) : Prop

Equations

• (p ⊮ᶜ φ) = ¬p ⊩ᶜ φ

def LO.WeakForcingRelation.«term_⊮ᶜ_» : Lean.TrailingParserDescr

Equations

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

class LO.WeakForcingRelation.BasicSemantics (ℙ : Type u_1) {F : Type u_2} [WeakForcingRelation ℙ F] [LogicalConnective F] : Prop

• verum (p : ℙ) : p ⊩ᶜ ⊤
• falsum (p : ℙ) : ¬p ⊩ᶜ ⊥
• and {φ ψ : F} (p : ℙ) : p ⊩ᶜ φ ⋏ ψ ↔ p ⊩ᶜ φ ∧ p ⊩ᶜ ψ

class LO.WeakForcingRelation.ClassicalKripke (ℙ : Type u_1) {F : Type u_2} [WeakForcingRelation ℙ F] [LogicalConnective F] (R : outParam (ℙ → ℙ → Prop)) extends LO.WeakForcingRelation.BasicSemantics ℙ : Prop

• verum (p : ℙ) : p ⊩ᶜ ⊤
• falsum (p : ℙ) : ¬p ⊩ᶜ ⊥
• and {φ ψ : F} (p : ℙ) : p ⊩ᶜ φ ⋏ ψ ↔ p ⊩ᶜ φ ∧ p ⊩ᶜ ψ
• or {φ ψ : F} (p : ℙ) : p ⊩ᶜ φ ⋎ ψ ↔ ∀ (q : ℙ), R p q → ∃ (x : ℙ), R q x ∧ (x ⊩ᶜ φ ∨ x ⊩ᶜ ψ)
• not {φ : F} (p : ℙ) : p ⊩ᶜ ∼φ ↔ ∀ (q : ℙ), R p q → ¬q ⊩ᶜ φ
• imply {φ ψ : F} (p : ℙ) : p ⊩ᶜ φ 🡒 ψ ↔ ∀ (q : ℙ), R p q → q ⊩ᶜ φ → q ⊩ᶜ ψ
• monotone {φ : F} {p : ℙ} : p ⊩ᶜ φ → ∀ (q : ℙ), R p q → q ⊩ᶜ φ
• generic {φ : F} {p : ℙ} : (∀ (q : ℙ), R p q → ∃ (r : ℙ), R q r ∧ r ⊩ᶜ φ) → p ⊩ᶜ φ

@[reducible, inline]

abbrev LO.WeakForcingRelation.AllForces (ℙ : Type u_1) {F : Type u_2} [WeakForcingRelation ℙ F] (φ : F) : Prop

Equations

• (ℙ ∀⊩ᶜ φ) = ∀ (p : ℙ), p ⊩ᶜ φ

def LO.WeakForcingRelation.«term_∀⊩ᶜ_» : Lean.TrailingParserDescr

Equations

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

@[reducible, inline]

abbrev LO.WeakForcingRelation.AllForcesSet (ℙ : Type u_1) {F : Type u_2} [WeakForcingRelation ℙ F] {S : Type u_3} (s : S) [AdjunctiveSet F S] : Prop

Equations

• (ℙ ∀⊩ᶜ* s) = ∀ φ ∈ s, ℙ ∀⊩ᶜ φ

def LO.WeakForcingRelation.«term_∀⊩ᶜ*_» : Lean.TrailingParserDescr

Equations

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

@[simp]

theorem LO.WeakForcingRelation.AllForces.verum {ℙ : Type u_1} {F : Type u_2} [WeakForcingRelation ℙ F] [LogicalConnective F] [BasicSemantics ℙ] : ℙ ∀⊩ᶜ ⊤

@[simp]

theorem LO.WeakForcingRelation.AllForces.falsum {ℙ : Type u_1} {F : Type u_2} [WeakForcingRelation ℙ F] [LogicalConnective F] [BasicSemantics ℙ] [Nonempty ℙ] : ¬ℙ ∀⊩ᶜ ⊥

@[simp]

theorem LO.WeakForcingRelation.AllForces.and {ℙ : Type u_1} {F : Type u_2} [WeakForcingRelation ℙ F] [LogicalConnective F] {φ ψ : F} [BasicSemantics ℙ] : ℙ ∀⊩ᶜ φ ⋏ ψ ↔ ℙ ∀⊩ᶜ φ ∧ ℙ ∀⊩ᶜ ψ