@[reducible, inline]

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

Equations

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

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

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

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

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

abbrev LO.FirstOrder.Derivable₀ {L : Language} (Γ : 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 : Language} {T : Theory L} {Δ : 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 : Language} {T : Theory L} {Δ : Sequent L} {k : ℕ} {r : L.Rel k} {v : Fin k → Semiterm L ℕ 0} : length (axL Δ r v) = 0

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• One or more equations did not get rendered due to their size.
• LO.FirstOrder.Derivation.repr (LO.FirstOrder.Derivation.axL Γ r v) = "\AxiomC{}\n" ++ "\RightLabel{\scriptsize(axL)}\n" ++ "\UnaryInfC{$" ++ reprStr Γ ++ "$}\n\n"
• LO.FirstOrder.Derivation.repr (LO.FirstOrder.Derivation.verum Γ) = "\AxiomC{}\n" ++ "\RightLabel{\scriptsize($top$)}\n" ++ "\UnaryInfC{$" ++ reprStr Γ ++ "$}\n\n"
• LO.FirstOrder.Derivation.repr d.or = LO.FirstOrder.Derivation.repr d ++ "\RightLabel{\scriptsize($lor$)}\n" ++ "\UnaryInfC{$" ++ reprStr (φ ⋎ ψ :: Γ) ++ "$}\n\n"
• LO.FirstOrder.Derivation.repr d.all = LO.FirstOrder.Derivation.repr d ++ "\RightLabel{\scriptsize($forall$)}\n" ++ "\UnaryInfC{$" ++ reprStr ((∀' φ) :: Γ) ++ "$}\n\n"
• LO.FirstOrder.Derivation.repr (d.wk a) = LO.FirstOrder.Derivation.repr d ++ "\RightLabel{\scriptsize(wk)}\n" ++ "\UnaryInfC{$" ++ reprStr Δ_3 ++ "$}\n\n"
• LO.FirstOrder.Derivation.repr (LO.FirstOrder.Derivation.root a) = "\AxiomC{}\n" ++ "\RightLabel{\scriptsize(ROOT)}\n" ++ "\UnaryInfC{$" ++ reprStr φ ++ ", " ++ reprStr (∼φ) ++ "$}\n\n"

unsafe instance LO.FirstOrder.Derivation.instReprDerivationSyntacticFormulaTheory {L : Language} {T : Theory L} {Δ : 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 : Language} {T : Theory L} {Δ Γ : Sequent L} (d : T ⟹ Δ) (e : Δ = Γ) : T ⟹ Γ

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Alias of LO.FirstOrder.Derivation.wk.

Equations

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

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

Equations

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

def LO.FirstOrder.Derivation.axL' {L : Language} {T : Theory L} {Δ : Sequent L} {k : ℕ} (r : L.Rel k) (v : Fin k → Semiterm L ℕ 0) (h : Semiformula.rel r v ∈ Δ) (hn : 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 : Language} {T : Theory L} {Δ : Sequent L} {φ : SyntacticSemiformula L (0 + 1)} (h : ∀' φ ∈ Δ) (d : T ⟹ Rewriting.free φ :: Rewriting.shifts Δ) : T ⟹ Δ

Equations

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

def LO.FirstOrder.Derivation.ex' {L : Language} {T : Theory L} {Δ : Sequent L} {φ : SyntacticSemiformula L (0 + 1)} (h : ∃' φ ∈ Δ) (t : 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

@[irreducible]

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

Equations

• One or more equations did not get rendered due to their size.
• LO.FirstOrder.Derivation.em hpos hneg = LO.FirstOrder.Derivation.verum' hpos
• LO.FirstOrder.Derivation.em hpos hneg = LO.FirstOrder.Derivation.verum' hneg
• LO.FirstOrder.Derivation.em hpos hneg = LO.FirstOrder.Derivation.axL' R v hpos hneg
• LO.FirstOrder.Derivation.em hpos hneg = LO.FirstOrder.Derivation.axL' R v hneg hpos
• LO.FirstOrder.Derivation.em hpos hneg = ((LO.FirstOrder.Derivation.and (LO.FirstOrder.Derivation.em ⋯ ⋯) (LO.FirstOrder.Derivation.em ⋯ ⋯)).wk ⋯).or.wk ⋯
• LO.FirstOrder.Derivation.em hpos hneg = ((LO.FirstOrder.Derivation.and (LO.FirstOrder.Derivation.em ⋯ ⋯) (LO.FirstOrder.Derivation.em ⋯ ⋯)).wk ⋯).or.wk ⋯

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

Equations

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

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

Equations

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

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

Equations

• LO.FirstOrder.Derivation.provableOfDerivable b = b

def LO.FirstOrder.Derivation.specialize {L : Language} {T : Theory L} {Γ : Sequent L} {φ : SyntacticSemiformula L 1} (t : 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 : Language} {T : Theory L} {k : ℕ} {φ : SyntacticSemiformula L k} {Γ : Sequent L} (v : Fin k → 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 : Language} {T : Theory L} {k : ℕ} {φ : SyntacticSemiformula L k} {Γ : Sequent L} {v : Fin k → 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 : Language} {T : Theory L} {φ : SyntacticFormula L} (dp : T ⊢ φ) (m : ℕ) : T ⊢ ∀* (Rewriting.app (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 : Language} {T : Theory L} {φ : SyntacticFormula L} (b : T ⊢ φ) : T ⊢ Semiformula.close φ

Equations

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

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

Equations

• ⋯ = ⋯

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

Equations

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

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

def LO.FirstOrder.Derivation.map {L : Language} {T : Theory L} {Δ : Sequent L} (d : T ⟹ Δ) (f : ℕ → ℕ) : T ⟹ List.map (fun (φ : SyntacticSemiformula L 0) => (Rewriting.app (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 : Language} {T : Theory L} {Δ : Sequent L} (d : T ⟹ Δ) : T ⟹ 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 : Language} {T U : Theory L} (F : U ⊢* T) {Γ : Sequent L} : T ⟹ Γ → U ⟹ Γ

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

Equations

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

def LO.FirstOrder.Derivation.invClose {L : Language} {T : Theory L} {φ : SyntacticFormula L} (b : T ⊢ 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 : Language} {T : Theory L} {φ : SyntacticFormula L} (b : T ⊢! Semiformula.close φ) : T ⊢! φ

Equations

• ⋯ = ⋯

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

Equations

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

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

Equations

• One or more equations did not get rendered due to their size.
• LO.FirstOrder.Derivation.lMap Φ (LO.FirstOrder.Derivation.verum Δ_2) = ⋯.mpr (LO.FirstOrder.Derivation.verum (List.map (⇑(LO.FirstOrder.Semiformula.lMap Φ)) Δ_2))
• LO.FirstOrder.Derivation.lMap Φ d.or = LO.FirstOrder.Derivation.cast (LO.FirstOrder.Derivation.or (LO.FirstOrder.Derivation.lMap Φ d)) ⋯
• LO.FirstOrder.Derivation.lMap Φ d.all = LO.FirstOrder.Derivation.cast (LO.FirstOrder.Derivation.all (LO.FirstOrder.Derivation.cast (LO.FirstOrder.Derivation.lMap Φ d) ⋯)) ⋯
• LO.FirstOrder.Derivation.lMap Φ (d.wk ss) = LO.FirstOrder.Derivation.wk (LO.FirstOrder.Derivation.lMap Φ d) ⋯
• LO.FirstOrder.Derivation.lMap Φ (LO.FirstOrder.Derivation.root h) = LO.FirstOrder.Derivation.root ⋯

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

def LO.FirstOrder.Derivation.genelalizeByNewver {L : Language} {T : Theory L} {Δ : Sequent L} {m : ℕ} {φ : SyntacticSemiformula L 1} (hp : ¬Semiformula.FVar? φ m) (hΔ : ∀ ψ ∈ Δ, ¬Semiformula.FVar? ψ m) (d : T ⟹ φ/[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 : Language} {T : Theory L} {Γ : Sequent L} (v : List (SyntacticTerm L)) (φ : SyntacticSemiformula L 1) (h : T ⟹ List.map (fun (x : 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 : Language} {T : Theory L} {Γ : Sequent L} (v : List (SyntacticTerm L)) (φ : SyntacticSemiformula L 1) (h : T ⟹ (∃' φ) :: List.map (fun (x : 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 ⋯)) ⋯

def LO.FirstOrder.newVar {L : Language} (Γ : Sequent L) : ℕ

Equations

• LO.FirstOrder.newVar Γ = List.foldr max 0 (List.map LO.FirstOrder.Semiformula.fvSup Γ)

theorem LO.FirstOrder.not_fvar?_newVar {L : Language} {φ : SyntacticFormula L} {Γ : Sequent L} (h : φ ∈ Γ) : ¬Semiformula.FVar? φ (newVar Γ)

def LO.FirstOrder.Derivation.allNvar {L : Language} {T : Theory L} {Δ : Sequent L} {φ : SyntacticSemiformula L (0 + 1)} (h : ∀' φ ∈ Δ) : T ⟹ φ/[Semiterm.fvar (newVar Δ)] :: Δ → T ⟹ Δ

Equations

• LO.FirstOrder.Derivation.allNvar h b = LO.Tait.wk (LO.FirstOrder.Derivation.genelalizeByNewver ⋯ ⋯ b) ⋯

def LO.FirstOrder.Derivation.id {L : Language} {T : Theory L} {Δ : Sequent L} {φ : SyntacticFormula L} (hp : φ ∈ T) : T ⟹ ∼Semiformula.close φ :: Δ → T ⟹ Δ

Equations

• LO.FirstOrder.Derivation.id hp b = LO.Tait.cut (LO.Tait.wk (LO.FirstOrder.Derivation.toClose (LO.FirstOrder.Derivation.root hp)) ⋯) b

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

Equations

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

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

Equations

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

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

An auxiliary structure to provide systems of provability of sentence.

• thy : Theory L

Instances For

• LO.FirstOrder.instSystemSentenceAlt

def LO.FirstOrder.Theory.alt {L : Language} (thy : Theory L) : 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 : Language} : System (Sentence L) (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 : Language} (T : Theory L) : T.alt.thy = T

@[reducible, inline]

abbrev LO.FirstOrder.Provable₀ {L : Language} (T : Theory L) (σ : 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 : Language} (T : Theory L) (σ : 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 : Language} (T : Theory.Alt L) : System.Classical T

Equations

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

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

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