Documentation

Foundation.FirstOrder.Basic.Calculus2

Derivation2 #

Different characterizations of proof.

inductive LO.FirstOrder.Derivation2 {L : LO.FirstOrder.Language} [(k : ) → DecidableEq (L.Func k)] [(k : ) → DecidableEq (L.Rel k)] (T : LO.FirstOrder.Theory L) :
Instances For
    @[reducible, inline]
    Equations
    Instances For
      @[reducible, inline]
      Equations
      Instances For
        theorem LO.FirstOrder.shifts_toFinset_eq_image_shift {L : LO.FirstOrder.Language} [(k : ) → DecidableEq (L.Func k)] [(k : ) → DecidableEq (L.Rel k)] (Δ : LO.FirstOrder.Sequent L) :
        (LO.FirstOrder.shifts Δ).toFinset = Finset.image ((LO.FirstOrder.Rew.hom LO.FirstOrder.Rew.shift)) (List.toFinset Δ)
        noncomputable def LO.FirstOrder.Derivation2.toDerivation {L : LO.FirstOrder.Language} [(k : ) → DecidableEq (L.Func k)] [(k : ) → DecidableEq (L.Rel k)] {T : LO.FirstOrder.Theory L} {Γ : Finset (LO.FirstOrder.SyntacticFormula L)} :
        LO.FirstOrder.Derivation2 T ΓT Γ.toList
        Instances For