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 : LO.FirstOrder.Language) (ξ : Type u_1) : ℕ → Type (max u_1 u_2)

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

@[reducible, inline]

abbrev LO.FirstOrder.Formulaᵢ (L : LO.FirstOrder.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 : LO.FirstOrder.Language) : Type u_1

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

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

Equations

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

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

Equations

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

@[reducible, inline]

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

Equations

• φ.neg = φ ➝ ⊥

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

Equations

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

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

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

Equations

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

def LO.FirstOrder.Semiformulaᵢ.toStr {ξ : Type u_1} {L : LO.FirstOrder.Language} [(k : ℕ) → ToString (L.Func k)] [(k : ℕ) → ToString (L.Rel k)] [ToString ξ] {n : ℕ} : LO.FirstOrder.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 : LO.FirstOrder.Language} [(k : ℕ) → ToString (L.Func k)] [(k : ℕ) → ToString (L.Rel k)] [ToString ξ] {n : ℕ} : Repr (LO.FirstOrder.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 : LO.FirstOrder.Language} [(k : ℕ) → ToString (L.Func k)] [(k : ℕ) → ToString (L.Rel k)] [ToString ξ] {n : ℕ} : ToString (LO.FirstOrder.Semiformulaᵢ L ξ n)

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def LO.FirstOrder.Semiformulaᵢ.complexity {L : LO.FirstOrder.Language} {ξ : Type u_2} {n : ℕ} : LO.FirstOrder.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 : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} : ⊤.complexity = 0

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def LO.FirstOrder.Semiformulaᵢ.cases' {L : LO.FirstOrder.Language} {ξ : Type u_2} {C : (n : ℕ) → LO.FirstOrder.Semiformulaᵢ L ξ n → Sort w} (hRel : {n k : ℕ} → (r : L.Rel k) → (v : Fin k → LO.FirstOrder.Semiterm L ξ n) → C n (LO.FirstOrder.Semiformulaᵢ.rel r v)) (hVerum : {n : ℕ} → C n ⊤) (hFalsum : {n : ℕ} → C n ⊥) (hAnd : {n : ℕ} → (φ ψ : LO.FirstOrder.Semiformulaᵢ L ξ n) → C n (φ ⋏ ψ)) (hOr : {n : ℕ} → (φ ψ : LO.FirstOrder.Semiformulaᵢ L ξ n) → C n (φ ⋎ ψ)) (hImp : {n : ℕ} → (φ ψ : LO.FirstOrder.Semiformulaᵢ L ξ n) → C n (φ ➝ ψ)) (hAll : {n : ℕ} → (φ : LO.FirstOrder.Semiformulaᵢ L ξ (n + 1)) → C n (∀' φ)) (hEx : {n : ℕ} → (φ : LO.FirstOrder.Semiformulaᵢ L ξ (n + 1)) → C n (∃' φ)) {n : ℕ} (φ : LO.FirstOrder.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 : LO.FirstOrder.Language} {ξ : Type u_2} {C : (n : ℕ) → LO.FirstOrder.Semiformulaᵢ L ξ n → Sort w} (hRel : {n k : ℕ} → (r : L.Rel k) → (v : Fin k → LO.FirstOrder.Semiterm L ξ n) → C n (LO.FirstOrder.Semiformulaᵢ.rel r v)) (hVerum : {n : ℕ} → C n ⊤) (hFalsum : {n : ℕ} → C n ⊥) (hAnd : {n : ℕ} → (φ ψ : LO.FirstOrder.Semiformulaᵢ L ξ n) → C n φ → C n ψ → C n (φ ⋏ ψ)) (hOr : {n : ℕ} → (φ ψ : LO.FirstOrder.Semiformulaᵢ L ξ n) → C n φ → C n ψ → C n (φ ⋎ ψ)) (hImp : {n : ℕ} → (φ ψ : LO.FirstOrder.Semiformulaᵢ L ξ n) → C n φ → C n ψ → C n (φ ➝ ψ)) (hAll : {n : ℕ} → (φ : LO.FirstOrder.Semiformulaᵢ L ξ (n + 1)) → C (n + 1) φ → C n (∀' φ)) (hEx : {n : ℕ} → (φ : LO.FirstOrder.Semiformulaᵢ L ξ (n + 1)) → C (n + 1) φ → C n (∃' φ)) {n : ℕ} (φ : LO.FirstOrder.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 : LO.FirstOrder.Language} [L.DecidableEq] [DecidableEq ξ] {n : ℕ} (φ ψ : LO.FirstOrder.Semiformulaᵢ L ξ n) : Decidable (φ = ψ)

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

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

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

Equations

• LO.FirstOrder.instCollectionSyntacticFormulaᵢTheoryᵢ = inferInstance

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

Equations

• LO.FirstOrder.instCollectionSentenceᵢClosedTheoryᵢ = inferInstance

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

Equations

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

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

Negative Formula

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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