@[reducible, inline]
Equations
Instances For
def
LO.FirstOrder.shifts
{L : LO.FirstOrder.Language}
{n : ℕ}
(Δ : List (LO.FirstOrder.SyntacticSemiformula L n))
:
Equations
- LO.FirstOrder.shifts Δ = List.map (⇑(LO.FirstOrder.Rew.hom LO.FirstOrder.Rew.shift)) Δ
Instances For
Equations
- LO.FirstOrder.«term_⁺» = Lean.ParserDescr.trailingNode `LO.FirstOrder.term_⁺ 1024 1024 (Lean.ParserDescr.symbol "⁺")
Instances For
@[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_union
{L : LO.FirstOrder.Language}
{n : ℕ}
(Δ : List (LO.FirstOrder.SyntacticSemiformula L n))
(Γ : List (LO.FirstOrder.SyntacticSemiformula L n))
:
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]
Instances For
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
Instances For
@[reducible, inline]
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.«term⊢ᵀ!_» = Lean.ParserDescr.node `LO.FirstOrder.term⊢ᵀ!_ 45 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⊢ᵀ! ") (Lean.ParserDescr.cat `term 45))
Instances For
def
LO.FirstOrder.Derivation.length
{L : LO.FirstOrder.Language}
{T : LO.FirstOrder.Theory L}
{Δ : LO.FirstOrder.Sequent L}
:
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
Instances For
@[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}
:
@[simp]
theorem
LO.FirstOrder.Derivation.length_verum
{L : LO.FirstOrder.Language}
{T : LO.FirstOrder.Theory L}
{Δ : LO.FirstOrder.Sequent L}
:
@[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 :: Δ)
:
@[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 :: Δ)
:
@[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 Δ)
:
@[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 :: Δ)
:
@[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 : Δ ⊆ Γ)
:
@[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 :: Δ)
:
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}
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
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)]
:
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
Instances For
@[simp]
theorem
LO.FirstOrder.Derivation.cast_eq
{L : LO.FirstOrder.Language}
{T : LO.FirstOrder.Theory L}
{Δ : LO.FirstOrder.Sequent L}
(d : T ⟹ Δ)
(e : Δ = Δ)
:
@[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 : Δ = Γ)
:
@[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 : Δ = Γ)
:
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
.
Instances For
def
LO.FirstOrder.Derivation.verum'
{L : LO.FirstOrder.Language}
{T : LO.FirstOrder.Theory L}
{Δ : LO.FirstOrder.Sequent L}
(h : ⊤ ∈ Δ)
:
T ⟹ Δ
Equations
Instances For
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 ⋯
Instances For
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 ⋯
Instances For
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 ⋯
Instances For
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.
Instances For
Equations
- One or more equations did not get rendered due to their size.
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
Instances For
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)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
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)
:
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 : 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}
:
Equations
- One or more equations did not get rendered due to their size.
- LO.FirstOrder.Derivation.instances b = LO.FirstOrder.Derivation.cast b ⋯
Instances For
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
Instances For
def
LO.FirstOrder.Derivation.toClose
{L : LO.FirstOrder.Language}
{T : LO.FirstOrder.Theory L}
{p : LO.FirstOrder.SyntacticFormula L}
(b : T ⊢ p)
:
Equations
Instances For
def
LO.FirstOrder.Derivation.toClose!
{L : LO.FirstOrder.Language}
{T : LO.FirstOrder.Theory L}
{p : LO.FirstOrder.SyntacticFormula L}
(b : T ⊢! p)
:
Equations
- ⋯ = ⋯
Instances For
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.
Instances For
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) Δ
Instances For
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)
Instances For
def
LO.FirstOrder.Derivation.shift
{L : LO.FirstOrder.Language}
{T : LO.FirstOrder.Theory L}
{Δ : LO.FirstOrder.Sequent L}
(d : T ⟹ Δ)
:
Equations
Instances For
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}
:
Instances For
instance
LO.FirstOrder.Derivation.instAxiomatizedSyntacticFormulaTheory
{L : LO.FirstOrder.Language}
:
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
Instances For
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
- ⋯ = ⋯
Instances For
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 ⟹ Γ)
:
Equations
Instances For
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
- ⋯ = ⋯
Instances For
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
- ⋯ = ⋯
Instances For
theorem
LO.FirstOrder.Derivation.shifts_image
{L₁ : LO.FirstOrder.Language}
{L₂ : LO.FirstOrder.Language}
(Φ : L₁.Hom L₂)
{Δ : List (LO.FirstOrder.SyntacticFormula L₁)}
:
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 Φ)) Δ
Instances For
theorem
LO.FirstOrder.Derivation.inconsistent_lMap
{L₁ : LO.FirstOrder.Language}
{L₂ : LO.FirstOrder.Language}
{T₁ : LO.FirstOrder.Theory L₁}
(Φ : L₁.Hom L₂)
:
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 :: Δ)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
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 ++ Γ)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
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 ++ Γ)
:
Equations
Instances For
instance
LO.FirstOrder.Theory.instSubtheorySyntacticFormulaHAdd
{L : LO.FirstOrder.Language}
{T : LO.FirstOrder.Theory L}
{U : LO.FirstOrder.Theory L}
:
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}
:
Equations
- LO.FirstOrder.Theory.instSubtheorySyntacticFormulaHAdd_1 = LO.System.Axiomatized.subtheoryOfSubset ⋯
An auxiliary structure to provide systems of provability of sentence.
- thy : LO.FirstOrder.Theory L
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 ⊢ ↑σ }
@[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)
:
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
@[reducible, inline]
abbrev
LO.FirstOrder.Unprovable₀
{L : LO.FirstOrder.Language}
(T : LO.FirstOrder.Theory L)
(σ : LO.FirstOrder.Sentence L)
:
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
instance
LO.FirstOrder.instClassicalAltSentence
{L : LO.FirstOrder.Language}
(T : LO.FirstOrder.Theory.Alt L)
:
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}
:
theorem
LO.FirstOrder.unprovable₀_iff
{L : LO.FirstOrder.Language}
{T : LO.FirstOrder.Theory L}
{σ : LO.FirstOrder.Sentence L}
: