@[reducible, inline]

abbrev LO.FirstOrder.Sequent (L : LO.FirstOrder.Language) : Type u_1

Equations

• LO.FirstOrder.Sequent L = List (LO.FirstOrder.SyntacticFormula L)

inductive LO.FirstOrder.Derivation {L : LO.FirstOrder.Language} (T : LO.FirstOrder.Theory L) : LO.FirstOrder.Sequent L → Type u_1

• axL: {L : LO.FirstOrder.Language} → {T : LO.FirstOrder.Theory L} → (Γ : List (LO.FirstOrder.SyntacticFormula L)) → {k : ℕ} → (r : L.Rel k) → (v : Fin k → LO.FirstOrder.Semiterm L ℕ 0) → LO.FirstOrder.Derivation T (LO.FirstOrder.Semiformula.rel r v :: LO.FirstOrder.Semiformula.nrel r v :: Γ)
• verum: {L : LO.FirstOrder.Language} → {T : LO.FirstOrder.Theory L} → (Γ : List (LO.FirstOrder.SyntacticFormula L)) → LO.FirstOrder.Derivation T (⊤ :: Γ)
• or: {L : LO.FirstOrder.Language} → {T : LO.FirstOrder.Theory L} → {Γ : List (LO.FirstOrder.SyntacticFormula L)} → {φ ψ : LO.FirstOrder.SyntacticFormula L} → LO.FirstOrder.Derivation T (φ :: ψ :: Γ) → LO.FirstOrder.Derivation T (φ ⋎ ψ :: Γ)
• and: {L : LO.FirstOrder.Language} → {T : LO.FirstOrder.Theory L} → {Γ : List (LO.FirstOrder.SyntacticFormula L)} → {φ ψ : LO.FirstOrder.SyntacticFormula L} → LO.FirstOrder.Derivation T (φ :: Γ) → LO.FirstOrder.Derivation T (ψ :: Γ) → LO.FirstOrder.Derivation T (φ ⋏ ψ :: Γ)
• all: {L : LO.FirstOrder.Language} → {T : LO.FirstOrder.Theory L} → {Γ : List (LO.FirstOrder.SyntacticSemiformula L 0)} → {φ : LO.FirstOrder.SyntacticSemiformula L (0 + 1)} → LO.FirstOrder.Derivation T (LO.FirstOrder.Rewriting.free φ :: LO.FirstOrder.Rewriting.shifts Γ) → LO.FirstOrder.Derivation T ((∀' φ) :: Γ)
• ex: {L : LO.FirstOrder.Language} → {T : LO.FirstOrder.Theory L} → {Γ : List (LO.FirstOrder.SyntacticFormula L)} → {φ : LO.FirstOrder.SyntacticSemiformula L (Nat.succ 0)} → (t : LO.FirstOrder.Semiterm L ℕ 0) → LO.FirstOrder.Derivation T (φ/[t] :: Γ) → LO.FirstOrder.Derivation T ((∃' φ) :: Γ)
• wk: {L : LO.FirstOrder.Language} → {T : LO.FirstOrder.Theory L} → {Γ Δ : LO.FirstOrder.Sequent L} → LO.FirstOrder.Derivation T Δ → Δ ⊆ Γ → LO.FirstOrder.Derivation T Γ
• cut: {L : LO.FirstOrder.Language} → {T : LO.FirstOrder.Theory L} → {Γ : List (LO.FirstOrder.SyntacticFormula L)} → {φ : LO.FirstOrder.SyntacticFormula L} → LO.FirstOrder.Derivation T (φ :: Γ) → LO.FirstOrder.Derivation T (∼φ :: Γ) → LO.FirstOrder.Derivation T Γ
• root: {L : LO.FirstOrder.Language} → {T : LO.FirstOrder.Theory L} → {φ : LO.FirstOrder.SyntacticFormula L} → φ ∈ T → LO.FirstOrder.Derivation T [φ]

instance LO.FirstOrder.instOneSidedSyntacticFormulaTheory {L : LO.FirstOrder.Language} : LO.OneSided (LO.FirstOrder.SyntacticFormula L) (LO.FirstOrder.Theory L)

Equations

• LO.FirstOrder.instOneSidedSyntacticFormulaTheory = { Derivation := LO.FirstOrder.Derivation }

@[reducible, inline]

abbrev LO.FirstOrder.Derivation₀ {L : LO.FirstOrder.Language} (Γ : LO.FirstOrder.Sequent L) : Type u_1

Equations

• (⊢ᵀ Γ) = (∅ ⟹ Γ)

@[reducible, inline]

abbrev LO.FirstOrder.Derivable₀ {L : LO.FirstOrder.Language} (Γ : LO.FirstOrder.Sequent L) : Prop

Equations

• (⊢ᵀ! Γ) = (∅ ⟹! Γ)

def LO.FirstOrder.«term⊢ᵀ_» : Lean.ParserDescr

Equations

• LO.FirstOrder.«term⊢ᵀ_» = Lean.ParserDescr.node `LO.FirstOrder.«term⊢ᵀ_» 45 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⊢ᵀ ") (Lean.ParserDescr.cat `term 45))

def LO.FirstOrder.«term⊢ᵀ!_» : Lean.ParserDescr

Equations

• LO.FirstOrder.«term⊢ᵀ!_» = Lean.ParserDescr.node `LO.FirstOrder.«term⊢ᵀ!_» 45 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⊢ᵀ! ") (Lean.ParserDescr.cat `term 45))

