Documentation

Incompleteness.Arith.Theory

Formalized $\Sigma_1$-Completeness #

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
      Instances For
        @[reducible, inline]
        Equations
        Instances For
          def LO.Arith.singleton {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Func k)] [(k : ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] (φ : LO.FirstOrder.SyntacticFormula L) :
          {φ}.Delta1Definable
          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.
            @[reducible, inline]
            Equations
            Instances For
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                Equations
                Instances For
                  @[reducible, inline]
                  Equations
                  Instances For
                    @[simp]
                    Equations
                    • One or more equations did not get rendered due to their size.

                    Provability predicate for arithmetic stronger than $\mathbf{R_0}$.

                    Equations
                    Instances For
                      theorem LO.Arith.provableₐ_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : LO.FirstOrder.Theory ℒₒᵣ) [T.Delta1Definable] :
                      𝚺₁-Predicate T.Provableₐ via T.provableₐ
                      @[simp]
                      theorem LO.Arith.eval_provableₐ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : LO.FirstOrder.Theory ℒₒᵣ) [T.Delta1Definable] (v : Fin 1V) :
                      V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val T.provableₐ) T.Provableₐ (v 0)
                      instance LO.Arith.provableₐ_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : LO.FirstOrder.Theory ℒₒᵣ) [T.Delta1Definable] :
                      𝚺₁-Predicate T.Provableₐ
                      Equations
                      • =
                      instance LO.Arith.provableₐ_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : LO.FirstOrder.Theory ℒₒᵣ) [T.Delta1Definable] :
                      { Γ := 𝚺, rank := 0 + 1 }-Predicate T.Provableₐ

                      instance for definability tactic

                      Equations
                      • =