Logic Symbols

This file defines structure that has logical connectives $\top, \bot, \land, \lor, \to, \lnot$ and their homomorphisms.

Main Definitions

• LO.LogicalConnective is defined so that LO.LogicalConnective F is a type that has logical connectives $\top, \bot, \land, \lor, \to, \lnot$.
• LO.LogicalConnective.Hom is defined so that f : F →ˡᶜ G is a homomorphism from F to G, i.e., a function that preserves logical connectives.

class LO.Tilde (α : Type u_1) : Type u_1

• tilde : α → α

class LO.Arrow (α : Type u_1) : Type u_1

• arrow : α → α → α

class LO.Wedge (α : Type u_1) : Type u_1

• wedge : α → α → α

class LO.Vee (α : Type u_1) : Type u_1

• vee : α → α → α

class LO.LogicalConnective (α : Type u_1) extends Top α, Bot α, LO.Tilde α, LO.Arrow α, LO.Wedge α, LO.Vee α : Type u_1

• top : α
• bot : α
• tilde : α → α
• arrow : α → α → α
• wedge : α → α → α
• vee : α → α → α

def LO.«term∼_» : Lean.ParserDescr

Equations

• LO.«term∼_» = Lean.ParserDescr.node `LO.«term∼_» 75 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∼") (Lean.ParserDescr.cat `term 75))

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

Equations

• LO.«term_➝_» = Lean.ParserDescr.trailingNode `LO.«term_➝_» 60 61 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ➝ ") (Lean.ParserDescr.cat `term 60))

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

Equations

• LO.«term_⋏_» = Lean.ParserDescr.trailingNode `LO.«term_⋏_» 69 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⋏ ") (Lean.ParserDescr.cat `term 69))

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

Equations

• LO.«term_⋎_» = Lean.ParserDescr.trailingNode `LO.«term_⋎_» 68 69 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⋎ ") (Lean.ParserDescr.cat `term 68))

class LO.DeMorgan (F : Type u_1) [LogicalConnective F] : Prop

• verum : ∼⊤ = ⊥
• falsum : ∼⊥ = ⊤
• imply (φ ψ : F) : φ ➝ ψ = ∼φ ⋎ ψ
• and (φ ψ : F) : ∼(φ ⋏ ψ) = ∼φ ⋎ ∼ψ
• or (φ ψ : F) : ∼(φ ⋎ ψ) = ∼φ ⋏ ∼ψ
• neg (φ : F) : ∼∼φ = φ

class LO.NegAbbrev (F : Type u_1) [Tilde F] [Arrow F] [Bot F] : Prop

Introducing ∼φ as an abbreviation of φ ➝ ⊥.

• neg {φ : F} : ∼φ = φ ➝ ⊥

@[match_pattern]

def LO.LogicalConnective.iff {α : Type u_1} [LogicalConnective α] (a b : α) : α

Equations

• a ⭤ b = (a ➝ b) ⋏ (b ➝ a)

def LO.LogicalConnective.«term_⭤_» : Lean.TrailingParserDescr

Equations

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

@[reducible]

instance LO.LogicalConnective.PropLogicSymbols : LogicalConnective Prop

Equations

• LO.LogicalConnective.PropLogicSymbols = LO.LogicalConnective.mk

@[simp]

theorem LO.LogicalConnective.Prop.top_eq : ⊤ = True

@[simp]

theorem LO.LogicalConnective.Prop.bot_eq : ⊥ = False

@[simp]

theorem LO.LogicalConnective.Prop.neg_eq (φ : Prop) : ∼φ = ¬φ

@[simp]

theorem LO.LogicalConnective.Prop.arrow_eq (φ ψ : Prop) : φ ➝ ψ = (φ → ψ)

@[simp]

theorem LO.LogicalConnective.Prop.and_eq (φ ψ : Prop) : φ ⋏ ψ = (φ ∧ ψ)

@[simp]

theorem LO.LogicalConnective.Prop.or_eq (φ ψ : Prop) : φ ⋎ ψ = (φ ∨ ψ)

@[simp]

theorem LO.LogicalConnective.Prop.iff_eq (φ ψ : Prop) : φ ⭤ ψ = (φ ↔ ψ)

instance LO.LogicalConnective.instDeMorganProp : DeMorgan Prop

class LO.LogicalConnective.HomClass (F : Type u_1) (α : outParam (Type u_2)) (β : outParam (Type u_3)) [LogicalConnective α] [LogicalConnective β] [FunLike F α β] : Prop

