Supporting results for pointwise provable equality.

Canonical model of classical first-order logic

Main reference: Jeremy Avigad, Algebraic proofs of cut elimination [Avi01]

inductive PointwiseComposition.FFL.FirstOrder.LK.Derivation.IsCutFree {L : Language} {Γ : Sequent L} : ⊢ᴸᴷ¹ Γ → Prop

Data and laws for Is Cut Free in FFL.FirstOrder.LK.Derivation.

• 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

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.LK.Derivation.isCutFree_or_iff {L : Language} {Γ : Sequent L} {φ ψ : Proposition L} {d : ⊢ᴸᴷ¹ Γ + (⦃φ⦄ + ⦃ψ⦄)} : d.or.IsCutFree ↔ d.IsCutFree

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.LK.Derivation.isCutFree_and_iff {L : Language} {Γ : Sequent L} {φ ψ : Proposition L} {dφ : ⊢ᴸᴷ¹ Γ + ⦃φ⦄} {dψ : ⊢ᴸᴷ¹ Γ + ⦃ψ⦄} : (dφ.and dψ).IsCutFree ↔ dφ.IsCutFree ∧ dψ.IsCutFree

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.LK.Derivation.isCutFree_all_iff {L : Language} {Γ : Sequent L} {φ : Semiproposition L (0 + 1)} {d : ⊢ᴸᴷ¹ Rewriting.shifts Γ + ⦃Rewriting.free φ⦄} : d.all.IsCutFree ↔ d.IsCutFree

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.LK.Derivation.isCutFree_exs_iff {L : Language} {Γ : Sequent L} {φ : Semiproposition L (Nat.succ 0)} {t : Semiterm L ℕ 0} {d : ⊢ᴸᴷ¹ Γ + ⦃φ/[t]⦄} : d.exs.IsCutFree ↔ d.IsCutFree

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.LK.Derivation.isCutFree_contraction_iff {L : Language} {Γ : Sequent L} {φ : Proposition L} {d : ⊢ᴸᴷ¹ Γ + (⦃φ⦄ + ⦃φ⦄)} : d.contraction.IsCutFree ↔ d.IsCutFree

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.LK.Derivation.isCutFree_weakening_iff {L : Language} {Γ : Sequent L} {φ : Proposition L} {d : ⊢ᴸᴷ¹ Γ} : d.weakening.IsCutFree ↔ d.IsCutFree

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.LK.Derivation.IsCutFree.cast {L : Language} {Γ Δ : Sequent L} {d : ⊢ᴸᴷ¹ Γ} {e : Γ = Δ} : (d.cast e).IsCutFree ↔ d.IsCutFree

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.LK.Derivation.IsCutFree.not_cut {L : Language} {Γ Δ : Sequent L} {φ : Proposition L} (dp : ⊢ᴸᴷ¹ Γ + ⦃φ⦄) (dn : ⊢ᴸᴷ¹ Δ + ⦃∼φ⦄) : ¬(dp.cut dn).IsCutFree

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.LK.Derivation.isCutFree_rewrite_iff_isCutFree {L : Language} {Γ : Sequent L} {f : ℕ → SyntacticTerm L} {d : ⊢ᴸᴷ¹ Γ} : (rewrite f d).IsCutFree ↔ d.IsCutFree

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.LK.Derivation.isCutFree_map_iff_isCutFree {L : Language} {Γ : Sequent L} {f : ℕ → ℕ} {d : ⊢ᴸᴷ¹ Γ} : (d.map f).IsCutFree ↔ d.IsCutFree

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.LK.Derivation.IsCutFree.generalizeByNewVar_isCutFree {L : Language} {Δ : Sequent L} {m : ℕ} {φ : Semiproposition L 1} (hp : ¬Semiformula.HasFreeVariable φ m) (hΔ : ∀ ψ ∈ Δ, ¬Semiformula.HasFreeVariable ψ m) (d : ⊢ᴸᴷ¹ Δ + ⦃φ/[Semiterm.fvar m]⦄) : (generalizeByNewVar hp hΔ d).IsCutFree ↔ d.IsCutFree