Formulas of intuitionistic first-order logic

This file defines the formulas of first-order logic.

φ : Semiformulaᵢ L ξ n is a (semi-)formula of language L with bounded variables of Fin n and free variables of ξ. The quantification is represented by de Bruijn index.

inductive LO.FirstOrder.Semiformulaᵢ (L : Language) (ξ : Type u_1) : ℕ → Type (max u_1 u_2)

• falsum {L : Language} {ξ : Type u_1} {n : ℕ} : Semiformulaᵢ L ξ n
• rel {L : Language} {ξ : Type u_1} {n arity : ℕ} : L.Rel arity → (Fin arity → Semiterm L ξ n) → Semiformulaᵢ L ξ n
• and {L : Language} {ξ : Type u_1} {n : ℕ} : Semiformulaᵢ L ξ n → Semiformulaᵢ L ξ n → Semiformulaᵢ L ξ n
• or {L : Language} {ξ : Type u_1} {n : ℕ} : Semiformulaᵢ L ξ n → Semiformulaᵢ L ξ n → Semiformulaᵢ L ξ n
• imp {L : Language} {ξ : Type u_1} {n : ℕ} : Semiformulaᵢ L ξ n → Semiformulaᵢ L ξ n → Semiformulaᵢ L ξ n
• all {L : Language} {ξ : Type u_1} {n : ℕ} : Semiformulaᵢ L ξ (n + 1) → Semiformulaᵢ L ξ n
• exs {L : Language} {ξ : Type u_1} {n : ℕ} : Semiformulaᵢ L ξ (n + 1) → Semiformulaᵢ L ξ n

@[reducible, inline]

abbrev LO.FirstOrder.Formulaᵢ (L : Language) (ξ : Type u_1) : Type (max u_1 u_2)

Equations

• LO.FirstOrder.Formulaᵢ L ξ = LO.FirstOrder.Semiformulaᵢ L ξ 0

@[reducible, inline]

abbrev LO.FirstOrder.Sentenceᵢ (L : Language) : Type u_1

Equations

• LO.FirstOrder.Sentenceᵢ L = LO.FirstOrder.Formulaᵢ L Empty

@[reducible, inline]

abbrev LO.FirstOrder.Semisentenceᵢ (L : Language) (n : ℕ) : Type u_1

Equations

• LO.FirstOrder.Semisentenceᵢ L n = LO.FirstOrder.Semiformulaᵢ L Empty n

@[reducible, inline]

abbrev LO.FirstOrder.Semipropositionᵢ (L : Language) (n : ℕ) : Type u_1

Equations

• LO.FirstOrder.Semipropositionᵢ L n = LO.FirstOrder.Semiformulaᵢ L ℕ n

@[reducible, inline]

abbrev LO.FirstOrder.Propositionᵢ (L : Language) : Type u_1

Equations

• LO.FirstOrder.Propositionᵢ L = LO.FirstOrder.Semipropositionᵢ L 0

@[implicit_reducible]

instance LO.FirstOrder.Semiformulaᵢ.instBot {L : Language} {ξ : Type u_2} {n : ℕ} : Bot (Semiformulaᵢ L ξ n)

Equations

• LO.FirstOrder.Semiformulaᵢ.instBot = { bot := LO.FirstOrder.Semiformulaᵢ.falsum }

@[implicit_reducible]

instance LO.FirstOrder.Semiformulaᵢ.instArrow {L : Language} {ξ : Type u_2} {n : ℕ} : Arrow (Semiformulaᵢ L ξ n)

Equations

• LO.FirstOrder.Semiformulaᵢ.instArrow = { arrow := LO.FirstOrder.Semiformulaᵢ.imp }

@[reducible, inline]

abbrev LO.FirstOrder.Semiformulaᵢ.neg {L : Language} {ξ : Type u_2} {n : ℕ} (φ : Semiformulaᵢ L ξ n) : Semiformulaᵢ L ξ n

Equations

• φ.neg = φ 🡒 ⊥

@[reducible, inline]

abbrev LO.FirstOrder.Semiformulaᵢ.verum {L : Language} {ξ : Type u_2} {n : ℕ} : Semiformulaᵢ L ξ n

Equations

• LO.FirstOrder.Semiformulaᵢ.verum = ⊥ 🡒 ⊥

@[implicit_reducible]

instance LO.FirstOrder.Semiformulaᵢ.instLogicalConnective {L : Language} {ξ : Type u_2} {n : ℕ} : LogicalConnective (Semiformulaᵢ L ξ n)