def LO.FirstOrder.Derivation.length {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {Δ : LO.FirstOrder.Sequent L} : T ⟹ Δ → ℕ

Equations

• LO.FirstOrder.Derivation.length (LO.FirstOrder.Derivation.axL Γ r v) = 0
• LO.FirstOrder.Derivation.length (LO.FirstOrder.Derivation.verum Γ) = 0
• LO.FirstOrder.Derivation.length d.or = (LO.FirstOrder.Derivation.length d).succ
• LO.FirstOrder.Derivation.length (dp.and dq) = (LO.FirstOrder.Derivation.length dp ⊔ LO.FirstOrder.Derivation.length dq).succ
• LO.FirstOrder.Derivation.length d.all = (LO.FirstOrder.Derivation.length d).succ
• LO.FirstOrder.Derivation.length (LO.FirstOrder.Derivation.ex t d) = (LO.FirstOrder.Derivation.length d).succ
• LO.FirstOrder.Derivation.length (d.wk a) = (LO.FirstOrder.Derivation.length d).succ
• LO.FirstOrder.Derivation.length (dp.cut dn) = (LO.FirstOrder.Derivation.length dp ⊔ LO.FirstOrder.Derivation.length dn).succ
• LO.FirstOrder.Derivation.length (LO.FirstOrder.Derivation.root a) = 0

@[simp]

theorem LO.FirstOrder.Derivation.length_axL {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {Δ : LO.FirstOrder.Sequent L} {k : ℕ} {r : L.Rel k} {v : Fin k → LO.FirstOrder.Semiterm L ℕ 0} : LO.FirstOrder.Derivation.length (LO.FirstOrder.Derivation.axL Δ r v) = 0

@[simp]

theorem LO.FirstOrder.Derivation.length_verum {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {Δ : LO.FirstOrder.Sequent L} : LO.FirstOrder.Derivation.length (LO.FirstOrder.Derivation.verum Δ) = 0

@[simp]

theorem LO.FirstOrder.Derivation.length_and {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {Δ : LO.FirstOrder.Sequent L} {φ ψ : LO.FirstOrder.SyntacticFormula L} (dp : T ⟹ φ :: Δ) (dq : T ⟹ ψ :: Δ) : LO.FirstOrder.Derivation.length (LO.FirstOrder.Derivation.and dp dq) = (LO.FirstOrder.Derivation.length dp ⊔ LO.FirstOrder.Derivation.length dq).succ

@[simp]

theorem LO.FirstOrder.Derivation.length_or {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {Δ : LO.FirstOrder.Sequent L} {φ ψ : LO.FirstOrder.SyntacticFormula L} (d : T ⟹ φ :: ψ :: Δ) : LO.FirstOrder.Derivation.length (LO.FirstOrder.Derivation.or d) = (LO.FirstOrder.Derivation.length d).succ

@[simp]

theorem LO.FirstOrder.Derivation.length_all {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {Δ : LO.FirstOrder.Sequent L} {φ : LO.FirstOrder.SyntacticSemiformula L (0 + 1)} (d : T ⟹ LO.FirstOrder.Rewriting.free φ :: LO.FirstOrder.Rewriting.shifts Δ) : LO.FirstOrder.Derivation.length (LO.FirstOrder.Derivation.all d) = (LO.FirstOrder.Derivation.length d).succ

@[simp]

theorem LO.FirstOrder.Derivation.length_ex {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {Δ : LO.FirstOrder.Sequent L} {t : LO.FirstOrder.Semiterm L ℕ 0} {φ : LO.FirstOrder.SyntacticSemiformula L (Nat.succ 0)} (d : T ⟹ φ/[t] :: Δ) : LO.FirstOrder.Derivation.length (LO.FirstOrder.Derivation.ex t d) = (LO.FirstOrder.Derivation.length d).succ

@[simp]

theorem LO.FirstOrder.Derivation.length_wk {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {Δ Γ : LO.FirstOrder.Sequent L} (d : T ⟹ Δ) (h : Δ ⊆ Γ) : LO.FirstOrder.Derivation.length (LO.FirstOrder.Derivation.wk d h) = (LO.FirstOrder.Derivation.length d).succ

@[simp]

theorem LO.FirstOrder.Derivation.length_cut {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {Δ : LO.FirstOrder.Sequent L} {φ : LO.FirstOrder.SyntacticFormula L} (dp : T ⟹ φ :: Δ) (dn : T ⟹ ∼φ :: Δ) : LO.FirstOrder.Derivation.length (LO.FirstOrder.Derivation.cut dp dn) = (LO.FirstOrder.Derivation.length dp ⊔ LO.FirstOrder.Derivation.length dn).succ

unsafe def LO.FirstOrder.Derivation.repr {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} [(k : ℕ) → ToString (L.Func k)] [(k : ℕ) → ToString (L.Rel k)] {Δ : LO.FirstOrder.Sequent L} : T ⟹ Δ → String

unsafe instance LO.FirstOrder.Derivation.instReprDerivationSyntacticFormulaTheory {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {Δ : LO.FirstOrder.Sequent L} [(k : ℕ) → ToString (L.Func k)] [(k : ℕ) → ToString (L.Rel k)] : Repr (T ⟹ Δ)

@[reducible, inline]

abbrev LO.FirstOrder.Derivation.cast {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {Δ Γ : LO.FirstOrder.Sequent L} (d : T ⟹ Δ) (e : Δ = Γ) : T ⟹ Γ

Equations

• LO.FirstOrder.Derivation.cast d e = e ▸ d

@[simp]

theorem LO.FirstOrder.Derivation.cast_eq {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {Δ : LO.FirstOrder.Sequent L} (d : T ⟹ Δ) (e : Δ = Δ) : LO.FirstOrder.Derivation.cast d e = d

@[simp]

theorem LO.FirstOrder.Derivation.length_cast {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {Δ Γ : LO.FirstOrder.Sequent L} (d : T ⟹ Δ) (e : Δ = Γ) : LO.FirstOrder.Derivation.length (LO.FirstOrder.Derivation.cast d e) = LO.FirstOrder.Derivation.length d

@[simp]

theorem LO.FirstOrder.Derivation.length_cast' {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {Δ Γ : LO.FirstOrder.Sequent L} (d : T ⟹ Δ) (e : Δ = Γ) : LO.FirstOrder.Derivation.length (e ▸ d) = LO.FirstOrder.Derivation.length d

def LO.FirstOrder.Derivation.weakening {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {Γ Δ : LO.FirstOrder.Sequent L} : LO.FirstOrder.Derivation T Δ → Δ ⊆ Γ → LO.FirstOrder.Derivation T Γ

Alias of LO.FirstOrder.Derivation.wk.

Equations

• @LO.FirstOrder.Derivation.weakening = @LO.FirstOrder.Derivation.wk

def LO.FirstOrder.Derivation.verum' {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {Δ : LO.FirstOrder.Sequent L} (h : ⊤ ∈ Δ) : T ⟹ Δ

Equations

• LO.FirstOrder.Derivation.verum' h = (LO.FirstOrder.Derivation.verum Δ).wk ⋯

def LO.FirstOrder.Derivation.axL' {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {Δ : LO.FirstOrder.Sequent L} {k : ℕ} (r : L.Rel k) (v : Fin k → LO.FirstOrder.Semiterm L ℕ 0) (h : LO.FirstOrder.Semiformula.rel r v ∈ Δ) (hn : LO.FirstOrder.Semiformula.nrel r v ∈ Δ) : T ⟹ Δ

Equations

• LO.FirstOrder.Derivation.axL' r v h hn = (LO.FirstOrder.Derivation.axL Δ r v).wk ⋯

def LO.FirstOrder.Derivation.all' {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {Δ : LO.FirstOrder.Sequent L} {φ : LO.FirstOrder.SyntacticSemiformula L (0 + 1)} (h : ∀' φ ∈ Δ) (d : T ⟹ LO.FirstOrder.Rewriting.free φ :: LO.FirstOrder.Rewriting.shifts Δ) : T ⟹ Δ

Equations

• LO.FirstOrder.Derivation.all' h d = (LO.FirstOrder.Derivation.all d).wk ⋯

def LO.FirstOrder.Derivation.ex' {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {Δ : LO.FirstOrder.Sequent L} {φ : LO.FirstOrder.SyntacticSemiformula L (0 + 1)} (h : ∃' φ ∈ Δ) (t : LO.FirstOrder.Semiterm L ℕ 0) (d : T ⟹ φ/[t] :: Δ) : T ⟹ Δ

Equations

• LO.FirstOrder.Derivation.ex' h t d = (LO.FirstOrder.Derivation.ex t d).wk ⋯

@[simp]

theorem LO.FirstOrder.Derivation.ne_step_max (n m : ℕ) : n ≠ n ⊔ m + 1

@[simp]

theorem LO.FirstOrder.Derivation.ne_step_max' (n m : ℕ) : n ≠ m ⊔ n + 1

def LO.FirstOrder.Derivation.em {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {φ : LO.FirstOrder.SyntacticFormula L} {Δ : LO.FirstOrder.Sequent L} (hpos : φ ∈ Δ) (hneg : ∼φ ∈ Δ) : T ⟹ Δ

Equations

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

instance LO.FirstOrder.Derivation.instTaitSyntacticFormulaTheory {L : LO.FirstOrder.Language} : LO.Tait (LO.FirstOrder.SyntacticFormula L) (LO.FirstOrder.Theory L)

Equations

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

instance LO.FirstOrder.Derivation.instCutSyntacticFormulaTheory {L : LO.FirstOrder.Language} : LO.Tait.Cut (LO.FirstOrder.SyntacticFormula L) (LO.FirstOrder.Theory L)

Equations

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

def LO.FirstOrder.Derivation.provableOfDerivable {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {φ : LO.FirstOrder.SyntacticFormula L} (b : T ⟹. φ) : T ⊢ φ

Equations

• LO.FirstOrder.Derivation.provableOfDerivable b = b

def LO.FirstOrder.Derivation.specialize {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {Γ : LO.FirstOrder.Sequent L} {φ : LO.FirstOrder.SyntacticSemiformula L 1} (t : LO.FirstOrder.SyntacticTerm L) : T ⟹ (∀' φ) :: Γ → T ⟹ φ/[t] :: Γ

Equations

• LO.FirstOrder.Derivation.specialize t d = (LO.FirstOrder.Derivation.wk d ⋯).cut (id (LO.FirstOrder.Derivation.ex t (⋯.mpr (LO.Tait.em ⋯ ⋯))))

def LO.FirstOrder.Derivation.specializes {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {k : ℕ} {φ : LO.FirstOrder.SyntacticSemiformula L k} {Γ : LO.FirstOrder.Sequent L} (v : Fin k → LO.FirstOrder.SyntacticTerm L) : T ⟹ (∀* φ) :: Γ → T ⟹ φ ⇜ v :: Γ

Equations

• One or more equations did not get rendered due to their size.
• LO.FirstOrder.Derivation.specializes x_5 x = LO.FirstOrder.Derivation.cast x ⋯

def LO.FirstOrder.Derivation.instances {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {k : ℕ} {φ : LO.FirstOrder.SyntacticSemiformula L k} {Γ : LO.FirstOrder.Sequent L} {v : Fin k → LO.FirstOrder.SyntacticTerm L} : T ⟹ φ ⇜ v :: Γ → T ⟹ (∃* φ) :: Γ

Equations

• LO.FirstOrder.Derivation.instances b = LO.FirstOrder.Derivation.cast b ⋯
• LO.FirstOrder.Derivation.instances b = LO.FirstOrder.Derivation.instances (LO.FirstOrder.Derivation.cast (LO.FirstOrder.Derivation.ex (v 0) (LO.FirstOrder.Derivation.cast b ⋯)) ⋯)

def LO.FirstOrder.Derivation.allClosureFixitr {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {φ : LO.FirstOrder.SyntacticFormula L} (dp : T ⊢ φ) (m : ℕ) : T ⊢ ∀* (LO.FirstOrder.Rewriting.app (LO.FirstOrder.Rew.fixitr 0 m)) φ

Equations

• LO.FirstOrder.Derivation.allClosureFixitr dp 0 = ⋯.mpr dp
• LO.FirstOrder.Derivation.allClosureFixitr dp m.succ = ⋯.mpr (⋯.mpr (LO.FirstOrder.Derivation.allClosureFixitr dp m)).all

def LO.FirstOrder.Derivation.toClose {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {φ : LO.FirstOrder.SyntacticFormula L} (b : T ⊢ φ) : T ⊢ LO.FirstOrder.Semiformula.close φ

Equations

• LO.FirstOrder.Derivation.toClose b = LO.FirstOrder.Derivation.allClosureFixitr b (LO.FirstOrder.Semiformula.fvSup φ)

def LO.FirstOrder.Derivation.toClose! {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {φ : LO.FirstOrder.SyntacticFormula L} (b : T ⊢! φ) : T ⊢! LO.FirstOrder.Semiformula.close φ

Equations

• ⋯ = ⋯

def LO.FirstOrder.Derivation.rewrite₁ {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {φ : LO.FirstOrder.SyntacticFormula L} (b : T ⊢ φ) (f : ℕ → LO.FirstOrder.SyntacticTerm L) : T ⊢ (LO.FirstOrder.Rewriting.app (LO.FirstOrder.Rew.rewrite f)) φ

Equations

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

def LO.FirstOrder.Derivation.rewrite {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {Δ : List (LO.FirstOrder.SyntacticFormula L)} : T ⟹ Δ → (f : ℕ → LO.FirstOrder.SyntacticTerm L) → T ⟹ List.map (fun (φ : LO.FirstOrder.SyntacticSemiformula L 0) => (LO.FirstOrder.Rewriting.app (LO.FirstOrder.Rew.rewrite f)) φ) Δ

def LO.FirstOrder.Derivation.map {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {Δ : LO.FirstOrder.Sequent L} (d : T ⟹ Δ) (f : ℕ → ℕ) : T ⟹ List.map (fun (φ : LO.FirstOrder.SyntacticSemiformula L 0) => (LO.FirstOrder.Rewriting.app (LO.FirstOrder.Rew.rewriteMap f)) φ) Δ

Equations

• LO.FirstOrder.Derivation.map d f = LO.FirstOrder.Derivation.rewrite d fun (x : ℕ) => LO.FirstOrder.Semiterm.fvar (f x)

def LO.FirstOrder.Derivation.shift {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {Δ : LO.FirstOrder.Sequent L} (d : T ⟹ Δ) : T ⟹ LO.FirstOrder.Rewriting.shifts Δ

Equations

• LO.FirstOrder.Derivation.shift d = LO.FirstOrder.Derivation.cast (LO.FirstOrder.Derivation.map d Nat.succ) ⋯

def LO.FirstOrder.Derivation.trans {L : LO.FirstOrder.Language} {T U : LO.FirstOrder.Theory L} (F : U ⊢* T) {Γ : LO.FirstOrder.Sequent L} : T ⟹ Γ → U ⟹ Γ

instance LO.FirstOrder.Derivation.instAxiomatizedSyntacticFormulaTheory {L : LO.FirstOrder.Language} : LO.Tait.Axiomatized (LO.FirstOrder.SyntacticFormula L) (LO.FirstOrder.Theory L)

Equations

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

def LO.FirstOrder.Derivation.invClose {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {φ : LO.FirstOrder.SyntacticFormula L} (b : T ⊢ LO.FirstOrder.Semiformula.close φ) : T ⊢ φ

Equations

• LO.FirstOrder.Derivation.invClose b = (LO.FirstOrder.Derivation.wk b ⋯).cut (LO.FirstOrder.Derivation.not_close' φ)

def LO.FirstOrder.Derivation.invClose! {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {φ : LO.FirstOrder.SyntacticFormula L} (b : T ⊢! LO.FirstOrder.Semiformula.close φ) : T ⊢! φ

Equations

• ⋯ = ⋯

def LO.FirstOrder.Derivation.deduction {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {Γ : LO.FirstOrder.Sequent L} {φ : LO.FirstOrder.SyntacticFormula L} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] (d : insert φ T ⟹ Γ) : T ⟹ ∼LO.FirstOrder.Semiformula.close φ :: Γ

Equations

• LO.FirstOrder.Derivation.deduction d = LO.Tait.ofAxiomSubset ⋯ (LO.FirstOrder.Derivation.deductionAux d)

def LO.FirstOrder.Derivation.provable_iff_inconsistent {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {φ : LO.FirstOrder.SyntacticFormula L} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] : T ⊢! φ ↔ LO.System.Inconsistent (insert (∼LO.FirstOrder.Semiformula.close φ) T)

Equations

• ⋯ = ⋯

def LO.FirstOrder.Derivation.unprovable_iff_consistent {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {φ : LO.FirstOrder.SyntacticFormula L} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] : T ⊬ φ ↔ LO.System.Consistent (insert (∼LO.FirstOrder.Semiformula.close φ) T)

Equations

• ⋯ = ⋯

theorem LO.FirstOrder.Derivation.shifts_image {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} (Φ : L₁.Hom L₂) {Δ : List (LO.FirstOrder.SyntacticFormula L₁)} : LO.FirstOrder.Rewriting.shifts (List.map (⇑(LO.FirstOrder.Semiformula.lMap Φ)) Δ) = List.map (⇑(LO.FirstOrder.Semiformula.lMap Φ)) (LO.FirstOrder.Rewriting.shifts Δ)

def LO.FirstOrder.Derivation.lMap {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {T₁ : LO.FirstOrder.Theory L₁} (Φ : L₁.Hom L₂) {Δ : List (LO.FirstOrder.SyntacticFormula L₁)} : T₁ ⟹ Δ → LO.FirstOrder.Theory.lMap Φ T₁ ⟹ List.map (⇑(LO.FirstOrder.Semiformula.lMap Φ)) Δ

theorem LO.FirstOrder.Derivation.inconsistent_lMap {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {T₁ : LO.FirstOrder.Theory L₁} (Φ : L₁.Hom L₂) : LO.System.Inconsistent T₁ → LO.System.Inconsistent (LO.FirstOrder.Theory.lMap Φ T₁)

def LO.FirstOrder.Derivation.genelalizeByNewver {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {Δ : LO.FirstOrder.Sequent L} {m : ℕ} {φ : LO.FirstOrder.SyntacticSemiformula L 1} (hp : ¬LO.FirstOrder.Semiformula.FVar? φ m) (hΔ : ∀ ψ ∈ Δ, ¬LO.FirstOrder.Semiformula.FVar? ψ m) (d : T ⟹ φ/[LO.FirstOrder.Semiterm.fvar m] :: Δ) : T ⟹ (∀' φ) :: Δ

Equations

• LO.FirstOrder.Derivation.genelalizeByNewver hp hΔ d = LO.FirstOrder.Derivation.all (LO.FirstOrder.Derivation.cast (LO.FirstOrder.Derivation.map d fun (x : ℕ) => if x = m then 0 else x + 1) ⋯)

def LO.FirstOrder.Derivation.exOfInstances {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {Γ : LO.FirstOrder.Sequent L} (v : List (LO.FirstOrder.SyntacticTerm L)) (φ : LO.FirstOrder.SyntacticSemiformula L 1) (h : T ⟹ List.map (fun (x : LO.FirstOrder.Semiterm L ℕ 0) => φ/[x]) v ++ Γ) : T ⟹ (∃' φ) :: Γ

Equations

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

def LO.FirstOrder.Derivation.exOfInstances' {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {Γ : LO.FirstOrder.Sequent L} (v : List (LO.FirstOrder.SyntacticTerm L)) (φ : LO.FirstOrder.SyntacticSemiformula L 1) (h : T ⟹ (∃' φ) :: List.map (fun (x : LO.FirstOrder.Semiterm L ℕ 0) => φ/[x]) v ++ Γ) : T ⟹ (∃' φ) :: Γ

Equations

• LO.FirstOrder.Derivation.exOfInstances' v φ h = LO.FirstOrder.Derivation.wk (LO.FirstOrder.Derivation.exOfInstances v φ (LO.FirstOrder.Derivation.wk h ⋯)) ⋯

instance LO.FirstOrder.Theory.instSubtheorySyntacticFormulaHAdd {L : LO.FirstOrder.Language} {T U : LO.FirstOrder.Theory L} : T ≼ T + U

Equations

• LO.FirstOrder.Theory.instSubtheorySyntacticFormulaHAdd = LO.System.Axiomatized.subtheoryOfSubset ⋯

instance LO.FirstOrder.Theory.instSubtheorySyntacticFormulaHAdd_1 {L : LO.FirstOrder.Language} {T U : LO.FirstOrder.Theory L} : U ≼ T + U

Equations

• LO.FirstOrder.Theory.instSubtheorySyntacticFormulaHAdd_1 = LO.System.Axiomatized.subtheoryOfSubset ⋯

structure LO.FirstOrder.Theory.Alt (L : LO.FirstOrder.Language) : Type u_1

An auxiliary structure to provide systems of provability of sentence.

• thy : LO.FirstOrder.Theory L

def LO.FirstOrder.Theory.alt {L : LO.FirstOrder.Language} (thy : LO.FirstOrder.Theory L) : LO.FirstOrder.Theory.Alt L

Alias of LO.FirstOrder.Theory.Alt.mk.

Equations

• @LO.FirstOrder.Theory.alt = @LO.FirstOrder.Theory.Alt.mk

instance LO.FirstOrder.instSystemSentenceAlt {L : LO.FirstOrder.Language} : LO.System (LO.FirstOrder.Sentence L) (LO.FirstOrder.Theory.Alt L)

Equations

• LO.FirstOrder.instSystemSentenceAlt = { Prf := fun (T : LO.FirstOrder.Theory.Alt L) (σ : LO.FirstOrder.Sentence L) => T.thy ⊢ ↑σ }

@[simp]

theorem LO.FirstOrder.Theory.alt_thy {L : LO.FirstOrder.Language} (T : LO.FirstOrder.Theory L) : T.alt.thy = T

@[reducible, inline]

abbrev LO.FirstOrder.Provable₀ {L : LO.FirstOrder.Language} (T : LO.FirstOrder.Theory L) (σ : LO.FirstOrder.Sentence L) : Prop

Equations

• (T ⊢!. σ) = (T.alt ⊢! σ)

def LO.FirstOrder.«term_⊢!._» : Lean.TrailingParserDescr

Equations

• LO.FirstOrder.«term_⊢!._» = Lean.ParserDescr.trailingNode `LO.FirstOrder.«term_⊢!._» 45 46 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊢!. ") (Lean.ParserDescr.cat `term 46))

@[reducible, inline]

abbrev LO.FirstOrder.Unprovable₀ {L : LO.FirstOrder.Language} (T : LO.FirstOrder.Theory L) (σ : LO.FirstOrder.Sentence L) : Prop

Equations

• (T ⊬. σ) = (T.alt ⊬ σ)

def LO.FirstOrder.«term_⊬._» : Lean.TrailingParserDescr

Equations

• LO.FirstOrder.«term_⊬._» = Lean.ParserDescr.trailingNode `LO.FirstOrder.«term_⊬._» 45 46 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊬. ") (Lean.ParserDescr.cat `term 46))

instance LO.FirstOrder.instClassicalAltSentence {L : LO.FirstOrder.Language} (T : LO.FirstOrder.Theory.Alt L) : LO.System.Classical T

Equations

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

theorem LO.FirstOrder.provable₀_iff {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {σ : LO.FirstOrder.Sentence L} : T ⊢!. σ ↔ T ⊢! ↑σ

theorem LO.FirstOrder.unprovable₀_iff {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {σ : LO.FirstOrder.Sentence L} : T ⊬. σ ↔ T ⊬ ↑σ