@[reducible, inline]

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

Equations

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

def LO.FirstOrder.shifts {L : LO.FirstOrder.Language} {n : ℕ} (Δ : List (LO.FirstOrder.SyntacticSemiformula L n)) : List (LO.FirstOrder.SyntacticSemiformula L n)

Equations

• LO.FirstOrder.shifts Δ = List.map (⇑(LO.FirstOrder.Rew.hom LO.FirstOrder.Rew.shift)) Δ

def LO.FirstOrder.«term_⁺» : Lean.TrailingParserDescr

Equations

• LO.FirstOrder.«term_⁺» = Lean.ParserDescr.trailingNode `LO.FirstOrder.term_⁺ 1024 1024 (Lean.ParserDescr.symbol "⁺")

@[simp]

theorem LO.FirstOrder.mem_shifts_iff {L : LO.FirstOrder.Language} {n : ℕ} {p : LO.FirstOrder.SyntacticSemiformula L n} {Δ : List (LO.FirstOrder.SyntacticSemiformula L n)} : (LO.FirstOrder.Rew.hom LO.FirstOrder.Rew.shift) p ∈ LO.FirstOrder.shifts Δ ↔ p ∈ Δ

@[simp]

theorem LO.FirstOrder.shifts_ss {L : LO.FirstOrder.Language} {n : ℕ} (Δ : List (LO.FirstOrder.SyntacticSemiformula L n)) (Γ : List (LO.FirstOrder.SyntacticSemiformula L n)) : LO.FirstOrder.shifts Δ ⊆ LO.FirstOrder.shifts Γ ↔ Δ ⊆ Γ

@[simp]

theorem LO.FirstOrder.shifts_cons {L : LO.FirstOrder.Language} {n : ℕ} (p : LO.FirstOrder.SyntacticSemiformula L n) (Δ : List (LO.FirstOrder.SyntacticSemiformula L n)) : LO.FirstOrder.shifts (p :: Δ) = (LO.FirstOrder.Rew.hom LO.FirstOrder.Rew.shift) p :: LO.FirstOrder.shifts Δ

@[simp]

theorem LO.FirstOrder.shifts_nil {L : LO.FirstOrder.Language} : LO.FirstOrder.shifts [] = []

theorem LO.FirstOrder.shifts_union {L : LO.FirstOrder.Language} {n : ℕ} (Δ : List (LO.FirstOrder.SyntacticSemiformula L n)) (Γ : List (LO.FirstOrder.SyntacticSemiformula L n)) : LO.FirstOrder.shifts (Δ ++ Γ) = LO.FirstOrder.shifts Δ ++ LO.FirstOrder.shifts Γ

theorem LO.FirstOrder.shifts_neg {L : LO.FirstOrder.Language} {n : ℕ} (Γ : List (LO.FirstOrder.SyntacticSemiformula L n)) : LO.FirstOrder.shifts (List.map (fun (x : LO.FirstOrder.SyntacticSemiformula L n) => ∼x) Γ) = List.map (fun (x : LO.FirstOrder.SyntacticSemiformula L n) => ∼x) (LO.FirstOrder.shifts Γ)

@[simp]

theorem LO.FirstOrder.shifts_emb {L : LO.FirstOrder.Language} {n : ℕ} (Γ : List (LO.FirstOrder.Semisentence L n)) : LO.FirstOrder.shifts (List.map (⇑LO.FirstOrder.Rew.emb.hom) Γ) = List.map (⇑LO.FirstOrder.Rew.emb.hom) Γ

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)} → {p q : LO.FirstOrder.SyntacticFormula L} → LO.FirstOrder.Derivation T (p :: q :: Δ) → LO.FirstOrder.Derivation T (p ⋎ q :: Δ)
• and: {L : LO.FirstOrder.Language} → {T : LO.FirstOrder.Theory L} → {Δ : List (LO.FirstOrder.SyntacticFormula L)} → {p q : LO.FirstOrder.SyntacticFormula L} → LO.FirstOrder.Derivation T (p :: Δ) → LO.FirstOrder.Derivation T (q :: Δ) → LO.FirstOrder.Derivation T (p ⋏ q :: Δ)
• all: {L : LO.FirstOrder.Language} → {T : LO.FirstOrder.Theory L} → {Δ : List (LO.FirstOrder.SyntacticSemiformula L 0)} → {p : LO.FirstOrder.Semiformula L ℕ (0 + 1)} → LO.FirstOrder.Derivation T ((LO.FirstOrder.Rew.hom LO.FirstOrder.Rew.free) p :: LO.FirstOrder.shifts Δ) → LO.FirstOrder.Derivation T ((∀' p) :: Δ)
• ex: {L : LO.FirstOrder.Language} → {T : LO.FirstOrder.Theory L} → {Δ : List (LO.FirstOrder.SyntacticFormula L)} → {p : LO.FirstOrder.Semiformula L ℕ (Nat.succ 0)} → (t : LO.FirstOrder.Semiterm L ℕ 0) → LO.FirstOrder.Derivation T ((LO.FirstOrder.Rew.substs ![t]).hom p :: Δ) → LO.FirstOrder.Derivation T ((∃' p) :: Δ)
• 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)} → {p : LO.FirstOrder.SyntacticFormula L} → LO.FirstOrder.Derivation T (p :: Δ) → LO.FirstOrder.Derivation T (∼p :: Δ) → LO.FirstOrder.Derivation T Δ
• root: {L : LO.FirstOrder.Language} → {T : LO.FirstOrder.Theory L} → {p : LO.FirstOrder.SyntacticFormula L} → p ∈ T → LO.FirstOrder.Derivation T [p]

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) = (max (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) = (max (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} {p : LO.FirstOrder.SyntacticFormula L} {q : LO.FirstOrder.SyntacticFormula L} (dp : T ⟹ p :: Δ) (dq : T ⟹ q :: Δ) : LO.FirstOrder.Derivation.length (LO.FirstOrder.Derivation.and dp dq) = (max (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} {p : LO.FirstOrder.SyntacticFormula L} {q : LO.FirstOrder.SyntacticFormula L} (d : T ⟹ p :: q :: Δ) : 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} {p : LO.FirstOrder.Semiformula L ℕ (0 + 1)} (d : T ⟹ (LO.FirstOrder.Rew.hom LO.FirstOrder.Rew.free) p :: LO.FirstOrder.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} {p : LO.FirstOrder.Semiformula L ℕ (Nat.succ 0)} (d : T ⟹ (LO.FirstOrder.Rew.substs ![t]).hom p :: Δ) : 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} {Γ : 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} {p : LO.FirstOrder.SyntacticFormula L} (dp : T ⟹ p :: Δ) (dn : T ⟹ ∼p :: Δ) : LO.FirstOrder.Derivation.length (LO.FirstOrder.Derivation.cut dp dn) = (max (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

Equations

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

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 ⟹ Δ)

Equations

• LO.FirstOrder.Derivation.instReprDerivationSyntacticFormulaTheory = { reprPrec := fun (d : T ⟹ Δ) (x : ℕ) => Std.Format.text (LO.FirstOrder.Derivation.repr d) }

@[reducible, inline]

abbrev LO.FirstOrder.Derivation.cast {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {Δ : LO.FirstOrder.Sequent 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} {Γ : 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} {Γ : 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.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} {p : LO.FirstOrder.SyntacticSemiformula L (0 + 1)} (h : ∀' p ∈ Δ) (d : T ⟹ (LO.FirstOrder.Rew.hom LO.FirstOrder.Rew.free) p :: LO.FirstOrder.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} {p : LO.FirstOrder.SyntacticSemiformula L (0 + 1)} (h : ∃' p ∈ Δ) (t : LO.FirstOrder.Semiterm L ℕ 0) (d : T ⟹ (LO.FirstOrder.Rew.substs ![t]).hom p :: Δ) : 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 ≠ max n m + 1

@[simp]

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

def LO.FirstOrder.Derivation.em {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {p : LO.FirstOrder.SyntacticFormula L} {Δ : LO.FirstOrder.Sequent L} (hpos : p ∈ Δ) (hneg : ∼p ∈ Δ) : 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} {p : LO.FirstOrder.SyntacticFormula L} (b : T ⟹. p) : T ⊢ p

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} {p : LO.FirstOrder.SyntacticSemiformula L 1} (t : LO.FirstOrder.SyntacticTerm L) : T ⟹ (∀' p) :: Γ → T ⟹ (LO.FirstOrder.Rew.substs ![t]).hom p :: Γ

Equations

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

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

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 : ℕ} {p : LO.FirstOrder.SyntacticSemiformula L k} {Γ : LO.FirstOrder.Sequent L} {v : Fin k → LO.FirstOrder.SyntacticTerm L} : T ⟹ (LO.FirstOrder.Rew.substs v).hom p :: Γ → T ⟹ (∃* p) :: Γ

Equations

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

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

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} {p : LO.FirstOrder.SyntacticFormula L} (b : T ⊢ p) : T ⊢ LO.FirstOrder.Semiformula.close p

Equations

• LO.FirstOrder.Derivation.toClose b = LO.FirstOrder.Derivation.allClosureFixitr b (LO.FirstOrder.Semiformula.upper p)

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

Equations

• ⋯ = ⋯

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

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 (⇑(LO.FirstOrder.Rew.rewrite f).hom) Δ

def LO.FirstOrder.Derivation.map {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {Δ : LO.FirstOrder.Sequent L} (d : T ⟹ Δ) (f : ℕ → ℕ) : T ⟹ List.map (⇑(LO.FirstOrder.Rew.rewriteMap f).hom) Δ

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.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 : LO.FirstOrder.Theory L} {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} {p : LO.FirstOrder.SyntacticFormula L} (b : T ⊢ LO.FirstOrder.Semiformula.close p) : T ⊢ p

Equations

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

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

Equations

• ⋯ = ⋯

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

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} {p : LO.FirstOrder.SyntacticFormula L} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] : T ⊢! p ↔ LO.System.Inconsistent (insert (∼LO.FirstOrder.Semiformula.close p) T)

Equations

• ⋯ = ⋯

def LO.FirstOrder.Derivation.unprovable_iff_consistent {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {p : LO.FirstOrder.SyntacticFormula L} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] : T ⊬ p ↔ LO.System.Consistent (insert (∼LO.FirstOrder.Semiformula.close p) 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.shifts (List.map (⇑(LO.FirstOrder.Semiformula.lMap Φ)) Δ) = List.map (⇑(LO.FirstOrder.Semiformula.lMap Φ)) (LO.FirstOrder.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 : ℕ} {p : LO.FirstOrder.SyntacticSemiformula L 1} (hp : ¬LO.FirstOrder.Semiformula.fvar? p m) (hΔ : ∀ q ∈ Δ, ¬LO.FirstOrder.Semiformula.fvar? q m) (d : T ⟹ (LO.FirstOrder.Rew.substs ![LO.FirstOrder.Semiterm.fvar m]).hom p :: Δ) : T ⟹ (∀' p) :: Δ

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)) (p : LO.FirstOrder.SyntacticSemiformula L 1) (h : T ⟹ List.map (fun (x : LO.FirstOrder.Semiterm L ℕ 0) => (LO.FirstOrder.Rew.substs ![x]).hom p) v ++ Γ) : T ⟹ (∃' p) :: Γ

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)) (p : LO.FirstOrder.SyntacticSemiformula L 1) (h : T ⟹ (∃' p) :: List.map (fun (x : LO.FirstOrder.Semiterm L ℕ 0) => (LO.FirstOrder.Rew.substs ![x]).hom p) v ++ Γ) : T ⟹ (∃' p) :: Γ

Equations

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

instance LO.FirstOrder.Theory.instSubtheorySyntacticFormulaHAdd {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {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 : LO.FirstOrder.Theory L} {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

Instances For

• LO.FirstOrder.instSystemSentenceAlt

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

Instances For

• LO.FirstOrder.Theory.Alt.instSubtheorySentenceAltOfSyntacticFormula_incompleteness

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

• LO.FirstOrder.instClassicalAltSentence T = LO.System.Classical.ofEquiv T.thy T LO.FirstOrder.Rew.emb.hom fun (x : LO.FirstOrder.Sentence L) => Equiv.refl (T.thy ⊢ LO.FirstOrder.Rew.emb.hom x)

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 ⊬ ↑σ