Equations

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

theorem LO.FirstOrder.Semiformulaᵢ.neg_def {L : Language} {ξ : Type u_1} {n : ℕ} (φ : Semiformulaᵢ L ξ n) : ∼φ = φ 🡒 ⊥

theorem LO.FirstOrder.Semiformulaᵢ.verum_def {L : Language} {ξ : Type u_1} {n : ℕ} : ⊤ = ⊥ 🡒 ⊥

@[implicit_reducible]

instance LO.FirstOrder.Semiformulaᵢ.instQuantifier {L : Language} {ξ : Type u_2} : Quantifier (Semiformulaᵢ L ξ)

Equations

• LO.FirstOrder.Semiformulaᵢ.instQuantifier = { all := fun {n : ℕ} => LO.FirstOrder.Semiformulaᵢ.all, exs := fun {n : ℕ} => LO.FirstOrder.Semiformulaᵢ.exs }

def LO.FirstOrder.Semiformulaᵢ.toStr {ξ : Type u_1} {L : Language} [(k : ℕ) → ToString (L.Func k)] [(k : ℕ) → ToString (L.Rel k)] [ToString ξ] {n : ℕ} : Semiformulaᵢ L ξ n → String

Equations

• LO.FirstOrder.Semiformulaᵢ.falsum.toStr = "\\bot"
• (LO.FirstOrder.Semiformulaᵢ.rel r a).toStr = "{" ++ toString r ++ "}"
• (LO.FirstOrder.Semiformulaᵢ.rel r v).toStr = ("{" ++ toString r ++ "} \\left(" ++ String.vecToStr fun (i : Fin (n + 1)) => toString (v i)) ++ "\\right)"
• (φ.and ψ).toStr = "\\left(" ++ φ.toStr ++ " \\land " ++ ψ.toStr ++ "\\right)"
• (φ.or ψ).toStr = "\\left(" ++ φ.toStr ++ " \\lor " ++ ψ.toStr ++ "\\right)"
• (φ.imp ψ).toStr = "\\left(" ++ φ.toStr ++ " \\to " ++ ψ.toStr ++ "\\right)"
• φ.all.toStr = "(\\forall x_{" ++ toString x✝ ++ "}) " ++ φ.toStr
• φ.exs.toStr = "(\\exists x_{" ++ toString x✝ ++ "}) " ++ φ.toStr

@[implicit_reducible]

instance LO.FirstOrder.Semiformulaᵢ.instRepr {ξ : Type u_1} {L : Language} [(k : ℕ) → ToString (L.Func k)] [(k : ℕ) → ToString (L.Rel k)] [ToString ξ] {n : ℕ} : Repr (Semiformulaᵢ L ξ n)

Equations

• LO.FirstOrder.Semiformulaᵢ.instRepr = { reprPrec := fun (t : LO.FirstOrder.Semiformulaᵢ L ξ n) (x : ℕ) => Std.Format.text t.toStr }

@[implicit_reducible]

instance LO.FirstOrder.Semiformulaᵢ.instToString {ξ : Type u_1} {L : Language} [(k : ℕ) → ToString (L.Func k)] [(k : ℕ) → ToString (L.Rel k)] [ToString ξ] {n : ℕ} : ToString (Semiformulaᵢ L ξ n)

Equations

• LO.FirstOrder.Semiformulaᵢ.instToString = { toString := LO.FirstOrder.Semiformulaᵢ.toStr }

@[simp]

theorem LO.FirstOrder.Semiformulaᵢ.and_inj {L : Language} {ξ : Type u_1} {n : ℕ} (φ₁ ψ₁ φ₂ ψ₂ : Semiformulaᵢ L ξ n) : φ₁ ⋏ φ₂ = ψ₁ ⋏ ψ₂ ↔ φ₁ = ψ₁ ∧ φ₂ = ψ₂

@[simp]

theorem LO.FirstOrder.Semiformulaᵢ.or_inj {L : Language} {ξ : Type u_1} {n : ℕ} (φ₁ ψ₁ φ₂ ψ₂ : Semiformulaᵢ L ξ n) : φ₁ ⋎ φ₂ = ψ₁ ⋎ ψ₂ ↔ φ₁ = ψ₁ ∧ φ₂ = ψ₂

@[simp]

theorem LO.FirstOrder.Semiformulaᵢ.imp_inj {L : Language} {ξ : Type u_1} {n : ℕ} {φ₁ φ₂ ψ₁ ψ₂ : Semiformulaᵢ L ξ n} : φ₁ 🡒 φ₂ = ψ₁ 🡒 ψ₂ ↔ φ₁ = ψ₁ ∧ φ₂ = ψ₂

