inductive LO.IntProp.Formula (α : Type u) : Type u

• atom {α : Type u} : α → Formula α
• verum {α : Type u} : Formula α
• falsum {α : Type u} : Formula α
• neg {α : Type u} : Formula α → Formula α
• and {α : Type u} : Formula α → Formula α → Formula α
• or {α : Type u} : Formula α → Formula α → Formula α
• imp {α : Type u} : Formula α → Formula α → Formula α

instance LO.IntProp.instDecidableEqFormula {α✝ : Type u_1} [DecidableEq α✝] : DecidableEq (Formula α✝)

Equations

• LO.IntProp.instDecidableEqFormula = LO.IntProp.decEqFormula✝

instance LO.IntProp.Formula.instLogicalConnective {α : Type u_1} : LogicalConnective (Formula α)

Equations

• LO.IntProp.Formula.instLogicalConnective = LO.LogicalConnective.mk

def LO.IntProp.Formula.toStr {α : Type u_1} [ToString α] : Formula α → String

Equations

• LO.IntProp.Formula.verum.toStr = "\top"
• LO.IntProp.Formula.falsum.toStr = "\bot"
• (LO.IntProp.Formula.atom a).toStr = "{" ++ toString a ++ "}"
• φ.neg.toStr = "\lnot " ++ φ.toStr
• (φ.and ψ).toStr = "\left(" ++ φ.toStr ++ " \land " ++ ψ.toStr ++ "\right)"
• (φ.or ψ).toStr = "\left(" ++ φ.toStr ++ " \lor " ++ ψ.toStr ++ "\right)"
• (φ.imp ψ).toStr = "\left(" ++ φ.toStr ++ " \rightarrow " ++ ψ.toStr ++ "\right)"

instance LO.IntProp.Formula.instRepr {α : Type u_1} [ToString α] : Repr (Formula α)

Equations

• LO.IntProp.Formula.instRepr = { reprPrec := fun (t : LO.IntProp.Formula α) (x : ℕ) => Std.Format.text t.toStr }

instance LO.IntProp.Formula.instToString {α : Type u_1} [ToString α] : ToString (Formula α)

Equations

• LO.IntProp.Formula.instToString = { toString := LO.IntProp.Formula.toStr }

@[simp]

theorem LO.IntProp.Formula.and_inj {α : Type u_1} (φ₁ ψ₁ φ₂ ψ₂ : Formula α) : φ₁ ⋏ φ₂ = ψ₁ ⋏ ψ₂ ↔ φ₁ = ψ₁ ∧ φ₂ = ψ₂

@[simp]

theorem LO.IntProp.Formula.or_inj {α : Type u_1} (φ₁ ψ₁ φ₂ ψ₂ : Formula α) : φ₁ ⋎ φ₂ = ψ₁ ⋎ ψ₂ ↔ φ₁ = ψ₁ ∧ φ₂ = ψ₂

@[simp]

theorem LO.IntProp.Formula.imp_inj {α : Type u_1} (φ₁ ψ₁ φ₂ ψ₂ : Formula α) : φ₁ ➝ φ₂ = ψ₁ ➝ ψ₂ ↔ φ₁ = ψ₁ ∧ φ₂ = ψ₂

@[simp]

theorem LO.IntProp.Formula.neg_inj {α : Type u_1} (φ ψ : Formula α) : ∼φ = ∼ψ ↔ φ = ψ

theorem LO.IntProp.Formula.iff_def {α : Type u_1} (φ ψ : Formula α) : φ ⭤ ψ = (φ ➝ ψ) ⋏ (ψ ➝ φ)

def LO.IntProp.Formula.complexity {α : Type u_1} : Formula α → ℕ

Equations

• (LO.IntProp.Formula.atom a).complexity = 0
• LO.IntProp.Formula.verum.complexity = 0
• LO.IntProp.Formula.falsum.complexity = 0
• φ.neg.complexity = φ.complexity + 1
• (φ.imp ψ).complexity = φ.complexity ⊔ ψ.complexity + 1
• (φ.and ψ).complexity = φ.complexity ⊔ ψ.complexity + 1
• (φ.or ψ).complexity = φ.complexity ⊔ ψ.complexity + 1

@[simp]

theorem LO.IntProp.Formula.complexity_bot {α : Type u_1} : ⊥.complexity = 0

@[simp]

theorem LO.IntProp.Formula.complexity_top {α : Type u_1} : ⊤.complexity = 0

@[simp]

theorem LO.IntProp.Formula.complexity_atom {α : Type u_1} (a : α) : (atom a).complexity = 0

@[simp]

theorem LO.IntProp.Formula.complexity_imp {α : Type u_1} (φ ψ : Formula α) : (φ ➝ ψ).complexity = φ.complexity ⊔ ψ.complexity + 1

@[simp]

theorem LO.IntProp.Formula.complexity_imp' {α : Type u_1} (φ ψ : Formula α) : (φ.imp ψ).complexity = φ.complexity ⊔ ψ.complexity + 1

@[simp]

theorem LO.IntProp.Formula.complexity_and {α : Type u_1} (φ ψ : Formula α) : (φ ⋏ ψ).complexity = φ.complexity ⊔ ψ.complexity + 1

@[simp]

theorem LO.IntProp.Formula.complexity_and' {α : Type u_1} (φ ψ : Formula α) : (φ.and ψ).complexity = φ.complexity ⊔ ψ.complexity + 1

@[simp]

theorem LO.IntProp.Formula.complexity_or {α : Type u_1} (φ ψ : Formula α) : (φ ⋎ ψ).complexity = φ.complexity ⊔ ψ.complexity + 1

@[simp]

theorem LO.IntProp.Formula.complexity_or' {α : Type u_1} (φ ψ : Formula α) : (φ.or ψ).complexity = φ.complexity ⊔ ψ.complexity + 1

def LO.IntProp.Formula.cases' {α : Type u_1} {C : Formula α → Sort w} (hfalsum : C ⊥) (hverum : C ⊤) (hatom : (a : α) → C (atom a)) (hneg : (φ : Formula α) → C (∼φ)) (himp : (φ ψ : Formula α) → C (φ ➝ ψ)) (hand : (φ ψ : Formula α) → C (φ ⋏ ψ)) (hor : (φ ψ : Formula α) → C (φ ⋎ ψ)) (φ : Formula α) : C φ

Equations

• LO.IntProp.Formula.cases' hfalsum hverum hatom hneg himp hand hor LO.IntProp.Formula.falsum = hfalsum
• LO.IntProp.Formula.cases' hfalsum hverum hatom hneg himp hand hor LO.IntProp.Formula.verum = hverum
• LO.IntProp.Formula.cases' hfalsum hverum hatom hneg himp hand hor (LO.IntProp.Formula.atom a) = hatom a
• LO.IntProp.Formula.cases' hfalsum hverum hatom hneg himp hand hor φ.neg = hneg φ
• LO.IntProp.Formula.cases' hfalsum hverum hatom hneg himp hand hor (φ.imp ψ) = himp φ ψ
• LO.IntProp.Formula.cases' hfalsum hverum hatom hneg himp hand hor (φ.and ψ) = hand φ ψ
• LO.IntProp.Formula.cases' hfalsum hverum hatom hneg himp hand hor (φ.or ψ) = hor φ ψ

def LO.IntProp.Formula.rec' {α : Type u_1} {C : Formula α → Sort w} (hfalsum : C ⊥) (hverum : C ⊤) (hatom : (a : α) → C (atom a)) (hneg : (φ : Formula α) → C φ → C (∼φ)) (himp : (φ ψ : Formula α) → C φ → C ψ → C (φ ➝ ψ)) (hand : (φ ψ : Formula α) → C φ → C ψ → C (φ ⋏ ψ)) (hor : (φ ψ : Formula α) → C φ → C ψ → C (φ ⋎ ψ)) (φ : Formula α) : C φ

Equations

• One or more equations did not get rendered due to their size.
• LO.IntProp.Formula.rec' hfalsum hverum hatom hneg himp hand hor LO.IntProp.Formula.falsum = hfalsum
• LO.IntProp.Formula.rec' hfalsum hverum hatom hneg himp hand hor LO.IntProp.Formula.verum = hverum
• LO.IntProp.Formula.rec' hfalsum hverum hatom hneg himp hand hor (LO.IntProp.Formula.atom a) = hatom a
• LO.IntProp.Formula.rec' hfalsum hverum hatom hneg himp hand hor φ.neg = hneg φ (LO.IntProp.Formula.rec' hfalsum hverum hatom hneg himp hand hor φ)

def LO.IntProp.Formula.hasDecEq {α : Type u_1} [DecidableEq α] (φ ψ : Formula α) : Decidable (φ = ψ)

Equations

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

