Documentation

Logic.FirstOrder.Arith.Model

source
@[simp]
theorem LO.FirstOrder.Arith.oringEmb_operator_zero_val {L : LO.FirstOrder.Language} [L.ORing] :
LO.FirstOrder.Semiterm.lMap LO.FirstOrder.Language.oringEmb op(0).term = op(0).term
source
@[simp]
theorem LO.FirstOrder.Arith.oringEmb_operator_one_val {L : LO.FirstOrder.Language} [L.ORing] :
LO.FirstOrder.Semiterm.lMap LO.FirstOrder.Language.oringEmb op(1).term = op(1).term
source
@[simp]
theorem LO.FirstOrder.Arith.oringEmb_operator_add_val {L : LO.FirstOrder.Language} [L.ORing] :
LO.FirstOrder.Semiterm.lMap LO.FirstOrder.Language.oringEmb op(+).term = op(+).term
source
@[simp]
theorem LO.FirstOrder.Arith.oringEmb_operator_mul_val {L : LO.FirstOrder.Language} [L.ORing] :
LO.FirstOrder.Semiterm.lMap LO.FirstOrder.Language.oringEmb op(*).term = op(*).term
source
@[simp]
theorem LO.FirstOrder.Arith.oringEmb_operator_eq_val {L : LO.FirstOrder.Language} [L.ORing] :
(LO.FirstOrder.Semiformula.lMap LO.FirstOrder.Language.oringEmb) op(=).sentence = op(=).sentence
source
@[simp]
theorem LO.FirstOrder.Arith.oringEmb_operator_lt_val {L : LO.FirstOrder.Language} [L.ORing] :
(LO.FirstOrder.Semiformula.lMap LO.FirstOrder.Language.oringEmb) op(<).sentence = op(<).sentence
source
instance LO.FirstOrder.Arith.standardModel (M : Type u_1) [LO.ORingStruc M] :
LO.FirstOrder.Structure β„’β‚’α΅£ M
Equations
  • One or more equations did not get rendered due to their size.
source
instance LO.FirstOrder.Arith.instEqORing (M : Type u_1) [LO.ORingStruc M] :
LO.FirstOrder.Structure.Eq β„’β‚’α΅£ M
Equations
  • β‹― = β‹―
source
instance LO.FirstOrder.Arith.instZeroORing (M : Type u_1) [LO.ORingStruc M] :
LO.FirstOrder.Structure.Zero β„’β‚’α΅£ M
Equations
  • β‹― = β‹―
source
instance LO.FirstOrder.Arith.instOneORing (M : Type u_1) [LO.ORingStruc M] :
LO.FirstOrder.Structure.One β„’β‚’α΅£ M
Equations
  • β‹― = β‹―
source
instance LO.FirstOrder.Arith.instAddORing (M : Type u_1) [LO.ORingStruc M] :
LO.FirstOrder.Structure.Add β„’β‚’α΅£ M
Equations
  • β‹― = β‹―
source
instance LO.FirstOrder.Arith.instMulORing (M : Type u_1) [LO.ORingStruc M] :
LO.FirstOrder.Structure.Mul β„’β‚’α΅£ M
Equations
  • β‹― = β‹―
source
instance LO.FirstOrder.Arith.instEqORing_1 (M : Type u_1) [LO.ORingStruc M] :
LO.FirstOrder.Structure.Eq β„’β‚’α΅£ M
Equations
  • β‹― = β‹―
source
instance LO.FirstOrder.Arith.instLTORing (M : Type u_1) [LO.ORingStruc M] :
LO.FirstOrder.Structure.LT β„’β‚’α΅£ M
Equations
  • β‹― = β‹―