• map_top (f : F) : f ⊤ = ⊤
• map_bot (f : F) : f ⊥ = ⊥
• map_neg (f : F) (φ : α) : f (∼φ) = ∼f φ
• map_imply (f : F) (φ ψ : α) : f (φ ➝ ψ) = f φ ➝ f ψ
• map_and (f : F) (φ ψ : α) : f (φ ⋏ ψ) = f φ ⋏ f ψ
• map_or (f : F) (φ ψ : α) : f (φ ⋎ ψ) = f φ ⋎ f ψ

instance LO.LogicalConnective.HomClass.instCoeFunForall (F : Type u_1) (α : outParam (Type u_2)) (β : outParam (Type u_3)) [FunLike F α β] : CoeFun F fun (x : F) => α → β

Equations

• LO.LogicalConnective.HomClass.instCoeFunForall F α β = { coe := DFunLike.coe }

@[simp]

theorem LO.LogicalConnective.HomClass.map_iff (F : Type u_1) (α : outParam (Type u_2)) (β : outParam (Type u_3)) [LogicalConnective α] [LogicalConnective β] [FunLike F α β] [HomClass F α β] (f : F) (a b : α) : f (a ⭤ b) = f a ⭤ f b

structure LO.LogicalConnective.Hom (α : Type u_1) (β : Type u_2) [LogicalConnective α] [LogicalConnective β] : Type (max u_1 u_2)

• toTr : α → β
• map_top' : self.toTr ⊤ = ⊤
• map_bot' : self.toTr ⊥ = ⊥
• map_neg' (φ : α) : self.toTr (∼φ) = ∼self.toTr φ
• map_imply' (φ ψ : α) : self.toTr (φ ➝ ψ) = self.toTr φ ➝ self.toTr ψ
• map_and' (φ ψ : α) : self.toTr (φ ⋏ ψ) = self.toTr φ ⋏ self.toTr ψ
• map_or' (φ ψ : α) : self.toTr (φ ⋎ ψ) = self.toTr φ ⋎ self.toTr ψ

def LO.LogicalConnective.«term_→ˡᶜ_» : Lean.TrailingParserDescr

Equations

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

instance LO.LogicalConnective.Hom.instFunLike {α : Type u_1} {β : Type u_2} [LogicalConnective α] [LogicalConnective β] : FunLike (α →ˡᶜ β) α β

Equations

• LO.LogicalConnective.Hom.instFunLike = { coe := LO.LogicalConnective.Hom.toTr, coe_injective' := ⋯ }

instance LO.LogicalConnective.Hom.instCoeFunForall {α : Type u_1} {β : Type u_2} [LogicalConnective α] [LogicalConnective β] : CoeFun (α →ˡᶜ β) fun (x : α →ˡᶜ β) => α → β

Equations

• LO.LogicalConnective.Hom.instCoeFunForall = DFunLike.hasCoeToFun

theorem LO.LogicalConnective.Hom.ext {α : Type u_1} {β : Type u_2} [LogicalConnective α] [LogicalConnective β] (f g : α →ˡᶜ β) (h : ∀ (x : α), f x = g x) : f = g

instance LO.LogicalConnective.Hom.instHomClass {α : Type u_1} {β : Type u_2} [LogicalConnective α] [LogicalConnective β] : HomClass (α →ˡᶜ β) α β

def LO.LogicalConnective.Hom.id {α : Type u_1} [LogicalConnective α] : α →ˡᶜ α

Equations

• LO.LogicalConnective.Hom.id = { toTr := id, map_top' := ⋯, map_bot' := ⋯, map_neg' := ⋯, map_imply' := ⋯, map_and' := ⋯, map_or' := ⋯ }

@[simp]

theorem LO.LogicalConnective.Hom.app_id {α : Type u_1} [LogicalConnective α] (a : α) : Hom.id a = a

def LO.LogicalConnective.Hom.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LogicalConnective α] [LogicalConnective β] [LogicalConnective γ] (g : β →ˡᶜ γ) (f : α →ˡᶜ β) : α →ˡᶜ γ

Equations

• g.comp f = { toTr := ⇑g ∘ ⇑f, map_top' := ⋯, map_bot' := ⋯, map_neg' := ⋯, map_imply' := ⋯, map_and' := ⋯, map_or' := ⋯ }

@[simp]

theorem LO.LogicalConnective.Hom.app_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LogicalConnective α] [LogicalConnective β] [LogicalConnective γ] (g : β →ˡᶜ γ) (f : α →ˡᶜ β) (a : α) : (g.comp f) a = g (f a)

class LO.LogicalConnective.AndOrClosed {F : Type u_4} [LogicalConnective F] (C : F → Prop) : Prop

• verum : C ⊤
• falsum : C ⊥
• and {f g : F} : C f → C g → C (f ⋏ g)
• or {f g : F} : C f → C g → C (f ⋎ g)

class LO.LogicalConnective.Closed {F : Type u_4} [LogicalConnective F] (C : F → Prop) extends LO.LogicalConnective.AndOrClosed C : Prop

• verum : C ⊤
• falsum : C ⊥
• and {f g : F} : C f → C g → C (f ⋏ g)
• or {f g : F} : C f → C g → C (f ⋎ g)
• not {f : F} : C f → C (∼f)
• imply {f g : F} : C f → C g → C (f ➝ g)

class LO.Tilde.Subclosed {F : Type u_1} [Tilde F] (C : F → Prop) : Prop

• tilde_closed {φ : F} : C (∼φ) → C φ

class LO.Arrow.Subclosed {F : Type u_1} [Arrow F] (C : F → Prop) : Prop

• arrow_closed {φ ψ : F} : C (φ ➝ ψ) → C φ ∧ C ψ

class LO.Wedge.Subclosed {F : Type u_1} [Wedge F] (C : F → Prop) : Prop

• wedge_closed {φ ψ : F} : C (φ ⋏ ψ) → C φ ∧ C ψ

class LO.Vee.Subclosed {F : Type u_1} [Vee F] (C : F → Prop) : Prop

• vee_closed {φ ψ : F} : C (φ ⋎ ψ) → C φ ∧ C ψ

class LO.LogicalConnective.Subclosed {F : Type u_1} [LogicalConnective F] (C : F → Prop) extends LO.Tilde.Subclosed C, LO.Arrow.Subclosed C, LO.Wedge.Subclosed C, LO.Vee.Subclosed C : Prop

• tilde_closed {φ : F} : C (∼φ) → C φ
• arrow_closed {φ ψ : F} : C (φ ➝ ψ) → C φ ∧ C ψ
• wedge_closed {φ ψ : F} : C (φ ⋏ ψ) → C φ ∧ C ψ
• vee_closed {φ ψ : F} : C (φ ⋎ ψ) → C φ ∧ C ψ

def LO.conjLt {α : Type u_1} [LogicalConnective α] (φ : ℕ → α) : ℕ → α

Equations

• LO.conjLt φ 0 = ⊤
• LO.conjLt φ k.succ = φ k ⋏ LO.conjLt φ k

@[simp]

theorem LO.conjLt_zero {α : Type u_1} [LogicalConnective α] (φ : ℕ → α) : conjLt φ 0 = ⊤

@[simp]

theorem LO.conjLt_succ {α : Type u_1} [LogicalConnective α] (φ : ℕ → α) (k : ℕ) : conjLt φ (k + 1) = φ k ⋏ conjLt φ k

@[simp]

theorem LO.hom_conj_prop {α : Type u_1} [LogicalConnective α] {F : Type u_3} {k : ℕ} [FunLike F α Prop] [LogicalConnective.HomClass F α Prop] (f : F) (φ : ℕ → α) : f (conjLt φ k) ↔ ∀ i < k, f (φ i)

def LO.disjLt {α : Type u_1} [LogicalConnective α] (φ : ℕ → α) : ℕ → α

Equations

• LO.disjLt φ 0 = ⊥
• LO.disjLt φ k.succ = φ k ⋎ LO.disjLt φ k

@[simp]

theorem LO.disjLt_zero {α : Type u_1} [LogicalConnective α] (φ : ℕ → α) : disjLt φ 0 = ⊥

@[simp]

theorem LO.disjLt_succ {α : Type u_1} [LogicalConnective α] (φ : ℕ → α) (k : ℕ) : disjLt φ (k + 1) = φ k ⋎ disjLt φ k

@[simp]

theorem LO.hom_disj_prop {α : Type u_1} [LogicalConnective α] {F : Type u_3} {k : ℕ} [FunLike F α Prop] [LogicalConnective.HomClass F α Prop] (f : F) (φ : ℕ → α) : f (disjLt φ k) ↔ ∃ i < k, f (φ i)

def Matrix.conj {α : Type u_1} [LO.LogicalConnective α] {n : ℕ} : (Fin n → α) → α

Equations

• Matrix.conj x_2 = ⊤
• Matrix.conj v = v 0 ⋏ Matrix.conj (Matrix.vecTail v)

@[simp]

theorem Matrix.conj_nil {α : Type u_1} [LO.LogicalConnective α] (v : Fin 0 → α) : conj v = ⊤

@[simp]