instance LO.IntProp.Formula.instDecidableEq {α : Type u_1} [DecidableEq α] : DecidableEq (Formula α)

Equations

• LO.IntProp.Formula.instDecidableEq = LO.IntProp.Formula.hasDecEq

def LO.IntProp.Formula.toNat {α : Type u_1} [Encodable α] : Formula α → ℕ

Equations

• (LO.IntProp.Formula.atom a).toNat = Nat.pair 0 (Encodable.encode a) + 1
• LO.IntProp.Formula.verum.toNat = Nat.pair 1 0 + 1
• LO.IntProp.Formula.falsum.toNat = Nat.pair 2 0 + 1
• φ.neg.toNat = Nat.pair 3 φ.toNat + 1
• (φ.imp ψ).toNat = Nat.pair 4 (Nat.pair φ.toNat ψ.toNat) + 1
• (φ.and ψ).toNat = Nat.pair 5 (Nat.pair φ.toNat ψ.toNat) + 1
• (φ.or ψ).toNat = Nat.pair 6 (Nat.pair φ.toNat ψ.toNat) + 1

@[irreducible]

def LO.IntProp.Formula.ofNat {α : Type u_1} [Encodable α] : ℕ → Option (Formula α)

Equations

• One or more equations did not get rendered due to their size.
• LO.IntProp.Formula.ofNat 0 = none

theorem LO.IntProp.Formula.ofNat_toNat {α : Type u_1} [Encodable α] (φ : Formula α) : ofNat φ.toNat = some φ

instance LO.IntProp.Formula.instEncodable {α : Type u_1} [Encodable α] : Encodable (Formula α)

Equations

• LO.IntProp.Formula.instEncodable = { encode := LO.IntProp.Formula.toNat, decode := LO.IntProp.Formula.ofNat, encodek := ⋯ }

def LO.IntProp.Formula.subst {α : Type u_1} (s : α → Formula α) : Formula α → Formula α

Equations

• LO.IntProp.Formula.subst s (LO.IntProp.Formula.atom a) = s a
• LO.IntProp.Formula.subst s LO.IntProp.Formula.verum = ⊤
• LO.IntProp.Formula.subst s LO.IntProp.Formula.falsum = ⊥
• LO.IntProp.Formula.subst s φ.neg = ∼LO.IntProp.Formula.subst s φ
• LO.IntProp.Formula.subst s (φ.imp ψ) = LO.IntProp.Formula.subst s φ ➝ LO.IntProp.Formula.subst s ψ
• LO.IntProp.Formula.subst s (φ.and ψ) = LO.IntProp.Formula.subst s φ ⋏ LO.IntProp.Formula.subst s ψ
• LO.IntProp.Formula.subst s (φ.or ψ) = LO.IntProp.Formula.subst s φ ⋎ LO.IntProp.Formula.subst s ψ

@[simp]

theorem LO.IntProp.Formula.subst_atom {α : Type u_1} {s : α → Formula α} {a : α} : subst s (atom a) = s a

@[simp]

theorem LO.IntProp.Formula.subst_and {α : Type u_1} {s : α → Formula α} {φ ψ : Formula α} : subst s (φ ⋏ ψ) = subst s φ ⋏ subst s ψ

@[simp]

theorem LO.IntProp.Formula.subst_or {α : Type u_1} {s : α → Formula α} {φ ψ : Formula α} : subst s (φ ⋎ ψ) = subst s φ ⋎ subst s ψ

@[simp]

theorem LO.IntProp.Formula.subst_imp {α : Type u_1} {s : α → Formula α} {φ ψ : Formula α} : subst s (φ ➝ ψ) = subst s φ ➝ subst s ψ

@[simp]

theorem LO.IntProp.Formula.subst_neg {α : Type u_1} {s : α → Formula α} {φ : Formula α} : subst s (∼φ) = ∼subst s φ

@[simp]

theorem LO.IntProp.Formula.subst_top {α : Type u_1} {s : α → Formula α} : subst s ⊤ = ⊤

@[simp]

theorem LO.IntProp.Formula.subst_bot {α : Type u_1} {s : α → Formula α} : subst s ⊥ = ⊥

@[reducible, inline]

abbrev LO.IntProp.Theory (α : Type u) : Type u

Equations

• LO.IntProp.Theory α = Set (LO.IntProp.Formula α)

@[reducible, inline]

abbrev LO.IntProp.Context (α : Type u) : Type u

Equations

• LO.IntProp.Context α = Finset (LO.IntProp.Formula α)