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)

• verum {L : Language} {ξ : Type u_1} {n : ℕ} : Semiformulaᵢ L ξ n
• 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
• ex {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.SyntacticSemiformulaᵢ (L : Language) (n : ℕ) : Type u_1

Equations

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

@[reducible, inline]

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

Equations

• LO.FirstOrder.SyntacticFormulaᵢ L = LO.FirstOrder.SyntacticSemiformulaᵢ L 0

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 }

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 = φ ➝ ⊥

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

Equations

• LO.FirstOrder.Semiformulaᵢ.instLogicalConnective = LO.LogicalConnective.mk

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

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

Equations

• LO.FirstOrder.Semiformulaᵢ.instQuantifier = LO.Quantifier.mk

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ᵢ.verum.toStr = "\top"
• 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
• φ.ex.toStr = "(\exists x_{" ++ toString x✝ ++ "}) " ++ φ.toStr

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 }

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ᵢ.ex_inj {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformulaᵢ L ξ (n + 1)) : ∃' φ = ∃' ψ ↔ φ = ψ

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem LO.FirstOrder.Semiformulaᵢ.exItr_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ᵢ.verum.complexity = 0
• LO.FirstOrder.Semiformulaᵢ.falsum.complexity = 0
• (LO.FirstOrder.Semiformulaᵢ.rel a a_1).complexity = 0
• (φ.and ψ).complexity = φ.complexity ⊔ ψ.complexity + 1
• (φ.or ψ).complexity = φ.complexity ⊔ ψ.complexity + 1
• (φ.imp ψ).complexity = φ.complexity ⊔ ψ.complexity + 1
• φ.all.complexity = φ.complexity + 1
• φ.ex.complexity = φ.complexity + 1

@[simp]

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

@[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 = φ.complexity ⊔ ψ.complexity + 1

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem LO.FirstOrder.Semiformulaᵢ.complexity_imp' {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformulaᵢ L ξ n) : (φ.imp ψ).complexity = φ.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_ex {L : Language} {ξ : Type u_1} {n : ℕ} (φ : Semiformulaᵢ L ξ (n + 1)) : (∃' φ).complexity = φ.complexity + 1

@[simp]

theorem LO.FirstOrder.Semiformulaᵢ.complexity_ex' {L : Language} {ξ : Type u_1} {n : ℕ} (φ : Semiformulaᵢ L ξ (n + 1)) : φ.ex.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)) (hVerum : {n : ℕ} → C n ⊤) (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 (∀' φ)) (hEx : {n : ℕ} → (φ : Semiformulaᵢ L ξ (n + 1)) → C n (∃' φ)) {n : ℕ} (φ : Semiformulaᵢ L ξ n) : C n φ

Equations

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

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)) (hVerum : {n : ℕ} → C n ⊤) (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 (∀' φ)) (hEx : {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 hVerum hFalsum hAnd hOr hImp hAll hEx (LO.FirstOrder.Semiformulaᵢ.rel r v) = hRel r v
• LO.FirstOrder.Semiformulaᵢ.rec' hRel hVerum hFalsum hAnd hOr hImp hAll hEx LO.FirstOrder.Semiformulaᵢ.verum = hVerum
• LO.FirstOrder.Semiformulaᵢ.rec' hRel hVerum hFalsum hAnd hOr hImp hAll hEx LO.FirstOrder.Semiformulaᵢ.falsum = hFalsum

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

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

@[reducible, inline]

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

Equations

• LO.FirstOrder.Theoryᵢ L = Set (LO.FirstOrder.SyntacticFormulaᵢ L)

@[reducible, inline]

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

Equations

• LO.FirstOrder.ClosedTheoryᵢ L = Set (LO.FirstOrder.Sentenceᵢ L)

instance LO.FirstOrder.instCollectionSyntacticFormulaᵢTheoryᵢ {L : Language} : Collection (SyntacticFormulaᵢ L) (Theoryᵢ L)

Equations

• LO.FirstOrder.instCollectionSyntacticFormulaᵢTheoryᵢ = inferInstance

instance LO.FirstOrder.instCollectionSentenceᵢClosedTheoryᵢ {L : Language} : Collection (Sentenceᵢ L) (ClosedTheoryᵢ L)

Equations

• LO.FirstOrder.instCollectionSentenceᵢClosedTheoryᵢ = inferInstance

instance LO.FirstOrder.Theoryᵢ.instAdd {L : Language} : Add (Theoryᵢ L)

Equations

• LO.FirstOrder.Theoryᵢ.instAdd = { add := fun (x1 x2 : LO.FirstOrder.Theoryᵢ L) => x1 ∪ x2 }

theorem LO.FirstOrder.Theoryᵢ.add_def {L : Language} (T U : Theoryᵢ L) : T + U = T ∪ U

(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.not_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_ex {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