@[reducible, inline]
Equations
Instances For
- 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 [φ]
Instances For
instance
LO.FirstOrder.instOneSidedSyntacticFormulaTheory
{L : Language}
:
OneSided (SyntacticFormula L) (Theory L)
Equations
- LO.FirstOrder.instOneSidedSyntacticFormulaTheory = { Derivation := LO.FirstOrder.Derivation }
Equations
- LO.FirstOrder.«term⊢ᵀ_» = Lean.ParserDescr.node `LO.FirstOrder.«term⊢ᵀ_» 45 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⊢ᵀ ") (Lean.ParserDescr.cat `term 45))
Instances For
Equations
- LO.FirstOrder.«term⊢ᵀ!_» = Lean.ParserDescr.node `LO.FirstOrder.«term⊢ᵀ!_» 45 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⊢ᵀ! ") (Lean.ParserDescr.cat `term 45))
Instances For
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
Instances For
@[simp]
theorem
LO.FirstOrder.Derivation.length_all
{L : Language}
{T : Theory L}
{Δ : Sequent L}
{φ : SyntacticSemiformula L (0 + 1)}
(d : T ⟹ Rewriting.free φ :: Rewriting.shifts Δ)
:
unsafe def
LO.FirstOrder.Derivation.repr
{L : Language}
{T : Theory L}
[(k : ℕ) → ToString (L.Func k)]
[(k : ℕ) → ToString (L.Rel k)]
{Δ : Sequent L}
:
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(
)}\n" ++ "\UnaryInfC{$" ++ reprStr Γ ++ "$}\n\n" - LO.FirstOrder.Derivation.repr d.or = LO.FirstOrder.Derivation.repr d ++ "\RightLabel{\scriptsize(
)}\n" ++ "\UnaryInfC{$" ++ reprStr (φ ⋎ ψ :: Γ) ++ "$}\n\n" - LO.FirstOrder.Derivation.repr d.all = LO.FirstOrder.Derivation.repr d ++ "\RightLabel{\scriptsize(
)}\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"
Instances For
unsafe instance
LO.FirstOrder.Derivation.instReprDerivationSyntacticFormulaTheory
{L : Language}
{T : Theory L}
{Δ : Sequent L}
[(k : ℕ) → ToString (L.Func k)]
[(k : ℕ) → ToString (L.Rel k)]
:
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
Instances For
@[simp]
theorem
LO.FirstOrder.Derivation.cast_eq
{L : Language}
{T : Theory L}
{Δ : Sequent L}
(d : T ⟹ Δ)
(e : Δ = Δ)
:
Derivation.cast d e = d
def
LO.FirstOrder.Derivation.weakening
{L : Language}
{T : Theory L}
{Γ Δ : Sequent L}
:
Derivation T Δ → Δ ⊆ Γ → Derivation T Γ
Alias of LO.FirstOrder.Derivation.wk
.
Instances For
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 ⋯
Instances For
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 ⋯
Instances For
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 ⋯
Instances For
@[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 ⋯
Instances For
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
Instances For
def
LO.FirstOrder.Derivation.specialize
{L : Language}
{T : Theory L}
{Γ : Sequent L}
{φ : SyntacticSemiformula L 1}
(t : SyntacticTerm L)
:
Equations
- LO.FirstOrder.Derivation.specialize t d = (LO.FirstOrder.Derivation.wk d ⋯).cut (id (LO.FirstOrder.Derivation.ex t (⋯.mpr (LO.Tait.em ⋯ ⋯))))
Instances For
def
LO.FirstOrder.Derivation.specializes
{L : Language}
{T : Theory L}
{k : ℕ}
{φ : SyntacticSemiformula L k}
{Γ : Sequent L}
(v : Fin k → SyntacticTerm L)
:
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✝ ⋯
Instances For
def
LO.FirstOrder.Derivation.instances
{L : Language}
{T : Theory L}
{k : ℕ}
{φ : SyntacticSemiformula L k}
{Γ : Sequent L}
{v : Fin k → SyntacticTerm L}
:
Equations
Instances For
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
Instances For
def
LO.FirstOrder.Derivation.toClose
{L : Language}
{T : Theory L}
{φ : SyntacticFormula L}
(b : T ⊢ φ)
:
T ⊢ Semiformula.close φ
Equations
Instances For
def
LO.FirstOrder.Derivation.toClose!
{L : Language}
{T : Theory L}
{φ : SyntacticFormula L}
(b : T ⊢! φ)
:
T ⊢! Semiformula.close φ
Equations
- ⋯ = ⋯
Instances For
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.
Instances For
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)) φ) Δ
Instances For
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)
Instances For
def
LO.FirstOrder.Derivation.shift
{L : Language}
{T : Theory L}
{Δ : Sequent L}
(d : T ⟹ Δ)
:
T ⟹ Rewriting.shifts Δ
Equations
Instances For
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
Instances For
def
LO.FirstOrder.Derivation.invClose!
{L : Language}
{T : Theory L}
{φ : SyntacticFormula L}
(b : T ⊢! Semiformula.close φ)
:
T ⊢! φ
Equations
- ⋯ = ⋯
Instances For
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
Instances For
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
- ⋯ = ⋯
Instances For
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
- ⋯ = ⋯
Instances For
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 ⋯
Instances For
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] :: Δ)
:
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) ⋯)
Instances For
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 ++ Γ)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
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 ++ Γ)
:
Equations
Instances For
Equations
Instances For
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
Instances For
def
LO.FirstOrder.Derivation.id
{L : Language}
{T : Theory L}
{Δ : Sequent L}
{φ : SyntacticFormula L}
(hp : φ ∈ T)
:
T ⟹ ∼Semiformula.close φ :: Δ → T ⟹ Δ
Equations
Instances For
Alias of LO.FirstOrder.Theory.Alt.mk
.
Instances For
Equations
- LO.FirstOrder.instSystemSentenceAlt = { Prf := fun (T : LO.FirstOrder.Theory.Alt L) (σ : LO.FirstOrder.Sentence L) => T.thy ⊢ ↑σ }
Equations
- LO.FirstOrder.«term_⊢!._» = Lean.ParserDescr.trailingNode `LO.FirstOrder.«term_⊢!._» 45 46 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊢!. ") (Lean.ParserDescr.cat `term 46))
Instances For
Equations
- LO.FirstOrder.«term_⊬._» = Lean.ParserDescr.trailingNode `LO.FirstOrder.«term_⊬._» 45 46 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊬. ") (Lean.ParserDescr.cat `term 46))
Instances For
Equations
- One or more equations did not get rendered due to their size.