theorem Matrix.conj_cons {α : Type u_1} [LO.LogicalConnective α] {n : ℕ} {a : α} {v : Fin n → α} : conj (a :> v) = a ⋏ conj v

@[simp]

theorem Matrix.conj_hom_prop {α : Type u_1} [LO.LogicalConnective α] {F : Type u_2} {n : ℕ} [FunLike F α Prop] [LO.LogicalConnective.HomClass F α Prop] (f : F) (v : Fin n → α) : f (conj v) = ∀ (i : Fin n), f (v i)

theorem Matrix.hom_conj {β : Type u_3} {α : Type u_1} [LO.LogicalConnective α] [LO.LogicalConnective β] {F : Type u_2} {n : ℕ} [FunLike F α β] [LO.LogicalConnective.HomClass F α β] (f : F) (v : Fin n → α) : f (conj v) = conj (⇑f ∘ v)

theorem Matrix.hom_conj₂ {β : Type u_3} {α : Type u_1} [LO.LogicalConnective α] [LO.LogicalConnective β] {F : Type u_2} {n : ℕ} [FunLike F α β] [LO.LogicalConnective.HomClass F α β] (f : F) (v : Fin n → α) : f (conj v) = conj fun (i : Fin n) => f (v i)

def Matrix.disj {α : Type u_1} [LO.LogicalConnective α] {n : ℕ} : (Fin n → α) → α

Equations

• Matrix.disj x_2 = ⊥
• Matrix.disj v = v 0 ⋎ Matrix.disj (Matrix.vecTail v)

@[simp]

theorem Matrix.disj_nil {α : Type u_1} [LO.LogicalConnective α] (v : Fin 0 → α) : disj v = ⊥

@[simp]

theorem Matrix.disj_cons {α : Type u_1} [LO.LogicalConnective α] {n : ℕ} {a : α} {v : Fin n → α} : disj (a :> v) = a ⋎ disj v

@[simp]

theorem Matrix.disj_hom_prop {α : Type u_1} [LO.LogicalConnective α] {F : Type u_2} {n : ℕ} [FunLike F α Prop] [LO.LogicalConnective.HomClass F α Prop] (f : F) (v : Fin n → α) : f (disj v) = ∃ (i : Fin n), f (v i)

theorem Matrix.hom_disj {β : Type u_3} {α : Type u_1} [LO.LogicalConnective α] [LO.LogicalConnective β] {F : Type u_2} {n : ℕ} [FunLike F α β] [LO.LogicalConnective.HomClass F α β] (f : F) (v : Fin n → α) : f (disj v) = disj (⇑f ∘ v)

theorem Matrix.hom_disj' {β : Type u_3} {α : Type u_1} [LO.LogicalConnective α] [LO.LogicalConnective β] {F : Type u_2} {n : ℕ} [FunLike F α β] [LO.LogicalConnective.HomClass F α β] (f : F) (v : Fin n → α) : f (disj v) = disj fun (i : Fin n) => f (v i)

def List.conj {α : Type u_1} [LO.LogicalConnective α] : List α → α

Equations

• [].conj = ⊤
• (a :: as).conj = a ⋏ as.conj

@[simp]

theorem List.conj_nil {α : Type u_1} [LO.LogicalConnective α] : [].conj = ⊤

@[simp]

theorem List.conj_cons {α : Type u_1} [LO.LogicalConnective α] {a : α} {as : List α} : (a :: as).conj = a ⋏ as.conj

theorem List.map_conj {α : Type u_1} [LO.LogicalConnective α] {F : Type u_2} [FunLike F α Prop] [LO.LogicalConnective.HomClass F α Prop] (f : F) (l : List α) : f l.conj ↔ ∀ a ∈ l, f a

theorem List.map_conj_append {α : Type u_1} [LO.LogicalConnective α] {F : Type u_2} [FunLike F α Prop] [LO.LogicalConnective.HomClass F α Prop] (f : F) (l₁ l₂ : List α) : f (l₁ ++ l₂).conj ↔ f (l₁.conj ⋏ l₂.conj)

def List.disj {α : Type u_1} [LO.LogicalConnective α] : List α → α

Equations

• [].disj = ⊥
• (a :: as).disj = a ⋎ as.disj

@[simp]

theorem List.disj_nil {α : Type u_1} [LO.LogicalConnective α] : [].disj = ⊥

@[simp]

theorem List.disj_cons {α : Type u_1} [LO.LogicalConnective α] {a : α} {as : List α} : (a :: as).disj = a ⋎ as.disj

theorem List.map_disj {α : Type u_1} [LO.LogicalConnective α] {F : Type u_2} [FunLike F α Prop] [LO.LogicalConnective.HomClass F α Prop] (f : F) (l : List α) : f l.disj ↔ ∃ a ∈ l, f a

