Documentation

Foundation.FirstOrder.Completeness.SearchTree

Instances For
    Instances For
      theorem LO.FirstOrder.Completeness.ReduxNat.antimonotone {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Func k)] [(k : ) → Encodable (L.Rel k)] {T : LO.FirstOrder.Theory L} {s : } {Δ₂ : LO.FirstOrder.Sequent L} {Δ₁ : LO.FirstOrder.Sequent L} (h : LO.FirstOrder.Completeness.ReduxNat T s Δ₂ Δ₁) :
      Δ₁ Δ₂
      Instances For
        @[reducible, inline]
        Equations
        • τ.rank = τ.fst
        Instances For
          @[reducible, inline]
          Equations
          • τ.seq = τ.snd.fst
          Instances For
            Instances For
              Equations
              • LO.FirstOrder.Completeness.SearchTree.instTop = { top := 0, Γ, LO.FirstOrder.Completeness.SearchTreeAux.zero }
              @[simp]
              theorem LO.FirstOrder.Completeness.SearchTree.rank_top {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Func k)] [(k : ) → Encodable (L.Rel k)] {T : LO.FirstOrder.Theory L} {Γ : LO.FirstOrder.Sequent L} :
              .rank = 0
              @[simp]
              theorem LO.FirstOrder.Completeness.SearchTree.seq_top {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Func k)] [(k : ) → Encodable (L.Rel k)] {T : LO.FirstOrder.Theory L} {Γ : LO.FirstOrder.Sequent L} :
              .seq = Γ
              noncomputable def LO.FirstOrder.Completeness.syntacticMainLemma {L : LO.FirstOrder.Language} [(k : ) → DecidableEq (L.Func k)] [(k : ) → DecidableEq (L.Rel k)] [(k : ) → Encodable (L.Func k)] [(k : ) → Encodable (L.Rel k)] {T : LO.FirstOrder.Theory L} {Γ : LO.FirstOrder.Sequent L} (wf : WellFounded (LO.FirstOrder.Completeness.SearchTree.Lt T Γ)) (p : LO.FirstOrder.Completeness.SearchTree T Γ) :
              T p.seq
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                noncomputable def LO.FirstOrder.Completeness.chain {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Func k)] [(k : ) → Encodable (L.Rel k)] (T : LO.FirstOrder.Theory L) (Γ : LO.FirstOrder.Sequent L) (s : ) :
                Equations
                Instances For
                  Equations
                  • LO.FirstOrder.Completeness.instInhabitedModel = { default := default }
                  Equations
                  • One or more equations did not get rendered due to their size.