@[simp]

theorem LO.FirstOrder.Semiformulaᵢ.all_inj {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformulaᵢ L ξ (n + 1)) : ∀¹ φ = ∀¹ ψ ↔ φ = ψ

@[simp]

theorem LO.FirstOrder.Semiformulaᵢ.exs_inj {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformulaᵢ L ξ (n + 1)) : ∃¹ φ = ∃¹ ψ ↔ φ = ψ

@[simp]

theorem LO.FirstOrder.Semiformulaᵢ.allClosure_inj {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformulaᵢ L ξ n) : ∀¹* φ = ∀¹* ψ ↔ φ = ψ

@[simp]

theorem LO.FirstOrder.Semiformulaᵢ.exsClosure_inj {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformulaᵢ L ξ n) : ∃¹* φ = ∃¹* ψ ↔ φ = ψ

@[simp]

theorem LO.FirstOrder.Semiformulaᵢ.allItr_inj {L : Language} {ξ : Type u_1} {n k : ℕ} (φ ψ : Semiformulaᵢ L ξ (n + k)) : ∀¹^[k] φ = ∀¹^[k] ψ ↔ φ = ψ

@[simp]

theorem LO.FirstOrder.Semiformulaᵢ.exsItr_inj {L : Language} {ξ : Type u_1} {n k : ℕ} (φ ψ : Semiformulaᵢ L ξ (n + k)) : ∃¹^[k] φ = ∃¹^[k] ψ ↔ φ = ψ

def LO.FirstOrder.Semiformulaᵢ.complexity {L : Language} {ξ : Type u_2} {n : ℕ} : Semiformulaᵢ L ξ n → ℕ

Equations

• LO.FirstOrder.Semiformulaᵢ.falsum.complexity = 0
• (LO.FirstOrder.Semiformulaᵢ.rel a a_1).complexity = 0
• (φ.and ψ).complexity = max φ.complexity ψ.complexity + 1
• (φ.or ψ).complexity = max φ.complexity ψ.complexity + 1
• (φ.imp ψ).complexity = max φ.complexity ψ.complexity + 1
• φ.all.complexity = φ.complexity + 1
• φ.exs.complexity = φ.complexity + 1

@[simp]

theorem LO.FirstOrder.Semiformulaᵢ.complexity_top {L : Language} {ξ : Type u_1} {n : ℕ} : ⊤.complexity = 1

@[simp]

theorem LO.FirstOrder.Semiformulaᵢ.complexity_bot {L : Language} {ξ : Type u_1} {n : ℕ} : ⊥.complexity = 0

@[simp]

theorem LO.FirstOrder.Semiformulaᵢ.complexity_rel {L : Language} {ξ : Type u_1} {n k : ℕ} (r : L.Rel k) (v : Fin k → Semiterm L ξ n) : (rel r v).complexity = 0

@[simp]

theorem LO.FirstOrder.Semiformulaᵢ.complexity_and {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformulaᵢ L ξ n) : (φ ⋏ ψ).complexity = max φ.complexity ψ.complexity + 1

@[simp]

theorem LO.FirstOrder.Semiformulaᵢ.complexity_and' {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformulaᵢ L ξ n) : (φ.and ψ).complexity = max φ.complexity ψ.complexity + 1

@[simp]

theorem LO.FirstOrder.Semiformulaᵢ.complexity_or {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformulaᵢ L ξ n) : (φ ⋎ ψ).complexity = max φ.complexity ψ.complexity + 1

@[simp]

theorem LO.FirstOrder.Semiformulaᵢ.complexity_or' {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformulaᵢ L ξ n) : (φ.or ψ).complexity = max φ.complexity ψ.complexity + 1

@[simp]

theorem LO.FirstOrder.Semiformulaᵢ.complexity_imp {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformulaᵢ L ξ n) : (φ 🡒 ψ).complexity = max φ.complexity ψ.complexity + 1

@[simp]

theorem LO.FirstOrder.Semiformulaᵢ.complexity_imp' {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformulaᵢ L ξ n) : (φ.imp ψ).complexity = max φ.complexity ψ.complexity + 1

@[simp]

theorem LO.FirstOrder.Semiformulaᵢ.complexity_all {L : Language} {ξ : Type u_1} {n : ℕ} (φ : Semiformulaᵢ L ξ (n + 1)) : (∀¹ φ).complexity = φ.complexity + 1