source
instance LO.FirstOrder.Arith.instORingORing :
β„’β‚’α΅£.ORing
Equations
source
theorem LO.FirstOrder.Arith.standardModel_unique' (M : Type u_1) [LO.ORingStruc M] (s : LO.FirstOrder.Structure β„’β‚’α΅£ M) (hZero : LO.FirstOrder.Structure.Zero β„’β‚’α΅£ M) (hOne : LO.FirstOrder.Structure.One β„’β‚’α΅£ M) (hAdd : LO.FirstOrder.Structure.Add β„’β‚’α΅£ M) (hMul : LO.FirstOrder.Structure.Mul β„’β‚’α΅£ M) (hEq : LO.FirstOrder.Structure.Eq β„’β‚’α΅£ M) (hLT : LO.FirstOrder.Structure.LT β„’β‚’α΅£ M) :
s = LO.FirstOrder.Arith.standardModel M
source
theorem LO.FirstOrder.Arith.standardModel_unique (M : Type u_1) [LO.ORingStruc M] (s : LO.FirstOrder.Structure β„’β‚’α΅£ M) [hZero : LO.FirstOrder.Structure.Zero β„’β‚’α΅£ M] [hOne : LO.FirstOrder.Structure.One β„’β‚’α΅£ M] [hAdd : LO.FirstOrder.Structure.Add β„’β‚’α΅£ M] [hMul : LO.FirstOrder.Structure.Mul β„’β‚’α΅£ M] [hEq : LO.FirstOrder.Structure.Eq β„’β‚’α΅£ M] [hLT : LO.FirstOrder.Structure.LT β„’β‚’α΅£ M] :
s = LO.FirstOrder.Arith.standardModel M
source
theorem LO.FirstOrder.Arith.standardModel_lMap_oringEmb_eq_standardModel (M : Type u_1) [LO.ORingStruc M] {L : LO.FirstOrder.Language} [L.ORing] [s : LO.FirstOrder.Structure L M] [LO.FirstOrder.Structure.Zero L M] [LO.FirstOrder.Structure.One L M] [LO.FirstOrder.Structure.Add L M] [LO.FirstOrder.Structure.Mul L M] [LO.FirstOrder.Structure.Eq L M] [LO.FirstOrder.Structure.LT L M] :
LO.FirstOrder.Structure.lMap LO.FirstOrder.Language.oringEmb s = LO.FirstOrder.Arith.standardModel M
source
@[simp]
theorem LO.FirstOrder.Arith.val_lMap_oringEmb {n : β„•} {ΞΎ : Type u_2} {M : Type u_1} [LO.ORingStruc M] {L : LO.FirstOrder.Language} [L.ORing] [s : LO.FirstOrder.Structure L M] [LO.FirstOrder.Structure.Zero L M] [LO.FirstOrder.Structure.One L M] [LO.FirstOrder.Structure.Add L M] [LO.FirstOrder.Structure.Mul L M] [LO.FirstOrder.Structure.Eq L M] [LO.FirstOrder.Structure.LT L M] {e : Fin n β†’ M} {Ξ΅ : ΞΎ β†’ M} {t : LO.FirstOrder.Semiterm β„’β‚’α΅£ ΞΎ n} :
LO.FirstOrder.Semiterm.valm M e Ξ΅ (LO.FirstOrder.Semiterm.lMap LO.FirstOrder.Language.oringEmb t) = LO.FirstOrder.Semiterm.valm M e Ξ΅ t
source
@[simp]
theorem LO.FirstOrder.Arith.eval_lMap_oringEmb {n : β„•} {ΞΎ : Type u_2} {M : Type u_1} [LO.ORingStruc M] {L : LO.FirstOrder.Language} [L.ORing] [s : LO.FirstOrder.Structure L M] [LO.FirstOrder.Structure.Zero L M] [LO.FirstOrder.Structure.One L M] [LO.FirstOrder.Structure.Add L M] [LO.FirstOrder.Structure.Mul L M] [LO.FirstOrder.Structure.Eq L M] [LO.FirstOrder.Structure.LT L M] {e : Fin n β†’ M} {Ξ΅ : ΞΎ β†’ M} {p : LO.FirstOrder.Semiformula β„’β‚’α΅£ ΞΎ n} :
(LO.FirstOrder.Semiformula.Evalm M e Ξ΅) ((LO.FirstOrder.Semiformula.lMap LO.FirstOrder.Language.oringEmb) p) ↔ (LO.FirstOrder.Semiformula.Evalm M e Ξ΅) p
source
@[simp]
theorem LO.FirstOrder.Arith.modelsTheory_lMap_oringEmb {L : LO.FirstOrder.Language} [L.ORing] {M : Type u_1} [LO.ORingStruc M] [s : LO.FirstOrder.Structure L M] [LO.FirstOrder.Structure.Zero L M] [LO.FirstOrder.Structure.One L M] [LO.FirstOrder.Structure.Add L M] [LO.FirstOrder.Structure.Mul L M] [LO.FirstOrder.Structure.Eq L M] [LO.FirstOrder.Structure.LT L M] (T : LO.FirstOrder.Theory β„’β‚’α΅£) :
M βŠ§β‚˜* LO.FirstOrder.Theory.lMap LO.FirstOrder.Language.oringEmb T ↔ M βŠ§β‚˜* T
source
instance LO.FirstOrder.Arith.instModelsTheoryPAMinusOfIOpen {M : Type u_1} [LO.ORingStruc M] [M βŠ§β‚˜* 𝐈open] :
M βŠ§β‚˜* 𝐏𝐀⁻
Equations
  • β‹― = β‹―
