def
LO.FirstOrder.Semiformula.isVType
{L : LO.FirstOrder.Language}
{μ : Type u_1}
{n : ℕ}
:
LO.FirstOrder.Semiformula L μ n → Bool
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.FirstOrder.Semiformula.ne_and_of_isVType
{L : LO.FirstOrder.Language}
{μ : Type u_1}
{n : ℕ}
{p : LO.FirstOrder.Semiformula L μ n}
{q : LO.FirstOrder.Semiformula L μ n}
{r : LO.FirstOrder.Semiformula L μ n}
(h : p.isVType = true)
:
theorem
LO.FirstOrder.Semiformula.ne_all_of_isVType
{L : LO.FirstOrder.Language}
{μ : Type u_1}
{n : ℕ}
{p : LO.FirstOrder.Semiformula L μ n}
{q : LO.FirstOrder.Semiformula L μ (n + 1)}
(h : p.isVType = true)
:
@[simp]
theorem
LO.FirstOrder.Semiformula.isVType_shift_iff
{L : LO.FirstOrder.Language}
{n : ℕ}
{p : LO.FirstOrder.SyntacticSemiformula L n}
:
((LO.FirstOrder.Rew.hom LO.FirstOrder.Rew.shift) p).isVType = LO.FirstOrder.Semiformula.isVType p
theorem
LO.FirstOrder.Semiformula.isVType_neg_true_of_eq_false
{L : LO.FirstOrder.Language}
{n : ℕ}
{p : LO.FirstOrder.SyntacticSemiformula L n}
:
@[reducible, inline]
abbrev
LO.FirstOrder.Derivation.Restricted
{L : LO.FirstOrder.Language}
(C : Set (LO.FirstOrder.SyntacticFormula L))
(Δ : LO.FirstOrder.Sequent L)
:
Type u
Equations
- LO.FirstOrder.Derivation.Restricted C Δ = { d : ⊢¹ Δ // LO.FirstOrder.Derivation.CutRestricted C d }
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
abbrev
LO.FirstOrder.Derivation.RestrictedComplexity
{L : LO.FirstOrder.Language}
(c : ℕ)
(Δ : LO.FirstOrder.Sequent L)
:
Type u
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
LO.FirstOrder.Derivation.Restricted.cutRestricted
{L : LO.FirstOrder.Language}
{C : Set (LO.FirstOrder.SyntacticFormula L)}
{Δ : LO.FirstOrder.Sequent L}
(d : LO.FirstOrder.Derivation.Restricted C Δ)
:
def
LO.FirstOrder.Derivation.Restricted.axL'
{L : LO.FirstOrder.Language}
{C : Set (LO.FirstOrder.SyntacticFormula L)}
{Δ : LO.FirstOrder.Sequent L}
{k : ℕ}
(r : L.Rel k)
(v : Fin k → LO.FirstOrder.Semiterm L ℕ 0)
(hp : LO.FirstOrder.Semiformula.rel r v ∈ Δ)
(hn : LO.FirstOrder.Semiformula.nrel r v ∈ Δ)
:
Equations
- LO.FirstOrder.Derivation.Restricted.axL' r v hp hn = ⟨LO.FirstOrder.Derivation.axL' r v hp hn, ⋯⟩
Instances For
def
LO.FirstOrder.Derivation.Restricted.verum'
{L : LO.FirstOrder.Language}
{C : Set (LO.FirstOrder.SyntacticFormula L)}
{Δ : LO.FirstOrder.Sequent L}
(h : ⊤ ∈ Δ)
:
Equations
Instances For
def
LO.FirstOrder.Derivation.Restricted.and
{L : LO.FirstOrder.Language}
{C : Set (LO.FirstOrder.SyntacticFormula L)}
{Δ : LO.FirstOrder.Sequent L}
{p : LO.FirstOrder.SyntacticFormula L}
{q : LO.FirstOrder.SyntacticFormula L}
(dp : LO.FirstOrder.Derivation.Restricted C (p :: Δ))
(dq : LO.FirstOrder.Derivation.Restricted C (q :: Δ))
:
LO.FirstOrder.Derivation.Restricted C (p ⋏ q :: Δ)
Equations
- dp.and dq = ⟨LO.FirstOrder.Derivation.and ↑dp ↑dq, ⋯⟩
Instances For
def
LO.FirstOrder.Derivation.Restricted.or
{L : LO.FirstOrder.Language}
{C : Set (LO.FirstOrder.SyntacticFormula L)}
{Δ : LO.FirstOrder.Sequent L}
{p : LO.FirstOrder.SyntacticFormula L}
{q : LO.FirstOrder.SyntacticFormula L}
(d : LO.FirstOrder.Derivation.Restricted C (p :: q :: Δ))
:
LO.FirstOrder.Derivation.Restricted C (p ⋎ q :: Δ)
Equations
- d.or = ⟨LO.FirstOrder.Derivation.or ↑d, ⋯⟩
Instances For
def
LO.FirstOrder.Derivation.Restricted.all
{L : LO.FirstOrder.Language}
{C : Set (LO.FirstOrder.SyntacticFormula L)}
{Δ : LO.FirstOrder.Sequent L}
{p : LO.FirstOrder.Semiformula L ℕ (0 + 1)}
(d : LO.FirstOrder.Derivation.Restricted C ((LO.FirstOrder.Rew.hom LO.FirstOrder.Rew.free) p :: LO.FirstOrder.shifts Δ))
:
LO.FirstOrder.Derivation.Restricted C ((∀' p) :: Δ)
Equations
- d.all = ⟨LO.FirstOrder.Derivation.all ↑d, ⋯⟩
Instances For
def
LO.FirstOrder.Derivation.Restricted.ex
{L : LO.FirstOrder.Language}
{C : Set (LO.FirstOrder.SyntacticFormula L)}
{Δ : LO.FirstOrder.Sequent L}
{p : LO.FirstOrder.Semiformula L ℕ (Nat.succ 0)}
(t : LO.FirstOrder.Semiterm L ℕ 0)
(d : LO.FirstOrder.Derivation.Restricted C ((LO.FirstOrder.Rew.substs ![t]).hom p :: Δ))
:
LO.FirstOrder.Derivation.Restricted C ((∃' p) :: Δ)
Equations
Instances For
def
LO.FirstOrder.Derivation.Restricted.wk
{L : LO.FirstOrder.Language}
{C : Set (LO.FirstOrder.SyntacticFormula L)}
{Δ : LO.FirstOrder.Sequent L}
{Γ : LO.FirstOrder.Sequent L}
(d : LO.FirstOrder.Derivation.Restricted C Γ)
(h : Γ ⊆ Δ)
:
Equations
- d.wk h = ⟨LO.FirstOrder.Derivation.wk (↑d) h, ⋯⟩
Instances For
def
LO.FirstOrder.Derivation.Restricted.cut
{L : LO.FirstOrder.Language}
{C : Set (LO.FirstOrder.SyntacticFormula L)}
{Δ : LO.FirstOrder.Sequent L}
{p : LO.FirstOrder.SyntacticFormula L}
(dp : LO.FirstOrder.Derivation.Restricted C (p :: Δ))
(dn : LO.FirstOrder.Derivation.Restricted C (~p :: Δ))
(h : p ∈ C)
:
Equations
- dp.cut dn h = ⟨LO.FirstOrder.Derivation.cut ↑dp ↑dn, ⋯⟩
Instances For
def
LO.FirstOrder.Derivation.Restricted.rewrite
{L : LO.FirstOrder.Language}
{C : Set (LO.FirstOrder.SyntacticFormula L)}
(hC : ∀ (f : ℕ → LO.FirstOrder.Semiterm L ℕ 0), ∀ p ∈ C, (LO.FirstOrder.Rew.rewrite f).hom p ∈ C)
{Δ : LO.FirstOrder.Sequent L}
(f : ℕ → LO.FirstOrder.SyntacticTerm L)
(d : LO.FirstOrder.Derivation.Restricted C Δ)
:
LO.FirstOrder.Derivation.Restricted C (List.map (⇑(LO.FirstOrder.Rew.rewrite f).hom) Δ)
Equations
- LO.FirstOrder.Derivation.Restricted.rewrite hC f d = ⟨LO.FirstOrder.Derivation.rewrite (↑d) f, ⋯⟩
Instances For
def
LO.FirstOrder.Derivation.Restricted.shifts
{L : LO.FirstOrder.Language}
{C : Set (LO.FirstOrder.SyntacticFormula L)}
(hC : ∀ (f : ℕ → LO.FirstOrder.Semiterm L ℕ 0), ∀ p ∈ C, (LO.FirstOrder.Rew.rewrite f).hom p ∈ C)
{Δ : LO.FirstOrder.Sequent L}
(d : LO.FirstOrder.Derivation.Restricted C Δ)
:
Equations
- LO.FirstOrder.Derivation.Restricted.shifts hC d = LO.FirstOrder.Derivation.Restricted.rewrite hC (fun (m : ℕ) => LO.FirstOrder.Semiterm.fvar m.succ) d
Instances For
@[reducible, inline]
abbrev
LO.FirstOrder.Derivation.Restricted.cast
{L : LO.FirstOrder.Language}
{C : Set (LO.FirstOrder.SyntacticFormula L)}
{Δ : LO.FirstOrder.Sequent L}
{Γ : LO.FirstOrder.Sequent L}
(d : LO.FirstOrder.Derivation.Restricted C Γ)
(e : Γ = Δ)
:
Equations
- d.cast e = ⟨LO.FirstOrder.Derivation.cast (↑d) e, ⋯⟩
Instances For
@[simp]
theorem
LO.FirstOrder.Derivation.Restricted.length_rewrite
{L : LO.FirstOrder.Language}
{C : Set (LO.FirstOrder.SyntacticFormula L)}
(hC : ∀ (f : ℕ → LO.FirstOrder.Semiterm L ℕ 0), ∀ p ∈ C, (LO.FirstOrder.Rew.rewrite f).hom p ∈ C)
{Δ : LO.FirstOrder.Sequent L}
(f : ℕ → LO.FirstOrder.SyntacticTerm L)
(d : LO.FirstOrder.Derivation.Restricted C Δ)
:
def
LO.FirstOrder.Derivation.Restricted.ofSubset
{L : LO.FirstOrder.Language}
{C : Set (LO.FirstOrder.SyntacticFormula L)}
{C' : Set (LO.FirstOrder.SyntacticFormula L)}
{Δ : LO.FirstOrder.Sequent L}
(h : C ⊆ C')
(d : LO.FirstOrder.Derivation.Restricted C Δ)
:
Equations
- LO.FirstOrder.Derivation.Restricted.ofSubset h d = ⟨↑d, ⋯⟩
Instances For
def
LO.FirstOrder.Derivation.RestrictedComplexity.ofLe
{L : LO.FirstOrder.Language}
{Δ : LO.FirstOrder.Sequent L}
{i : ℕ}
{j : ℕ}
(hij : i ≤ j)
(d : LO.FirstOrder.Derivation.RestrictedComplexity i Δ)
:
Equations
Instances For
@[irreducible]
def
LO.FirstOrder.Derivation.andInversion₁Aux
{L : LO.FirstOrder.Language}
[(k : ℕ) → DecidableEq (L.Func k)]
[(k : ℕ) → DecidableEq (L.Rel k)]
{C : Set (LO.FirstOrder.SyntacticFormula L)}
{Δ : LO.FirstOrder.Sequent L}
:
LO.FirstOrder.Derivation.Restricted C Δ →
(p q : LO.FirstOrder.SyntacticFormula L) → LO.FirstOrder.Derivation.Restricted C (p :: List.remove (p ⋏ q) Δ)
Instances For
def
LO.FirstOrder.Derivation.andInversion₁
{L : LO.FirstOrder.Language}
[(k : ℕ) → DecidableEq (L.Func k)]
[(k : ℕ) → DecidableEq (L.Rel k)]
{C : Set (LO.FirstOrder.SyntacticFormula L)}
{Δ : LO.FirstOrder.Sequent L}
{p : LO.FirstOrder.SyntacticFormula L}
{q : LO.FirstOrder.SyntacticFormula L}
(d : LO.FirstOrder.Derivation.Restricted C (p ⋏ q :: Δ))
:
Equations
Instances For
@[irreducible]
def
LO.FirstOrder.Derivation.andInversion₂Aux
{L : LO.FirstOrder.Language}
[(k : ℕ) → DecidableEq (L.Func k)]
[(k : ℕ) → DecidableEq (L.Rel k)]
{C : Set (LO.FirstOrder.SyntacticFormula L)}
{Δ : LO.FirstOrder.Sequent L}
:
LO.FirstOrder.Derivation.Restricted C Δ →
(p q : LO.FirstOrder.SyntacticFormula L) → LO.FirstOrder.Derivation.Restricted C (q :: List.remove (p ⋏ q) Δ)
Instances For
def
LO.FirstOrder.Derivation.andInversion₂
{L : LO.FirstOrder.Language}
[(k : ℕ) → DecidableEq (L.Func k)]
[(k : ℕ) → DecidableEq (L.Rel k)]
{C : Set (LO.FirstOrder.SyntacticFormula L)}
{Δ : LO.FirstOrder.Sequent L}
{p : LO.FirstOrder.SyntacticFormula L}
{q : LO.FirstOrder.SyntacticFormula L}
(d : LO.FirstOrder.Derivation.Restricted C (p ⋏ q :: Δ))
:
Equations
Instances For
@[irreducible]
def
LO.FirstOrder.Derivation.allInversionAux
{L : LO.FirstOrder.Language}
[(k : ℕ) → DecidableEq (L.Func k)]
[(k : ℕ) → DecidableEq (L.Rel k)]
{C : Set (LO.FirstOrder.SyntacticFormula L)}
(hC : ∀ (f : ℕ → LO.FirstOrder.Semiterm L ℕ 0), ∀ p ∈ C, (LO.FirstOrder.Rew.rewrite f).hom p ∈ C)
{Δ : LO.FirstOrder.Sequent L}
:
LO.FirstOrder.Derivation.Restricted C Δ →
(p : LO.FirstOrder.SyntacticSemiformula L 1) →
(t : LO.FirstOrder.SyntacticTerm L) →
LO.FirstOrder.Derivation.Restricted C ((LO.FirstOrder.Rew.substs ![t]).hom p :: List.remove (∀' p) Δ)
Instances For
def
LO.FirstOrder.Derivation.allInversion
{L : LO.FirstOrder.Language}
[(k : ℕ) → DecidableEq (L.Func k)]
[(k : ℕ) → DecidableEq (L.Rel k)]
{C : Set (LO.FirstOrder.SyntacticFormula L)}
(hC : ∀ (f : ℕ → LO.FirstOrder.Semiterm L ℕ 0), ∀ p ∈ C, (LO.FirstOrder.Rew.rewrite f).hom p ∈ C)
{Δ : LO.FirstOrder.Sequent L}
{p : LO.FirstOrder.SyntacticSemiformula L (0 + 1)}
(d : LO.FirstOrder.Derivation.Restricted C ((∀' p) :: Δ))
(t : LO.FirstOrder.Semiterm L ℕ 0)
:
LO.FirstOrder.Derivation.Restricted C ((LO.FirstOrder.Rew.substs ![t]).hom p :: Δ)
Equations
- LO.FirstOrder.Derivation.allInversion hC d t = (LO.FirstOrder.Derivation.allInversionAux hC d p t).wk ⋯
Instances For
@[irreducible]
def
LO.FirstOrder.Derivation.falsumElimAux
{L : LO.FirstOrder.Language}
[(k : ℕ) → DecidableEq (L.Func k)]
[(k : ℕ) → DecidableEq (L.Rel k)]
{C : Set (LO.FirstOrder.SyntacticFormula L)}
{Δ : LO.FirstOrder.Sequent L}
:
Instances For
def
LO.FirstOrder.Derivation.falsumElim
{L : LO.FirstOrder.Language}
[(k : ℕ) → DecidableEq (L.Func k)]
[(k : ℕ) → DecidableEq (L.Rel k)]
{C : Set (LO.FirstOrder.SyntacticFormula L)}
{Δ : LO.FirstOrder.Sequent L}
(d : LO.FirstOrder.Derivation.Restricted C (⊥ :: Δ))
:
Equations
Instances For
@[irreducible]
def
LO.FirstOrder.Derivation.reductionAux
{L : LO.FirstOrder.Language}
[(k : ℕ) → DecidableEq (L.Func k)]
[(k : ℕ) → DecidableEq (L.Rel k)]
{i : ℕ}
{Δ : LO.FirstOrder.Sequent L}
:
LO.FirstOrder.Derivation.RestrictedComplexity i Δ →
{p : LO.FirstOrder.SyntacticFormula L} →
LO.FirstOrder.Semiformula.isVType p = true →
LO.FirstOrder.Semiformula.complexity p ≤ i →
{Γ : LO.FirstOrder.Sequent L} →
LO.FirstOrder.Derivation.RestrictedComplexity i (~p :: Γ) →
LO.FirstOrder.Derivation.RestrictedComplexity i (List.remove p Δ ++ Γ)
Instances For
def
LO.FirstOrder.Derivation.reduction
{L : LO.FirstOrder.Language}
[(k : ℕ) → DecidableEq (L.Func k)]
[(k : ℕ) → DecidableEq (L.Rel k)]
{Δ : LO.FirstOrder.Sequent L}
{i : ℕ}
{p : LO.FirstOrder.SyntacticFormula L}
(hp : LO.FirstOrder.Semiformula.complexity p ≤ i)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[irreducible]
def
LO.FirstOrder.Derivation.elimination
{L : LO.FirstOrder.Language}
[(k : ℕ) → DecidableEq (L.Func k)]
[(k : ℕ) → DecidableEq (L.Rel k)]
{i : ℕ}
{Δ : LO.FirstOrder.Sequent L}
:
Instances For
def
LO.FirstOrder.Derivation.hauptsatzClx
{L : LO.FirstOrder.Language}
[(k : ℕ) → DecidableEq (L.Func k)]
[(k : ℕ) → DecidableEq (L.Rel k)]
{Δ : LO.FirstOrder.Sequent L}
{i : ℕ}
:
LO.FirstOrder.Derivation.RestrictedComplexity i Δ → { d : ⊢¹ Δ // LO.FirstOrder.Derivation.CutFree d }
Equations
Instances For
def
LO.FirstOrder.Derivation.toClx
{L : LO.FirstOrder.Language}
{Δ : LO.FirstOrder.Sequent L}
:
⊢¹ Δ → (i : ℕ) × LO.FirstOrder.Derivation.RestrictedComplexity i Δ
Instances For
def
LO.FirstOrder.Derivation.hauptsatz
{L : LO.FirstOrder.Language}
[(k : ℕ) → DecidableEq (L.Func k)]
[(k : ℕ) → DecidableEq (L.Rel k)]
{Δ : LO.FirstOrder.Sequent L}
:
⊢¹ Δ → { d : ⊢¹ Δ // LO.FirstOrder.Derivation.CutFree d }
Equations
Instances For
theorem
LO.FirstOrder.Derivation.iff_cut
{L : LO.FirstOrder.Language}
{Δ : LO.FirstOrder.Sequent L}
:
Nonempty { d : ⊢¹ Δ // LO.FirstOrder.Derivation.CutFree d } ↔ ⊢¹! Δ