Supporting results for pointwise provable equality.

Forcing relation

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

Data and laws for Forcing Relation in FFL.

• Forces : W → F → Prop

  The Forces construction in FFL.ForcingRelation.

def PointwiseComposition.FFL.«term_⊩_» : Lean.TrailingParserDescr

The «term ⊩ » construction in FFL.

Equations

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

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

Data and laws for Forcing Exists in FFL.

• Forces : W → α → Prop

  The Forces construction in FFL.ForcingExists.

def PointwiseComposition.FFL.«term_⊩↓_» : Lean.TrailingParserDescr

The «term ⊩↓ » construction in FFL.

Equations

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

@[reducible, inline]

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

The Not Forces construction in FFL.ForcingRelation.

Equations

• (w ⊮ φ) = ¬w ⊩ φ

def PointwiseComposition.FFL.ForcingRelation.«term_⊮_» : Lean.TrailingParserDescr

The «term ⊮ » construction in FFL.ForcingRelation.

Equations

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

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

Data and laws for Basic Semantics in FFL.ForcingRelation.

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

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

Data and laws for Monotone in FFL.ForcingRelation.

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

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

Data and laws for Int Kripke in FFL.ForcingRelation.

• 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 PointwiseComposition.FFL.ForcingRelation.iff {W : Type u_1} {F : Type u_2} [ForcingRelation W F] [LogicalConnective F] [LogicalNeutral F] {w : W} {φ ψ : F} (R : W → W → Prop) [IntKripke W R] : w ⊩ φ ⇔ₗ ψ ↔ ∀ (v : W), R w v → (v ⊩ φ ↔ v ⊩ ψ)

@[reducible, inline]

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

The All Forces construction in FFL.ForcingRelation.

Equations

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

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

The «term ∀⊩ » construction in FFL.ForcingRelation.

Equations

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

@[reducible, inline]

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

The All Forces Set construction in FFL.ForcingRelation.

Equations

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

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

The «term ∀⊩* » construction in FFL.ForcingRelation.

Equations

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

@[simp]

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

@[simp]

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

Forcing relation for classical logic

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

Data and laws for Weak Forcing Relation in FFL.

• WeaklyForces : ℙ → F → Prop

  The Weakly Forces construction in FFL.WeakForcingRelation.

def PointwiseComposition.FFL.«term_⊩ᶜ_» : Lean.TrailingParserDescr

The «term ⊩ᶜ » construction in FFL.

Equations

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

@[reducible, inline]

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

The Not Forces construction in FFL.WeakForcingRelation.

Equations

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

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

The «term ⊮ᶜ » construction in FFL.WeakForcingRelation.

Equations

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

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

Data and laws for Basic Semantics in FFL.WeakForcingRelation.

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

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

Data and laws for Classical Kripke in FFL.WeakForcingRelation.

• 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 PointwiseComposition.FFL.WeakForcingRelation.AllForces (ℙ : Type u_1) {F : Type u_2} [WeakForcingRelation ℙ F] (φ : F) : Prop

The All Forces construction in FFL.WeakForcingRelation.

Equations

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

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

The «term ∀⊩ᶜ » construction in FFL.WeakForcingRelation.

Equations

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

@[reducible, inline]

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

The All Forces Set construction in FFL.WeakForcingRelation.

Equations

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

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

The «term ∀⊩ᶜ* » construction in FFL.WeakForcingRelation.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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