@[simp]

theorem LO.FirstOrder.Semiformulaᵢ.complexity_all' {L : Language} {ξ : Type u_1} {n : ℕ} (φ : Semiformulaᵢ L ξ (n + 1)) : φ.all.complexity = φ.complexity + 1

@[simp]

theorem LO.FirstOrder.Semiformulaᵢ.complexity_exs {L : Language} {ξ : Type u_1} {n : ℕ} (φ : Semiformulaᵢ L ξ (n + 1)) : (∃¹ φ).complexity = φ.complexity + 1

@[simp]

theorem LO.FirstOrder.Semiformulaᵢ.complexity_exs' {L : Language} {ξ : Type u_1} {n : ℕ} (φ : Semiformulaᵢ L ξ (n + 1)) : φ.exs.complexity = φ.complexity + 1

@[simp]

theorem LO.FirstOrder.Semiformulaᵢ.complexity_neg {L : Language} {ξ : Type u_1} {n : ℕ} (φ : Semiformulaᵢ L ξ n) : (∼φ).complexity = φ.complexity + 1

def LO.FirstOrder.Semiformulaᵢ.cases' {L : Language} {ξ : Type u_2} {C : (n : ℕ) → Semiformulaᵢ L ξ n → Sort w} (hRel : {n k : ℕ} → (r : L.Rel k) → (v : Fin k → Semiterm L ξ n) → C n (rel r v)) (hFalsum : {n : ℕ} → C n ⊥) (hAnd : {n : ℕ} → (φ ψ : Semiformulaᵢ L ξ n) → C n (φ ⋏ ψ)) (hOr : {n : ℕ} → (φ ψ : Semiformulaᵢ L ξ n) → C n (φ ⋎ ψ)) (hImp : {n : ℕ} → (φ ψ : Semiformulaᵢ L ξ n) → C n (φ 🡒 ψ)) (hAll : {n : ℕ} → (φ : Semiformulaᵢ L ξ (n + 1)) → C n (∀¹ φ)) (hExs : {n : ℕ} → (φ : Semiformulaᵢ L ξ (n + 1)) → C n (∃¹ φ)) {n : ℕ} (φ : Semiformulaᵢ L ξ n) : C n φ

Equations

• LO.FirstOrder.Semiformulaᵢ.cases' hRel hFalsum hAnd hOr hImp hAll hExs (LO.FirstOrder.Semiformulaᵢ.rel r v) = hRel r v
• LO.FirstOrder.Semiformulaᵢ.cases' hRel hFalsum hAnd hOr hImp hAll hExs LO.FirstOrder.Semiformulaᵢ.falsum = hFalsum
• LO.FirstOrder.Semiformulaᵢ.cases' hRel hFalsum hAnd hOr hImp hAll hExs (φ.and ψ) = hAnd φ ψ
• LO.FirstOrder.Semiformulaᵢ.cases' hRel hFalsum hAnd hOr hImp hAll hExs (φ.or ψ) = hOr φ ψ
• LO.FirstOrder.Semiformulaᵢ.cases' hRel hFalsum hAnd hOr hImp hAll hExs (φ.imp ψ) = hImp φ ψ
• LO.FirstOrder.Semiformulaᵢ.cases' hRel hFalsum hAnd hOr hImp hAll hExs φ.all = hAll φ
• LO.FirstOrder.Semiformulaᵢ.cases' hRel hFalsum hAnd hOr hImp hAll hExs φ.exs = hExs φ

def LO.FirstOrder.Semiformulaᵢ.rec' {L : Language} {ξ : Type u_2} {C : (n : ℕ) → Semiformulaᵢ L ξ n → Sort w} (hRel : {n k : ℕ} → (r : L.Rel k) → (v : Fin k → Semiterm L ξ n) → C n (rel r v)) (hFalsum : {n : ℕ} → C n ⊥) (hAnd : {n : ℕ} → (φ ψ : Semiformulaᵢ L ξ n) → C n φ → C n ψ → C n (φ ⋏ ψ)) (hOr : {n : ℕ} → (φ ψ : Semiformulaᵢ L ξ n) → C n φ → C n ψ → C n (φ ⋎ ψ)) (hImp : {n : ℕ} → (φ ψ : Semiformulaᵢ L ξ n) → C n φ → C n ψ → C n (φ 🡒 ψ)) (hAll : {n : ℕ} → (φ : Semiformulaᵢ L ξ (n + 1)) → C (n + 1) φ → C n (∀¹ φ)) (hExs : {n : ℕ} → (φ : Semiformulaᵢ L ξ (n + 1)) → C (n + 1) φ → C n (∃¹ φ)) {n : ℕ} (φ : Semiformulaᵢ L ξ n) : C n φ

