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} {Γ : Multiset (Proposition L)} {φ ψ : Proposition L} {d : ⊢ᴸᴷ¹ Γ + (⦃φ⦄ + ⦃ψ⦄)} : d.IsCutFree → d.or.IsCutFree
- and {L : Language} {Γ : Multiset (Proposition L)} {φ ψ : Proposition L} {dφ : ⊢ᴸᴷ¹ Γ + ⦃φ⦄} {dψ : ⊢ᴸᴷ¹ Γ + ⦃ψ⦄} : dφ.IsCutFree → dψ.IsCutFree → (dφ.and dψ).IsCutFree
- all {L : Language} {Γ : Multiset (Semiproposition L 0)} {φ : Semiproposition L (0 + 1)} {d : ⊢ᴸᴷ¹ Rewriting.shifts Γ + ⦃Rewriting.free φ⦄} : d.IsCutFree → d.all.IsCutFree
- exs {L : Language} {Γ : Multiset (Semiproposition L 0)} {φ : Semiproposition L (Nat.succ 0)} (t : Semiterm L ℕ 0) {d : ⊢ᴸᴷ¹ Γ + ⦃φ/[t]⦄} : d.IsCutFree → d.exs.IsCutFree
- contraction {L : Language} {Γ : Multiset (Proposition L)} {φ : Proposition L} {d : ⊢ᴸᴷ¹ Γ + (⦃φ⦄ + ⦃φ⦄)} : d.IsCutFree → d.contraction.IsCutFree
- weakening {L : Language} {Γ : Sequent L} {φ : Proposition L} {d : ⊢ᴸᴷ¹ Γ} : d.IsCutFree → d.weakening.IsCutFree
Instances For
@[simp]
theorem
FFL.FirstOrder.LK.Derivation.isCutFree_all_iff
{L : Language}
{Γ : Sequent L}
{φ : Semiproposition L (0 + 1)}
{d : ⊢ᴸᴷ¹ Rewriting.shifts Γ + ⦃Rewriting.free φ⦄}
:
@[simp]
theorem
FFL.FirstOrder.LK.Derivation.isCutFree_weakening_iff
{L : Language}
{Γ : Sequent L}
{φ : Proposition L}
{d : ⊢ᴸᴷ¹ Γ}
:
@[simp]
theorem
FFL.FirstOrder.LK.Derivation.IsCutFree.generalizeByNewVar_isCutFree
{L : Language}
{Δ : Sequent L}
{m : ℕ}
{φ : Semiproposition L 1}
(hp : ¬Semiformula.FVar? φ m)
(hΔ : ∀ ψ ∈ Δ, ¬Semiformula.FVar? ψ m)
(d : ⊢ᴸᴷ¹ Δ + ⦃φ/[Semiterm.fvar m]⦄)
: