Canonical model of classical first-order logic #
Main reference: Jeremy Avigad, Algebraic proofs of cut elimination [Avi01]
- identity {L : Language} {k : ℕ} (r : L.Rel k) (v : Fin k → Semiterm L ℕ 0) : (Derivation.identity r v).IsCutFree
- verum {L : Language} : Derivation.verum.IsCutFree
- or {L : Language} {φ ψ : Proposition L} {Γ : List (Proposition L)} {d : ⊢ᴸᴷ¹ φ :: ψ :: Γ} : d.IsCutFree → d.or.IsCutFree
- and {L : Language} {φ : Proposition L} {Γ : List (Proposition L)} {ψ : Proposition L} {dφ : ⊢ᴸᴷ¹ φ :: Γ} {dψ : ⊢ᴸᴷ¹ ψ :: Γ} : dφ.IsCutFree → dψ.IsCutFree → (dφ.and dψ).IsCutFree
- all {L : Language} {φ : Semiproposition L (0 + 1)} {Γ : List (Semiproposition L 0)} {d : ⊢ᴸᴷ¹ Rewriting.free φ :: Rewriting.shifts Γ} : d.IsCutFree → d.all.IsCutFree
- exs {L : Language} {φ : Semiproposition L (Nat.succ 0)} {Γ : List (Proposition L)} (t : Semiterm L ℕ 0) {d : ⊢ᴸᴷ¹ φ/[t] :: Γ} : d.IsCutFree → d.exs.IsCutFree
- contraction {L : Language} {Δ Γ : Sequent L} {d : ⊢ᴸᴷ¹ Δ} (ss : Δ ⊆ Γ) : d.IsCutFree → (d.contraction ss).IsCutFree
Instances For
@[simp]
theorem
LO.FirstOrder.Derivation.isCutFree_all_iff
{L : Language}
{Γ : Sequent L}
{φ : Semiproposition L (0 + 1)}
{d : ⊢ᴸᴷ¹ Rewriting.free φ :: Rewriting.shifts Γ}
:
@[simp]
theorem
LO.FirstOrder.Derivation.isCutFree_contraction_iff
{L : Language}
{Γ Δ : Sequent L}
{d : ⊢ᴸᴷ¹ Δ}
{ss : Δ ⊆ Γ}
:
@[simp]
theorem
LO.FirstOrder.Derivation.IsCutFree.genelalizeByNewver_isCutFree
{L : Language}
{Δ : Sequent L}
{m : ℕ}
{φ : Semiproposition L 1}
(hp : ¬Semiformula.FVar? φ m)
(hΔ : ∀ ψ ∈ Δ, ¬Semiformula.FVar? ψ m)
(d : ⊢ᴸᴷ¹ φ/[Semiterm.fvar m] :: Δ)
: