Documentation

Foundation.FirstOrder.Arith.Nonstandard

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