@[reducible, inline]

abbrev LO.Modal.Axiom (α : Type u_1) : Type u_1

Equations

• LO.Modal.Axiom α = Set (LO.Modal.Formula α)

@[reducible, inline]

abbrev LO.Modal.Axiom.instances {α : Type u_1} (Ax : Axiom α) : FormulaSet α

Equations

• Ax.instances = {φ : LO.Modal.Formula α | ∃ ψ ∈ Ax, ∃ (s : LO.Modal.Substitution α), φ = ψ⟦s⟧}

theorem LO.Modal.Axiom.of_mem {α : Type u_1} {s : Substitution α} {Ax : Axiom α} {φ : Formula α} (hφ : φ ∈ Ax) : φ⟦s⟧ ∈ Ax.instances

class LO.Modal.Axiom.HasM {α : Type u_1} (Ax : Axiom α) : Type u_1

• p : α
• q : α
• ne_pq : p Ax ≠ q Ax
• mem_m : Axioms.M (Formula.atom (p Ax)) (Formula.atom (q Ax)) ∈ Ax

class LO.Modal.Axiom.HasC {α : Type u_1} (Ax : Axiom α) : Type u_1

• p : α
• q : α
• ne_pq : p Ax ≠ q Ax
• mem_c : Axioms.C (Formula.atom (p Ax)) (Formula.atom (q Ax)) ∈ Ax

class LO.Modal.Axiom.HasN {α : Type u_1} (Ax : Axiom α) : Prop

• mem_n : Axioms.N ∈ Ax

class LO.Modal.Axiom.HasK {α : Type u_1} (Ax : Axiom α) : Type u_1

• p : α
• q : α
• ne_pq : p Ax ≠ q Ax
• mem_K : Axioms.K (Formula.atom (p Ax)) (Formula.atom (q Ax)) ∈ Ax

class LO.Modal.Axiom.HasT {α : Type u_1} (Ax : Axiom α) : Type u_1

• p : α
• mem_T : Axioms.T (Formula.atom (p Ax)) ∈ Ax

class LO.Modal.Axiom.HasD {α : Type u_1} (Ax : Axiom α) : Type u_1

• p : α
• mem_D : Axioms.D (Formula.atom (p Ax)) ∈ Ax

class LO.Modal.Axiom.HasP {α : Type u_1} (Ax : Axiom α) : Prop

• mem_P : Axioms.P ∈ Ax

class LO.Modal.Axiom.HasB {α : Type u_1} (Ax : Axiom α) : Type u_1

• p : α
• mem_B : Axioms.B (Formula.atom (p Ax)) ∈ Ax

class LO.Modal.Axiom.HasFour {α : Type u_1} (Ax : Axiom α) : Type u_1

• p : α
• mem_Four : Axioms.Four (Formula.atom (p Ax)) ∈ Ax

class LO.Modal.Axiom.HasFourN {α : Type u_1} (n : ℕ) (Ax : Axiom α) : Type u_1

• p : α
• mem_FourN : Axioms.FourN n (Formula.atom (p n Ax)) ∈ Ax

class LO.Modal.Axiom.HasFive {α : Type u_1} (Ax : Axiom α) : Type u_1

• p : α
• mem_Five : Axioms.Five (Formula.atom (p Ax)) ∈ Ax

class LO.Modal.Axiom.HasPoint2 {α : Type u_1} (Ax : Axiom α) : Type u_1

• p : α
• mem_Point2 : Axioms.Point2 (Formula.atom (p Ax)) ∈ Ax

class LO.Modal.Axiom.HasWeakPoint2 {α : Type u_1} (Ax : Axiom α) : Type u_1

• p : α
• q : α
• ne_pq : p Ax ≠ q Ax
• mem_WeakPoint2 : Axioms.WeakPoint2 (Formula.atom (p Ax)) (Formula.atom (q Ax)) ∈ Ax

class LO.Modal.Axiom.HasPoint3 {α : Type u_1} (Ax : Axiom α) : Type u_1

• p : α
• q : α
• ne_pq : p Ax ≠ q Ax
• mem_Point3 : Axioms.Point3 (Formula.atom (p Ax)) (Formula.atom (q Ax)) ∈ Ax

class LO.Modal.Axiom.HasWeakPoint3 {α : Type u_1} (Ax : Axiom α) : Type u_1

• p : α
• q : α
• ne_pq : p Ax ≠ q Ax
• mem_WeakPoint3 : Axioms.WeakPoint3 (Formula.atom (p Ax)) (Formula.atom (q Ax)) ∈ Ax

class LO.Modal.Axiom.HasPoint4 {α : Type u_1} (Ax : Axiom α) : Type u_1

• p : α
• mem_Point4 : Axioms.Point4 (Formula.atom (p Ax)) ∈ Ax

class LO.Modal.Axiom.HasL {α : Type u_1} (Ax : Axiom α) : Type u_1

• p : α
• mem_L : Axioms.L (Formula.atom (p Ax)) ∈ Ax

class LO.Modal.Axiom.HasZ {α : Type u_1} (Ax : Axiom α) : Type u_1

• p : α
• mem_Z : Axioms.Z (Formula.atom (p Ax)) ∈ Ax

class LO.Modal.Axiom.HasGrz {α : Type u_1} (Ax : Axiom α) : Type u_1

• p : α
• mem_Grz : Axioms.Grz (Formula.atom (p Ax)) ∈ Ax

class LO.Modal.Axiom.HasDum {α : Type u_1} (Ax : Axiom α) : Type u_1

• p : α
• mem_Dum : Axioms.Dum (Formula.atom (p Ax)) ∈ Ax

class LO.Modal.Axiom.HasTc {α : Type u_1} (Ax : Axiom α) : Type u_1

• p : α
• mem_Tc : Axioms.Tc (Formula.atom (p Ax)) ∈ Ax

class LO.Modal.Axiom.HasVer {α : Type u_1} (Ax : Axiom α) : Type u_1

• p : α
• mem_Ver : Axioms.Ver (Formula.atom (p Ax)) ∈ Ax

class LO.Modal.Axiom.HasHen {α : Type u_1} (Ax : Axiom α) : Type u_1

• p : α
• mem_Hen : Axioms.Hen (Formula.atom (p Ax)) ∈ Ax

class LO.Modal.Axiom.HasMcK {α : Type u_1} (Ax : Axiom α) : Type u_1

• p : α
• mem_McK : Axioms.McK (Formula.atom (p Ax)) ∈ Ax

class LO.Modal.Axiom.HasMk {α : Type u_1} (Ax : Axiom α) : Type u_1

• p : α
• q : α
• ne_pq : p Ax ≠ q Ax
• mem_Mk : Axioms.Mk (Formula.atom (p Ax)) (Formula.atom (q Ax)) ∈ Ax

class LO.Modal.Axiom.HasH1 {α : Type u_1} (Ax : Axiom α) : Type u_1

• p : α
• mem_H1 : Axioms.H (Formula.atom (p Ax)) ∈ Ax

class LO.Modal.Axiom.HasGeach {α : Type u_1} (g : Axioms.Geach.Taple) (Ax : Axiom α) : Type u_1

• p : α
• mem_Geach : Axioms.Geach g (Formula.atom (p g Ax)) ∈ Ax