theorem List.map_disj_append {α : Type u_1} [LO.LogicalConnective α] {F : Type u_2} [FunLike F α Prop] [LO.LogicalConnective.HomClass F α Prop] (f : F) (l₁ l₂ : List α) : f (l₁ ++ l₂).disj ↔ f (l₁.disj ⋎ l₂.disj)

def List.conj₂ {F : Type u} [LO.LogicalConnective F] : List F → F

Remark: [φ].conj₂ = φ ≠ φ ⋏ ⊤ = [φ].conj

Equations

• ⋀[] = ⊤
• ⋀[φ] = φ
• ⋀(φ :: ψ :: rs) = φ ⋏ ⋀(ψ :: rs)

def List.«term⋀_» : Lean.ParserDescr

Equations

• List.«term⋀_» = Lean.ParserDescr.node `List.«term⋀_» 80 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⋀") (Lean.ParserDescr.cat `term 80))

@[simp]

theorem List.conj₂_nil {F : Type u} [LO.LogicalConnective F] : ⋀[] = ⊤

@[simp]

theorem List.conj₂_singleton {F : Type u} [LO.LogicalConnective F] {φ : F} : ⋀[φ] = φ

@[simp]

theorem List.conj₂_doubleton {F : Type u} [LO.LogicalConnective F] {φ ψ : F} : ⋀[φ, ψ] = φ ⋏ ψ

@[simp]

theorem List.conj₂_cons_nonempty {F : Type u} [LO.LogicalConnective F] {a : F} {as : List F} (h : as ≠ [] := by assumption) : ⋀(a :: as) = a ⋏ ⋀as

def List.disj₂ {F : Type u} [LO.LogicalConnective F] : List F → F

Remark: [φ].disj = φ ≠ φ ⋎ ⊥ = [φ].disj

Equations

• ⋁[] = ⊥
• ⋁[φ] = φ
• ⋁(φ :: ψ :: rs) = φ ⋎ ⋁(ψ :: rs)

def List.«term⋁_» : Lean.ParserDescr

Equations

• List.«term⋁_» = Lean.ParserDescr.node `List.«term⋁_» 80 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⋁") (Lean.ParserDescr.cat `term 80))

@[simp]

theorem List.disj₂_nil {F : Type u} [LO.LogicalConnective F] : ⋁[] = ⊥

@[simp]

theorem List.disj₂_singleton {F : Type u} [LO.LogicalConnective F] {φ : F} : ⋁[φ] = φ

@[simp]

theorem List.disj₂_doubleton {F : Type u} [LO.LogicalConnective F] {φ ψ : F} : ⋁[φ, ψ] = φ ⋎ ψ

@[simp]

theorem List.disj₂_cons_nonempty {F : Type u} [LO.LogicalConnective F] {a : F} {as : List F} (h : as ≠ [] := by assumption) : ⋁(a :: as) = a ⋎ ⋁as

noncomputable def Finset.conj {α : Type u_1} [LO.LogicalConnective α] (s : Finset α) : α

Equations

• s.conj = s.toList.conj

theorem Finset.map_conj {α : Type u_2} [LO.LogicalConnective α] {F : Type u_1} [FunLike F α Prop] [LO.LogicalConnective.HomClass F α Prop] (f : F) (s : Finset α) : f s.conj ↔ ∀ a ∈ s, f a

theorem Finset.map_conj_union {α : Type u_2} [LO.LogicalConnective α] {F : Type u_1} [DecidableEq α] [FunLike F α Prop] [LO.LogicalConnective.HomClass F α Prop] (f : F) (s₁ s₂ : Finset α) : f (s₁ ∪ s₂).conj ↔ f (s₁.conj ⋏ s₂.conj)

noncomputable def Finset.disj {α : Type u_1} [LO.LogicalConnective α] (s : Finset α) : α

Equations

• s.disj = s.toList.disj

theorem Finset.map_disj {α : Type u_2} [LO.LogicalConnective α] {F : Type u_1} [FunLike F α Prop] [LO.LogicalConnective.HomClass F α Prop] (f : F) (s : Finset α) : f s.disj ↔ ∃ a ∈ s, f a

theorem Finset.map_disj_union {α : Type u_2} [LO.LogicalConnective α] {F : Type u_1} [DecidableEq α] [FunLike F α Prop] [LO.LogicalConnective.HomClass F α Prop] (f : F) (s₁ s₂ : Finset α) : f (s₁ ∪ s₂).disj ↔ f (s₁.disj ⋎ s₂.disj)