Formula

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

Imported declaration from the Incompleteness formalization.

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

def LO.IntProp.instDecidableEqFormula.decEq {α✝ : Type u_1} [DecidableEq α✝] (x✝ x✝¹ : Formula α✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• LO.IntProp.instDecidableEqFormula.decEq (LO.IntProp.Formula.atom a) (LO.IntProp.Formula.atom b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• LO.IntProp.instDecidableEqFormula.decEq (LO.IntProp.Formula.atom a) LO.IntProp.Formula.falsum = isFalse ⋯
• LO.IntProp.instDecidableEqFormula.decEq (LO.IntProp.Formula.atom a) (a_1.and a_2) = isFalse ⋯
• LO.IntProp.instDecidableEqFormula.decEq (LO.IntProp.Formula.atom a) (a_1.or a_2) = isFalse ⋯
• LO.IntProp.instDecidableEqFormula.decEq (LO.IntProp.Formula.atom a) (a_1.imp a_2) = isFalse ⋯
• LO.IntProp.instDecidableEqFormula.decEq LO.IntProp.Formula.falsum (LO.IntProp.Formula.atom a) = isFalse ⋯
• LO.IntProp.instDecidableEqFormula.decEq LO.IntProp.Formula.falsum LO.IntProp.Formula.falsum = isTrue ⋯
• LO.IntProp.instDecidableEqFormula.decEq LO.IntProp.Formula.falsum (a.and a_1) = isFalse ⋯
• LO.IntProp.instDecidableEqFormula.decEq LO.IntProp.Formula.falsum (a.or a_1) = isFalse ⋯
• LO.IntProp.instDecidableEqFormula.decEq LO.IntProp.Formula.falsum (a.imp a_1) = isFalse ⋯
• LO.IntProp.instDecidableEqFormula.decEq (a.and a_1) (LO.IntProp.Formula.atom a_2) = isFalse ⋯
• LO.IntProp.instDecidableEqFormula.decEq (a.and a_1) LO.IntProp.Formula.falsum = isFalse ⋯
• LO.IntProp.instDecidableEqFormula.decEq (a.and a_1) (a_2.or a_3) = isFalse ⋯
• LO.IntProp.instDecidableEqFormula.decEq (a.and a_1) (a_2.imp a_3) = isFalse ⋯
• LO.IntProp.instDecidableEqFormula.decEq (a.or a_1) (LO.IntProp.Formula.atom a_2) = isFalse ⋯
• LO.IntProp.instDecidableEqFormula.decEq (a.or a_1) LO.IntProp.Formula.falsum = isFalse ⋯
• LO.IntProp.instDecidableEqFormula.decEq (a.or a_1) (a_2.and a_3) = isFalse ⋯
• LO.IntProp.instDecidableEqFormula.decEq (a.or a_1) (a_2.imp a_3) = isFalse ⋯
• LO.IntProp.instDecidableEqFormula.decEq (a.imp a_1) (LO.IntProp.Formula.atom a_2) = isFalse ⋯
• LO.IntProp.instDecidableEqFormula.decEq (a.imp a_1) LO.IntProp.Formula.falsum = isFalse ⋯
• LO.IntProp.instDecidableEqFormula.decEq (a.imp a_1) (a_2.and a_3) = isFalse ⋯
• LO.IntProp.instDecidableEqFormula.decEq (a.imp a_1) (a_2.or a_3) = isFalse ⋯

@[implicit_reducible]

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

Equations

• LO.IntProp.instDecidableEqFormula = LO.IntProp.instDecidableEqFormula.decEq

@[reducible, inline]

abbrev LO.IntProp.Formula.neg {α : Type u} (φ : Formula α) : Formula α

Imported declaration from the Incompleteness formalization.

Equations

• φ.neg = φ.imp LO.IntProp.Formula.falsum

@[reducible, inline]

abbrev LO.IntProp.Formula.verum {α : Type u} : Formula α

Imported declaration from the Incompleteness formalization.

Equations

• LO.IntProp.Formula.verum = LO.IntProp.Formula.falsum.imp LO.IntProp.Formula.falsum

@[implicit_reducible]

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

Equations

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

instance LO.IntProp.Formula.instNegAbbrev {α : Type u_1} : NegAbbrev (Formula α)

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[implicit_reducible]

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 }

@[implicit_reducible]

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.neg_def {α : Type u_1} (φ : Formula α) : ∼φ = φ ==> ⊥

theorem LO.IntProp.Formula.top_def {α : Type u_1} : ⊤ = ⊥ ==> ⊥

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[simp]

theorem LO.IntProp.Formula.complexity_bot {α : 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 = max φ.complexity ψ.complexity + 1

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

• LO.IntProp.Formula.rec' hfalsum hatom himp hand hor LO.IntProp.Formula.falsum = hfalsum
• LO.IntProp.Formula.rec' hfalsum hatom himp hand hor (LO.IntProp.Formula.atom a) = hatom a
• LO.IntProp.Formula.rec' hfalsum hatom himp hand hor (φ.imp ψ) = himp φ ψ (LO.IntProp.Formula.rec' hfalsum hatom himp hand hor φ) (LO.IntProp.Formula.rec' hfalsum hatom himp hand hor ψ)
• LO.IntProp.Formula.rec' hfalsum hatom himp hand hor (φ.and ψ) = hand φ ψ (LO.IntProp.Formula.rec' hfalsum hatom himp hand hor φ) (LO.IntProp.Formula.rec' hfalsum hatom himp hand hor ψ)
• LO.IntProp.Formula.rec' hfalsum hatom himp hand hor (φ.or ψ) = hor φ ψ (LO.IntProp.Formula.rec' hfalsum hatom himp hand hor φ) (LO.IntProp.Formula.rec' hfalsum hatom himp hand hor ψ)

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

Imported declaration from the Incompleteness formalization.

Equations

• x✝¹.hasDecEq x✝ = inferInstance

@[implicit_reducible]

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 α → ℕ

Imported declaration from the Incompleteness formalization.

Equations

• LO.IntProp.Formula.falsum.toNat = Nat.pair 0 0 + 1
• (LO.IntProp.Formula.atom a).toNat = Nat.pair 1 (Encodable.encode a) + 1
• (φ.imp ψ).toNat = Nat.pair 2 (Nat.pair φ.toNat ψ.toNat) + 1
• (φ.and ψ).toNat = Nat.pair 3 (Nat.pair φ.toNat ψ.toNat) + 1
• (φ.or ψ).toNat = Nat.pair 4 (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 φ

@[implicit_reducible]

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 := ⋯ }

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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