Documentation

Foundation.FirstOrder.Arith.Nonstandard

source
@[reducible, inline]
abbrev LO.FirstOrder.Arith.withStar :
LO.FirstOrder.Language
Equations
Instances For
    source
    def LO.FirstOrder.Arith.starUnbounded (c : ℕ) :
    LO.FirstOrder.Theory LO.FirstOrder.Arith.withStar
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def LO.FirstOrder.Arith.trueArithWithStarUnbounded (n : ℕ) :
      LO.FirstOrder.Theory LO.FirstOrder.Arith.withStar
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem LO.FirstOrder.Arith.trueArithWithStarUnbounded.cumulative :
        LO.Cumulative LO.FirstOrder.Arith.trueArithWithStarUnbounded
        source
        def LO.FirstOrder.Arith.modelStar (c : ℕ) :
        LO.FirstOrder.Structure LO.FirstOrder.Language.unit ℕ
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem LO.FirstOrder.Arith.satisfiable_trueArithWithStarUnbounded (c : ℕ) :
          LO.FirstOrder.Satisfiable (LO.FirstOrder.Arith.trueArithWithStarUnbounded c)
          source
          theorem LO.FirstOrder.Arith.satisfiable_union_trueArithWithStarUnbounded :
          LO.FirstOrder.Satisfiable (⋃ (c : ℕ), LO.FirstOrder.Arith.trueArithWithStarUnbounded c)
          source
          instance LO.FirstOrder.Arith.trueArithWithStarUnbounded.eqTheory :
          𝐄𝐐 ≼ ⋃ (c : ℕ), LO.FirstOrder.Arith.trueArithWithStarUnbounded c
          Equations
          source
          @[reducible, inline]
          abbrev LO.FirstOrder.Arith.Nonstandard :
          Type
          Equations
          Instances For
            source
            def LO.FirstOrder.Arith.Nonstandard.«termℕ⋆» :
            Lean.ParserDescr
            Equations
            Instances For
              source
              def LO.FirstOrder.Arith.Nonstandard.star :
              ℕ⋆
              Equations
              Instances For
                source
                theorem LO.FirstOrder.Arith.Nonstandard.models_union_trueArithWithStarUnbounded :
                ℕ⋆ ⊧ₘ* ⋃ (c : ℕ), LO.FirstOrder.Arith.trueArithWithStarUnbounded c
                source
                instance LO.FirstOrder.Arith.Nonstandard.trueArith :
                ℕ⋆ ⊧ₘ* 𝐓𝐀
                Equations
                source
                instance LO.FirstOrder.Arith.Nonstandard.instModelsTheoryPAMinus :
                ℕ⋆ ⊧ₘ* 𝐏𝐀⁻
                Equations
                source
                theorem LO.FirstOrder.Arith.Nonstandard.star_unbounded (n : ℕ) :
                ↑n < LO.FirstOrder.Arith.Nonstandard.star