source
instance LO.FirstOrder.Arith.instModelsTheoryIndSchemeORingOpenNatOfIOpen {M : Type u_1} [LO.ORingStruc M] [M βŠ§β‚˜* 𝐈open] :
M βŠ§β‚˜* LO.FirstOrder.Theory.indScheme β„’β‚’α΅£ LO.FirstOrder.Semiformula.Open
Equations
  • β‹― = β‹―
source
def LO.FirstOrder.Arith.models_PAMinus_of_models_indH {M : Type u_1} [LO.ORingStruc M] (Ξ“ : LO.Polarity) (n : β„•) [M βŠ§β‚˜* πˆππƒΞ“ n] :
M βŠ§β‚˜* 𝐏𝐀⁻
Equations
  • β‹― = β‹―
Instances For
    source
    def LO.FirstOrder.Arith.models_indScheme_of_models_indH {M : Type u_1} [LO.ORingStruc M] (Ξ“ : LO.Polarity) (n : β„•) [M βŠ§β‚˜* πˆππƒΞ“ n] :
    M βŠ§β‚˜* LO.FirstOrder.Theory.indScheme β„’β‚’α΅£ (LO.FirstOrder.Arith.Hierarchy Ξ“ n)
    Equations
    • β‹― = β‹―
    Instances For
      source
      instance LO.FirstOrder.Arith.models_PAMinus_of_models_peano {M : Type u_1} [LO.ORingStruc M] [M βŠ§β‚˜* 𝐏𝐀] :
      M βŠ§β‚˜* 𝐏𝐀⁻
      Equations
      • β‹― = β‹―
      source
      instance LO.FirstOrder.Arith.Standard.models_CobhamR0 :
      β„• βŠ§β‚˜* 𝐑₀
      Equations
      source
      instance LO.FirstOrder.Arith.Standard.models_PAMinus :
      β„• βŠ§β‚˜* 𝐏𝐀⁻
      Equations
      source
      theorem LO.FirstOrder.Arith.Standard.models_succInd (p : LO.FirstOrder.Semiformula β„’β‚’α΅£ β„• 1) :
      β„• βŠ§β‚˜ LO.FirstOrder.succInd p
      source
      instance LO.FirstOrder.Arith.Standard.models_iSigma (Ξ“ : LO.Polarity) (k : β„•) :
      β„• βŠ§β‚˜* πˆππƒΞ“ k
      Equations
      • β‹― = β‹―
      source
      instance LO.FirstOrder.Arith.Standard.models_iSigmaZero :
      β„• βŠ§β‚˜* πˆπšΊβ‚€
      Equations
      source
      instance LO.FirstOrder.Arith.Standard.models_iSigmaOne :
      β„• βŠ§β‚˜* πˆπšΊβ‚
      Equations
      source
      instance LO.FirstOrder.Arith.Standard.models_peano :
      β„• βŠ§β‚˜* 𝐏𝐀
      Equations
      source
      structure LO.FirstOrder.Arith.Cut (L : LO.FirstOrder.Language) [L.ORing] (M : Type w) [s : LO.FirstOrder.Structure L M] :
      Type w
      Instances For
        source
        theorem LO.FirstOrder.Arith.Cut.closedSucc {L : LO.FirstOrder.Language} [L.ORing] {M : Type w} [s : LO.FirstOrder.Structure L M] (self : LO.FirstOrder.Arith.Cut L M) (x : M) :
        x ∈ self.domain β†’ LO.FirstOrder.Semiterm.valb s ![x] (β€˜(!!(LO.FirstOrder.Semiterm.bvar 0) + 1)’) ∈ self.domain
        source
        theorem LO.FirstOrder.Arith.Cut.closedLt {L : LO.FirstOrder.Language} [L.ORing] {M : Type w} [s : LO.FirstOrder.Structure L M] (self : LO.FirstOrder.Arith.Cut L M) (x : M) (y : M) :
        (LO.FirstOrder.Semiformula.Evalb s ![x, y]) (β€œ!!(LO.FirstOrder.Semiterm.bvar 0) < !!(LO.FirstOrder.Semiterm.bvar 1)”) β†’ y ∈ self.domain β†’ x ∈ self.domain
        source
        structure LO.FirstOrder.Arith.ClosedCut (L : LO.FirstOrder.Language) [L.ORing] (M : Type w) [s : LO.FirstOrder.Structure L M] extends LO.FirstOrder.Structure.ClosedSubset :
        Type w
        Instances For
          source
          theorem LO.FirstOrder.Arith.ClosedCut.closedLt {L : LO.FirstOrder.Language} [L.ORing] {M : Type w} [s : LO.FirstOrder.Structure L M] (self : LO.FirstOrder.Arith.ClosedCut L M) (x : M) (y : M) :
          (LO.FirstOrder.Semiformula.Evalb s ![x, y]) (β€œ!!(LO.FirstOrder.Semiterm.bvar 0) < !!(LO.FirstOrder.Semiterm.bvar 1)”) β†’ y ∈ self.domain β†’ x ∈ self.domain
          source
          @[reducible, inline]
          abbrev LO.FirstOrder.Arith.Theory.TrueArith :
          LO.FirstOrder.Theory β„’β‚’α΅£
          Equations
          Instances For
            source
            def LO.FirstOrder.Arith.Β«term𝐓𝐀» :
            Lean.ParserDescr
            Equations
            Instances For
              source
              instance LO.FirstOrder.Arith.Standard.models_trueArith :
              β„• βŠ§β‚˜* 𝐓𝐀
              Equations
              source
              theorem LO.FirstOrder.Arith.oRing_consequence_of (T : LO.FirstOrder.Theory β„’β‚’α΅£) [𝐄𝐐 β‰Ό T] (p : LO.FirstOrder.SyntacticFormula β„’β‚’α΅£) (H : βˆ€ (M : Type u_1) [inst : LO.ORingStruc M] [inst_1 : M βŠ§β‚˜* T], M βŠ§β‚˜ p) :
              T ⊨ p
              source
              instance LO.FirstOrder.Theory.CobhamR0.consistent :
              LO.System.Consistent 𝐑₀
              Equations
              source
              instance LO.FirstOrder.Theory.Peano.consistent :
              LO.System.Consistent 𝐏𝐀
              Equations