Documentation

Arithmetization.ISigmaOne.Metamath.Proof.Derivation

Equations
  • L.IsFormulaSet s = ps, L.IsFormula p
Instances For
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      theorem LO.Arith.Language.isFormulaSet_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] :
      𝚫₁-Predicate L.IsFormulaSet via pL.isFormulaSetDef
      Equations
      • =
      instance LO.Arith.Language.isFormulaSet_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {Γ : LO.SigmaPiDelta} {m : } :
      { Γ := Γ, rank := m + 1 }-Predicate L.IsFormulaSet
      Equations
      • =
      @[simp]
      theorem LO.Arith.Language.IsFormulaSet.empty {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] :
      L.IsFormulaSet
      @[simp]
      theorem LO.Arith.Language.IsFormulaSet.singleton {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {p : V} :
      L.IsFormulaSet {p} L.IsFormula p
      @[simp]
      theorem LO.Arith.Language.IsFormulaSet.insert_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {p : V} {s : V} :
      L.IsFormulaSet (insert p s) L.IsFormula p L.IsFormulaSet s
      theorem LO.Arith.Language.IsFormulaSet.insert {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {p : V} {s : V} :
      L.IsFormulaSet (insert p s)L.IsFormula p L.IsFormulaSet s

      Alias of the forward direction of LO.Arith.Language.IsFormulaSet.insert_iff.

      @[simp]
      theorem LO.Arith.Language.IsFormulaSet.union {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {s₁ : V} {s₂ : V} :
      L.IsFormulaSet (s₁ s₂) L.IsFormulaSet s₁ L.IsFormulaSet s₂
      theorem LO.Arith.setShift_existsUnique {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (s : V) :
      ∃! t : V, ∀ (y : V), y t xs, y = L.shift x
      def LO.Arith.Language.setShift {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (s : V) :
      V
      Equations
      Instances For
        theorem LO.Arith.mem_setShift_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {s : V} {y : V} :
        y L.setShift s xs, y = L.shift x
        theorem LO.Arith.Language.IsFormulaSet.setShift {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {s : V} (h : L.IsFormulaSet s) :
        L.IsFormulaSet (L.setShift s)
        theorem LO.Arith.shift_mem_setShift {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {p : V} {s : V} (h : p s) :
        L.shift p L.setShift s
        @[simp]
        theorem LO.Arith.Language.IsFormulaSet.setShift_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {s : V} :
        L.IsFormulaSet (L.setShift s) L.IsFormulaSet s
        @[simp]
        theorem LO.Arith.mem_setShift_union {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {s : V} {t : V} :
        L.setShift (s t) = L.setShift s L.setShift t
        @[simp]
        theorem LO.Arith.mem_setShift_insert {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {x : V} {s : V} :
        L.setShift (insert x s) = insert (L.shift x) (L.setShift s)
        @[simp]
        theorem LO.Arith.setShift_empty {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] :
        L.setShift =
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          Equations
          • =
          def LO.Arith.axL {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (p : V) :
          V
          Equations
          Instances For
            def LO.Arith.verumIntro {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) :
            V
            Equations
            Instances For
              def LO.Arith.andIntro {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (p : V) (q : V) (dp : V) (dq : V) :
              V
              Equations
              Instances For
                def LO.Arith.orIntro {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (p : V) (q : V) (d : V) :
                V
                Equations
                Instances For
                  def LO.Arith.allIntro {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (p : V) (d : V) :
                  V
                  Equations
                  Instances For
                    def LO.Arith.exIntro {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (p : V) (t : V) (d : V) :
                    V
                    Equations
                    Instances For
                      def LO.Arith.wkRule {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (d : V) :
                      V
                      Equations
                      Instances For
                        def LO.Arith.shiftRule {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (d : V) :
                        V
                        Equations
                        Instances For
                          def LO.Arith.cutRule {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (p : V) (d₁ : V) (d₂ : V) :
                          V
                          Equations
                          Instances For
                            def LO.Arith.root {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (p : V) :
                            V
                            Equations
                            Instances For
                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  @[simp]
                                                  theorem LO.Arith.seq_lt_axL {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (p : V) :
                                                  @[simp]
                                                  theorem LO.Arith.arity_lt_axL {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (p : V) :
                                                  @[simp]
                                                  theorem LO.Arith.seq_lt_andIntro {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (p : V) (q : V) (dp : V) (dq : V) :
                                                  s < LO.Arith.andIntro s p q dp dq
                                                  @[simp]
                                                  theorem LO.Arith.p_lt_andIntro {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (p : V) (q : V) (dp : V) (dq : V) :
                                                  p < LO.Arith.andIntro s p q dp dq
                                                  @[simp]
                                                  theorem LO.Arith.q_lt_andIntro {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (p : V) (q : V) (dp : V) (dq : V) :
                                                  q < LO.Arith.andIntro s p q dp dq
                                                  @[simp]
                                                  theorem LO.Arith.dp_lt_andIntro {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (p : V) (q : V) (dp : V) (dq : V) :
                                                  dp < LO.Arith.andIntro s p q dp dq
                                                  @[simp]
                                                  theorem LO.Arith.dq_lt_andIntro {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (p : V) (q : V) (dp : V) (dq : V) :
                                                  dq < LO.Arith.andIntro s p q dp dq
                                                  @[simp]
                                                  theorem LO.Arith.seq_lt_orIntro {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (p : V) (q : V) (d : V) :
                                                  @[simp]
                                                  theorem LO.Arith.p_lt_orIntro {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (p : V) (q : V) (d : V) :
                                                  @[simp]
                                                  theorem LO.Arith.q_lt_orIntro {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (p : V) (q : V) (d : V) :
                                                  @[simp]
                                                  theorem LO.Arith.d_lt_orIntro {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (p : V) (q : V) (d : V) :
                                                  @[simp]
                                                  theorem LO.Arith.seq_lt_allIntro {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (p : V) (d : V) :
                                                  @[simp]
                                                  theorem LO.Arith.p_lt_allIntro {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (p : V) (d : V) :
                                                  @[simp]
                                                  theorem LO.Arith.s_lt_allIntro {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (p : V) (d : V) :
                                                  @[simp]
                                                  theorem LO.Arith.seq_lt_exIntro {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (p : V) (t : V) (d : V) :
                                                  @[simp]
                                                  theorem LO.Arith.p_lt_exIntro {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (p : V) (t : V) (d : V) :
                                                  @[simp]
                                                  theorem LO.Arith.t_lt_exIntro {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (p : V) (t : V) (d : V) :
                                                  @[simp]
                                                  theorem LO.Arith.d_lt_exIntro {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (p : V) (t : V) (d : V) :
                                                  @[simp]
                                                  theorem LO.Arith.seq_lt_wkRule {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (d : V) :
                                                  @[simp]
                                                  theorem LO.Arith.d_lt_wkRule {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (d : V) :
                                                  @[simp]
                                                  theorem LO.Arith.seq_lt_shiftRule {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (d : V) :
                                                  @[simp]
                                                  theorem LO.Arith.d_lt_shiftRule {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (d : V) :
                                                  @[simp]
                                                  theorem LO.Arith.seq_lt_cutRule {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (p : V) (d₁ : V) (d₂ : V) :
                                                  s < LO.Arith.cutRule s p d₁ d₂
                                                  @[simp]
                                                  theorem LO.Arith.p_lt_cutRule {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (p : V) (d₁ : V) (d₂ : V) :
                                                  p < LO.Arith.cutRule s p d₁ d₂
                                                  @[simp]
                                                  theorem LO.Arith.d₁_lt_cutRule {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (p : V) (d₁ : V) (d₂ : V) :
                                                  d₁ < LO.Arith.cutRule s p d₁ d₂
                                                  @[simp]
                                                  theorem LO.Arith.d₂_lt_cutRule {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (p : V) (d₁ : V) (d₂ : V) :
                                                  d₂ < LO.Arith.cutRule s p d₁ d₂
                                                  @[simp]
                                                  theorem LO.Arith.seq_lt_root {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (p : V) :
                                                  @[simp]
                                                  theorem LO.Arith.p_lt_root {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (p : V) :
                                                  @[simp]
                                                  theorem LO.Arith.fstIdx_axL {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (p : V) :
                                                  @[simp]
                                                  theorem LO.Arith.fstIdx_andIntro {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (p : V) (q : V) (dp : V) (dq : V) :
                                                  @[simp]
                                                  theorem LO.Arith.fstIdx_orIntro {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (p : V) (q : V) (dpq : V) :
                                                  @[simp]
                                                  theorem LO.Arith.fstIdx_allIntro {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (p : V) (d : V) :
                                                  @[simp]
                                                  theorem LO.Arith.fstIdx_exIntro {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (p : V) (t : V) (d : V) :
                                                  @[simp]
                                                  @[simp]
                                                  theorem LO.Arith.fstIdx_cutRule {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (p : V) (d₁ : V) (d₂ : V) :
                                                  @[simp]
                                                  theorem LO.Arith.fstIdx_root {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (p : V) :
                                                  @[reducible, inline]
                                                  Equations
                                                  Instances For
                                                    def LO.Arith.Derivation.Phi {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (T : L.Theory) (C : Set V) (d : V) :
                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For
                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For
                                                        def LO.Arith.Derivation.construction {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (T : L.Theory) {pT : pL.TDef} [T.Defined pT] :
                                                        Equations
                                                        Instances For
                                                          def LO.Arith.Language.Theory.Derivation {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (T : L.Theory) {pT : pL.TDef} [T.Defined pT] :
                                                          VProp
                                                          Equations
                                                          Instances For
                                                            def LO.Arith.Language.Theory.DerivationOf {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (T : L.Theory) {pT : pL.TDef} [T.Defined pT] (d : V) (s : V) :
                                                            Equations
                                                            Instances For
                                                              def LO.Arith.Language.Theory.Derivable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (T : L.Theory) {pT : pL.TDef} [T.Defined pT] (s : V) :
                                                              Equations
                                                              • T.Derivable s = ∃ (d : V), T.DerivationOf d s
                                                              Instances For
                                                                def LO.Arith.Language.Theory.Provable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (T : L.Theory) {pT : pL.TDef} [T.Defined pT] (p : V) :
                                                                Equations
                                                                • T.Provable p = T.Derivable {p}
                                                                Instances For
                                                                  Equations
                                                                  Instances For
                                                                    theorem LO.Arith.Language.Theory.derivation_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (T : L.Theory) {pT : pL.TDef} [T.Defined pT] :
                                                                    𝚫₁-Predicate T.Derivation via pT.derivationDef
                                                                    instance LO.Arith.Language.Theory.derivation_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (T : L.Theory) {pT : pL.TDef} [T.Defined pT] :
                                                                    𝚫₁-Predicate T.Derivation
                                                                    Equations
                                                                    • =
                                                                    instance LO.Arith.Language.Theory.derivation_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (T : L.Theory) {pT : pL.TDef} [T.Defined pT] {Γ : LO.SigmaPiDelta} {m : } :
                                                                    { Γ := Γ, rank := m + 1 }-Predicate T.Derivation
                                                                    Equations
                                                                    • =
                                                                    Equations
                                                                    • One or more equations did not get rendered due to their size.
                                                                    Instances For
                                                                      theorem LO.Arith.Language.Theory.derivationOf_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (T : L.Theory) {pT : pL.TDef} [T.Defined pT] :
                                                                      𝚫₁-Relation T.DerivationOf via pT.derivationOfDef
                                                                      instance LO.Arith.Language.Theory.derivationOf_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (T : L.Theory) {pT : pL.TDef} [T.Defined pT] :
                                                                      𝚫₁-Relation T.DerivationOf
                                                                      Equations
                                                                      • =
                                                                      instance LO.Arith.Language.Theory.derivationOf_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (T : L.Theory) {pT : pL.TDef} [T.Defined pT] {Γ : LO.SigmaPiDelta} {m : } :
                                                                      { Γ := Γ, rank := m + 1 }-Relation T.DerivationOf
                                                                      Equations
                                                                      • =
                                                                      Equations
                                                                      • One or more equations did not get rendered due to their size.
                                                                      Instances For
                                                                        theorem LO.Arith.Language.Theory.derivable_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (T : L.Theory) {pT : pL.TDef} [T.Defined pT] :
                                                                        𝚺₁-Predicate T.Derivable via pT.derivableDef
                                                                        instance LO.Arith.Language.Theory.derivable_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (T : L.Theory) {pT : pL.TDef} [T.Defined pT] :
                                                                        𝚺₁-Predicate T.Derivable
                                                                        Equations
                                                                        • =
                                                                        instance LO.Arith.Language.Theory.derivable_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (T : L.Theory) {pT : pL.TDef} [T.Defined pT] :
                                                                        { Γ := 𝚺, rank := 0 + 1 }-Predicate T.Derivable

                                                                        instance for definability tactic

                                                                        Equations
                                                                        • =
                                                                        def LO.FirstOrder.Arith.LDef.TDef.prv {pL : LO.FirstOrder.Arith.LDef} (pT : pL.TDef) :
                                                                        𝚺₁.Semisentence 1
                                                                        Equations
                                                                        • One or more equations did not get rendered due to their size.
                                                                        Instances For
                                                                          theorem LO.Arith.Language.Theory.provable_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (T : L.Theory) {pT : pL.TDef} [T.Defined pT] :
                                                                          𝚺₁-Predicate T.Provable via pT.prv
                                                                          instance LO.Arith.Language.Theory.provable_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (T : L.Theory) {pT : pL.TDef} [T.Defined pT] :
                                                                          Equations
                                                                          • =
                                                                          instance LO.Arith.Language.Theory.provable_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (T : L.Theory) {pT : pL.TDef} [T.Defined pT] :
                                                                          { Γ := 𝚺, rank := 0 + 1 }-Predicate T.Provable

                                                                          instance for definability tactic

                                                                          Equations
                                                                          • =
                                                                          theorem LO.Arith.Language.Theory.Derivation.case_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {d : V} :
                                                                          T.Derivation d L.IsFormulaSet (LO.Arith.fstIdx d) ((∃ (s : V) (p : V), d = LO.Arith.axL s p p s L.neg p s) (∃ (s : V), d = LO.Arith.verumIntro s LO.Arith.qqVerum s) (∃ (s : V) (p : V) (q : V) (dp : V) (dq : V), d = LO.Arith.andIntro s p q dp dq LO.Arith.qqAnd p q s T.DerivationOf dp (insert p s) T.DerivationOf dq (insert q s)) (∃ (s : V) (p : V) (q : V) (dpq : V), d = LO.Arith.orIntro s p q dpq LO.Arith.qqOr p q s T.DerivationOf dpq (insert p (insert q s))) (∃ (s : V) (p : V) (dp : V), d = LO.Arith.allIntro s p dp LO.Arith.qqAll p s T.DerivationOf dp (insert (L.free p) (L.setShift s))) (∃ (s : V) (p : V) (t : V) (dp : V), d = LO.Arith.exIntro s p t dp LO.Arith.qqEx p s L.IsTerm t T.DerivationOf dp (insert (L.substs₁ t p) s)) (∃ (s : V) (d' : V), d = LO.Arith.wkRule s d' LO.Arith.fstIdx d' s T.Derivation d') (∃ (s : V) (d' : V), d = LO.Arith.shiftRule s d' s = L.setShift (LO.Arith.fstIdx d') T.Derivation d') (∃ (s : V) (p : V) (d₁ : V) (d₂ : V), d = LO.Arith.cutRule s p d₁ d₂ T.DerivationOf d₁ (insert p s) T.DerivationOf d₂ (insert (L.neg p) s)) ∃ (s : V) (p : V), d = LO.Arith.root s p p s p T)
                                                                          theorem LO.Arith.Language.Theory.Derivation.mk {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {d : V} :
                                                                          L.IsFormulaSet (LO.Arith.fstIdx d) ((∃ (s : V) (p : V), d = LO.Arith.axL s p p s L.neg p s) (∃ (s : V), d = LO.Arith.verumIntro s LO.Arith.qqVerum s) (∃ (s : V) (p : V) (q : V) (dp : V) (dq : V), d = LO.Arith.andIntro s p q dp dq LO.Arith.qqAnd p q s T.DerivationOf dp (insert p s) T.DerivationOf dq (insert q s)) (∃ (s : V) (p : V) (q : V) (dpq : V), d = LO.Arith.orIntro s p q dpq LO.Arith.qqOr p q s T.DerivationOf dpq (insert p (insert q s))) (∃ (s : V) (p : V) (dp : V), d = LO.Arith.allIntro s p dp LO.Arith.qqAll p s T.DerivationOf dp (insert (L.free p) (L.setShift s))) (∃ (s : V) (p : V) (t : V) (dp : V), d = LO.Arith.exIntro s p t dp LO.Arith.qqEx p s L.IsTerm t T.DerivationOf dp (insert (L.substs₁ t p) s)) (∃ (s : V) (d' : V), d = LO.Arith.wkRule s d' LO.Arith.fstIdx d' s T.Derivation d') (∃ (s : V) (d' : V), d = LO.Arith.shiftRule s d' s = L.setShift (LO.Arith.fstIdx d') T.Derivation d') (∃ (s : V) (p : V) (d₁ : V) (d₂ : V), d = LO.Arith.cutRule s p d₁ d₂ T.DerivationOf d₁ (insert p s) T.DerivationOf d₂ (insert (L.neg p) s)) ∃ (s : V) (p : V), d = LO.Arith.root s p p s p T)T.Derivation d

                                                                          Alias of the reverse direction of LO.Arith.Language.Theory.Derivation.case_iff.

                                                                          theorem LO.Arith.Language.Theory.Derivation.case {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {d : V} :
                                                                          T.Derivation dL.IsFormulaSet (LO.Arith.fstIdx d) ((∃ (s : V) (p : V), d = LO.Arith.axL s p p s L.neg p s) (∃ (s : V), d = LO.Arith.verumIntro s LO.Arith.qqVerum s) (∃ (s : V) (p : V) (q : V) (dp : V) (dq : V), d = LO.Arith.andIntro s p q dp dq LO.Arith.qqAnd p q s T.DerivationOf dp (insert p s) T.DerivationOf dq (insert q s)) (∃ (s : V) (p : V) (q : V) (dpq : V), d = LO.Arith.orIntro s p q dpq LO.Arith.qqOr p q s T.DerivationOf dpq (insert p (insert q s))) (∃ (s : V) (p : V) (dp : V), d = LO.Arith.allIntro s p dp LO.Arith.qqAll p s T.DerivationOf dp (insert (L.free p) (L.setShift s))) (∃ (s : V) (p : V) (t : V) (dp : V), d = LO.Arith.exIntro s p t dp LO.Arith.qqEx p s L.IsTerm t T.DerivationOf dp (insert (L.substs₁ t p) s)) (∃ (s : V) (d' : V), d = LO.Arith.wkRule s d' LO.Arith.fstIdx d' s T.Derivation d') (∃ (s : V) (d' : V), d = LO.Arith.shiftRule s d' s = L.setShift (LO.Arith.fstIdx d') T.Derivation d') (∃ (s : V) (p : V) (d₁ : V) (d₂ : V), d = LO.Arith.cutRule s p d₁ d₂ T.DerivationOf d₁ (insert p s) T.DerivationOf d₂ (insert (L.neg p) s)) ∃ (s : V) (p : V), d = LO.Arith.root s p p s p T)

                                                                          Alias of the forward direction of LO.Arith.Language.Theory.Derivation.case_iff.

                                                                          theorem LO.Arith.Language.Theory.Derivation.induction1 {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] (Γ : LO.SigmaPiDelta) {P : VProp} (hP : { Γ := Γ, rank := 1 }-Predicate P) {d : V} (hd : T.Derivation d) (hAxL : ∀ (s : V), L.IsFormulaSet sps, L.neg p sP (LO.Arith.axL s p)) (hVerumIntro : ∀ (s : V), L.IsFormulaSet sLO.Arith.qqVerum sP (LO.Arith.verumIntro s)) (hAnd : ∀ (s : V), L.IsFormulaSet s∀ (p q dp dq : V), LO.Arith.qqAnd p q sT.DerivationOf dp (insert p s)T.DerivationOf dq (insert q s)P dpP dqP (LO.Arith.andIntro s p q dp dq)) (hOr : ∀ (s : V), L.IsFormulaSet s∀ (p q d : V), LO.Arith.qqOr p q sT.DerivationOf d (insert p (insert q s))P dP (LO.Arith.orIntro s p q d)) (hAll : ∀ (s : V), L.IsFormulaSet s∀ (p d : V), LO.Arith.qqAll p sT.DerivationOf d (insert (L.free p) (L.setShift s))P dP (LO.Arith.allIntro s p d)) (hEx : ∀ (s : V), L.IsFormulaSet s∀ (p t d : V), LO.Arith.qqEx p sL.IsTerm tT.DerivationOf d (insert (L.substs₁ t p) s)P dP (LO.Arith.exIntro s p t d)) (hWk : ∀ (s : V), L.IsFormulaSet s∀ (d : V), LO.Arith.fstIdx d sT.Derivation dP dP (LO.Arith.wkRule s d)) (hShift : ∀ (s : V), L.IsFormulaSet s∀ (d : V), s = L.setShift (LO.Arith.fstIdx d)T.Derivation dP dP (LO.Arith.shiftRule s d)) (hCut : ∀ (s : V), L.IsFormulaSet s∀ (p d₁ d₂ : V), T.DerivationOf d₁ (insert p s)T.DerivationOf d₂ (insert (L.neg p) s)P d₁P d₂P (LO.Arith.cutRule s p d₁ d₂)) (hRoot : ∀ (s : V), L.IsFormulaSet sps, p TP (LO.Arith.root s p)) :
                                                                          P d
                                                                          theorem LO.Arith.Language.Theory.Derivation.isFormulaSet {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {d : V} (h : T.Derivation d) :
                                                                          L.IsFormulaSet (LO.Arith.fstIdx d)
                                                                          theorem LO.Arith.Language.Theory.DerivationOf.isFormulaSet {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {d : V} {s : V} (h : T.DerivationOf d s) :
                                                                          L.IsFormulaSet s
                                                                          theorem LO.Arith.Language.Theory.Derivation.axL {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {s : V} {p : V} (hs : L.IsFormulaSet s) (h : p s) (hn : L.neg p s) :
                                                                          T.Derivation (LO.Arith.axL s p)
                                                                          theorem LO.Arith.Language.Theory.Derivation.verumIntro {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {s : V} (hs : L.IsFormulaSet s) (h : LO.Arith.qqVerum s) :
                                                                          T.Derivation (LO.Arith.verumIntro s)
                                                                          theorem LO.Arith.Language.Theory.Derivation.andIntro {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {s : V} {p : V} {q : V} {dp : V} {dq : V} (h : LO.Arith.qqAnd p q s) (hdp : T.DerivationOf dp (insert p s)) (hdq : T.DerivationOf dq (insert q s)) :
                                                                          T.Derivation (LO.Arith.andIntro s p q dp dq)
                                                                          theorem LO.Arith.Language.Theory.Derivation.orIntro {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {s : V} {p : V} {q : V} {dpq : V} (h : LO.Arith.qqOr p q s) (hdpq : T.DerivationOf dpq (insert p (insert q s))) :
                                                                          T.Derivation (LO.Arith.orIntro s p q dpq)
                                                                          theorem LO.Arith.Language.Theory.Derivation.allIntro {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {s : V} {p : V} {dp : V} (h : LO.Arith.qqAll p s) (hdp : T.DerivationOf dp (insert (L.free p) (L.setShift s))) :
                                                                          T.Derivation (LO.Arith.allIntro s p dp)
                                                                          theorem LO.Arith.Language.Theory.Derivation.exIntro {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {s : V} {p : V} {t : V} {dp : V} (h : LO.Arith.qqEx p s) (ht : L.IsTerm t) (hdp : T.DerivationOf dp (insert (L.substs₁ t p) s)) :
                                                                          T.Derivation (LO.Arith.exIntro s p t dp)
                                                                          theorem LO.Arith.Language.Theory.Derivation.wkRule {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {s : V} {s' : V} {d : V} (hs : L.IsFormulaSet s) (h : s' s) (hd : T.DerivationOf d s') :
                                                                          T.Derivation (LO.Arith.wkRule s d)
                                                                          theorem LO.Arith.Language.Theory.Derivation.shiftRule {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {s : V} {d : V} (hd : T.DerivationOf d s) :
                                                                          T.Derivation (LO.Arith.shiftRule (L.setShift s) d)
                                                                          theorem LO.Arith.Language.Theory.Derivation.cutRule {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {s : V} {p : V} {d₁ : V} {d₂ : V} (hd₁ : T.DerivationOf d₁ (insert p s)) (hd₂ : T.DerivationOf d₂ (insert (L.neg p) s)) :
                                                                          T.Derivation (LO.Arith.cutRule s p d₁ d₂)
                                                                          theorem LO.Arith.Language.Theory.Derivation.root {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {s : V} {p : V} (hs : L.IsFormulaSet s) (hp : p s) (hT : p T) :
                                                                          T.Derivation (LO.Arith.root s p)
                                                                          theorem LO.Arith.Language.Theory.Derivation.of_ss {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {U : L.Theory} {pU : pL.TDef} [U.Defined pU] (h : T U) {d : V} :
                                                                          T.Derivation dU.Derivation d
                                                                          theorem LO.Arith.Language.Theory.Derivable.isFormulaSet {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {s : V} (h : T.Derivable s) :
                                                                          L.IsFormulaSet s
                                                                          theorem LO.Arith.Language.Theory.Derivable.em {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {s : V} (hs : L.IsFormulaSet s) (p : V) (h : p s) (hn : L.neg p s) :
                                                                          T.Derivable s
                                                                          theorem LO.Arith.Language.Theory.Derivable.verum {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {s : V} (hs : L.IsFormulaSet s) (h : LO.Arith.qqVerum s) :
                                                                          T.Derivable s
                                                                          theorem LO.Arith.Language.Theory.Derivable.and_m {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {s : V} {p : V} {q : V} (h : LO.Arith.qqAnd p q s) (hp : T.Derivable (insert p s)) (hq : T.Derivable (insert q s)) :
                                                                          T.Derivable s
                                                                          theorem LO.Arith.Language.Theory.Derivable.or_m {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {s : V} {p : V} {q : V} (h : LO.Arith.qqOr p q s) (hpq : T.Derivable (insert p (insert q s))) :
                                                                          T.Derivable s
                                                                          theorem LO.Arith.Language.Theory.Derivable.all_m {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {s : V} {p : V} (h : LO.Arith.qqAll p s) (hp : T.Derivable (insert (L.free p) (L.setShift s))) :
                                                                          T.Derivable s
                                                                          theorem LO.Arith.Language.Theory.Derivable.ex_m {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {s : V} {p : V} {t : V} (h : LO.Arith.qqEx p s) (ht : L.IsTerm t) (hp : T.Derivable (insert (L.substs₁ t p) s)) :
                                                                          T.Derivable s
                                                                          theorem LO.Arith.Language.Theory.Derivable.wk {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {s : V} {s' : V} (hs : L.IsFormulaSet s) (h : s' s) (hd : T.Derivable s') :
                                                                          T.Derivable s
                                                                          theorem LO.Arith.Language.Theory.Derivable.shift {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {s : V} (hd : T.Derivable s) :
                                                                          T.Derivable (L.setShift s)
                                                                          theorem LO.Arith.Language.Theory.Derivable.ofSetEq {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {s : V} {s' : V} (h : ∀ (x : V), x s' x s) (hd : T.Derivable s') :
                                                                          T.Derivable s
                                                                          theorem LO.Arith.Language.Theory.Derivable.cut {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {s : V} (p : V) (hd₁ : T.Derivable (insert p s)) (hd₂ : T.Derivable (insert (L.neg p) s)) :
                                                                          T.Derivable s
                                                                          theorem LO.Arith.Language.Theory.Derivable.by_axm {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {s : V} (hs : L.IsFormulaSet s) (p : V) (hp : p s) (hT : p T) :
                                                                          T.Derivable s
                                                                          theorem LO.Arith.Language.Theory.Derivable.of_ss {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {U : L.Theory} {pU : pL.TDef} [U.Defined pU] (h : T U) {s : V} :
                                                                          T.Derivable sU.Derivable s
                                                                          theorem LO.Arith.Language.Theory.Derivable.and {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {s : V} {p : V} {q : V} (hp : T.Derivable (insert p s)) (hq : T.Derivable (insert q s)) :
                                                                          T.Derivable (insert (LO.Arith.qqAnd p q) s)
                                                                          theorem LO.Arith.Language.Theory.Derivable.or {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {s : V} {p : V} {q : V} (hpq : T.Derivable (insert p (insert q s))) :
                                                                          T.Derivable (insert (LO.Arith.qqOr p q) s)
                                                                          theorem LO.Arith.Language.Theory.Derivable.conj {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] (ps : V) {s : V} (hs : L.IsFormulaSet s) (ds : i < LO.Arith.len ps, T.Derivable (insert (LO.Arith.nth ps i) s)) :
                                                                          T.Derivable (insert (LO.Arith.qqConj ps) s)

                                                                          Crucial inducion for formalized $\Sigma_1$-completeness.

                                                                          theorem LO.Arith.Language.Theory.Derivable.disjDistr {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] (ps : V) (s : V) (d : T.Derivable (LO.Arith.vecToSet ps s)) :
                                                                          T.Derivable (insert (LO.Arith.qqDisj ps) s)
                                                                          theorem LO.Arith.Language.Theory.Derivable.disj {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] (ps : V) (s : V) {i : V} (hps : i < LO.Arith.len ps, L.IsFormula (LO.Arith.nth ps i)) (hi : i < LO.Arith.len ps) (d : T.Derivable (insert (LO.Arith.nth ps i) s)) :
                                                                          T.Derivable (insert (LO.Arith.qqDisj ps) s)
                                                                          theorem LO.Arith.Language.Theory.Derivable.all {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {s : V} {p : V} (hp : L.IsSemiformula 1 p) (dp : T.Derivable (insert (L.free p) (L.setShift s))) :
                                                                          T.Derivable (insert (LO.Arith.qqAll p) s)
                                                                          theorem LO.Arith.Language.Theory.Derivable.ex {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {s : V} {p : V} {t : V} (hp : L.IsSemiformula 1 p) (ht : L.IsTerm t) (dp : T.Derivable (insert (L.substs₁ t p) s)) :
                                                                          T.Derivable (insert (LO.Arith.qqEx p) s)