Equations

• One or more equations did not get rendered due to their size.
• LO.FirstOrder.Semiformulaᵢ.rec' hRel hFalsum hAnd hOr hImp hAll hExs (LO.FirstOrder.Semiformulaᵢ.rel r v) = hRel r v
• LO.FirstOrder.Semiformulaᵢ.rec' hRel hFalsum hAnd hOr hImp hAll hExs LO.FirstOrder.Semiformulaᵢ.falsum = hFalsum

def LO.FirstOrder.Semiformulaᵢ.hasDecEq {ξ : Type u_1} {L : Language} [L.DecidableEq] [DecidableEq ξ] {n : ℕ} (φ ψ : Semiformulaᵢ L ξ n) : Decidable (φ = ψ)

Equations

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

@[implicit_reducible]

instance LO.FirstOrder.Semiformulaᵢ.instDecidableEq {ξ : Type u_1} {L : Language} [L.DecidableEq] [DecidableEq ξ] {n : ℕ} : DecidableEq (Semiformulaᵢ L ξ n)

Equations

• LO.FirstOrder.Semiformulaᵢ.instDecidableEq = LO.FirstOrder.Semiformulaᵢ.hasDecEq

(Weak) Negative formula

inductive LO.FirstOrder.Semiformulaᵢ.IsNegative {L : Language} {ξ : Type u_2} {n : ℕ} : Semiformulaᵢ L ξ n → Prop

• falsum {L : Language} {ξ : Type u_2} {n : ℕ} : ⊥.IsNegative
• and {L : Language} {ξ : Type u_2} {n : ℕ} {φ ψ : Semiformulaᵢ L ξ n} : φ.IsNegative → ψ.IsNegative → (φ ⋏ ψ).IsNegative
• imply {L : Language} {ξ : Type u_2} {n : ℕ} {φ ψ : Semiformulaᵢ L ξ n} : ψ.IsNegative → (φ 🡒 ψ).IsNegative
• all {L : Language} {ξ : Type u_2} {n : ℕ} {φ : Semiformulaᵢ L ξ (n + 1)} : φ.IsNegative → (∀¹ φ).IsNegative

@[simp]

theorem LO.FirstOrder.Semiformulaᵢ.IsNegative.and_iff {L : Language} {ξ : Type u_1} {n : ℕ} {φ ψ : Semiformulaᵢ L ξ n} : (φ ⋏ ψ).IsNegative ↔ φ.IsNegative ∧ ψ.IsNegative

@[simp]

theorem LO.FirstOrder.Semiformulaᵢ.IsNegative.imp_iff {L : Language} {ξ : Type u_1} {n : ℕ} {φ ψ : Semiformulaᵢ L ξ n} : (φ 🡒 ψ).IsNegative ↔ ψ.IsNegative

@[simp]

theorem LO.FirstOrder.Semiformulaᵢ.IsNegative.all_iff {L : Language} {ξ : Type u_1} {n : ℕ} {φ : Semiformulaᵢ L ξ (n + 1)} : (∀¹ φ).IsNegative ↔ φ.IsNegative

@[simp]

theorem LO.FirstOrder.Semiformulaᵢ.IsNegative.verum {L : Language} {ξ : Type u_1} {n : ℕ} : ⊤.IsNegative

@[simp]

theorem LO.FirstOrder.Semiformulaᵢ.IsNegative.not_or {L : Language} {ξ : Type u_1} {n : ℕ} {φ ψ : Semiformulaᵢ L ξ n} : ¬(φ ⋎ ψ).IsNegative

@[simp]

theorem LO.FirstOrder.Semiformulaᵢ.IsNegative.not_exs {L : Language} {ξ : Type u_1} {n : ℕ} {φ : Semiformulaᵢ L ξ (n + 1)} : ¬(∃¹ φ).IsNegative

@[simp]

theorem LO.FirstOrder.Semiformulaᵢ.IsNegative.not_rel {L : Language} {ξ : Type u_1} {n k : ℕ} (r : L.Rel k) (v : Fin k → Semiterm L ξ n) : ¬(rel r v).IsNegative

@[simp]

theorem LO.FirstOrder.Semiformulaᵢ.IsNegative.neg {L : Language} {ξ : Type u_1} {n : ℕ} (φ : Semiformulaᵢ L ξ n) : (∼φ).IsNegative