Documentation

LeanPool.PointwiseComposition.Foundation.FirstOrder.Incompleteness.Consistency

Supporting results for pointwise provable equality.

Consistency predicate #

source
def PointwiseComposition.FFL.FirstOrder.Theory.Consistent (V : Type u_1) [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] :
Prop

The Consistent construction in FFL.FirstOrder.Theory.

Equations
Instances For
    source
    def PointwiseComposition.FFL.FirstOrder.Theory.ConsistentWith {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] (φ : V) :
    Prop

    The Consistent With construction in FFL.FirstOrder.Theory.

    Equations
    Instances For
      source
      theorem PointwiseComposition.FFL.FirstOrder.Theory.ConsistentWith.quote_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] {σ : Sentence L} :
      T.ConsistentWith ⌜σ⌝ ↔ ¬Arithmetic.Bootstrapping.Provable T ⌜∼σ⌝
      source
      noncomputable def PointwiseComposition.FFL.FirstOrder.Theory.consistent {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] :
      Π₁.Sentence

      The consistent construction in FFL.FirstOrder.Theory.

      Equations
      Instances For
        source
        @[simp]
        theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.consistent.defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] :
        (Semiformula.Evalb ![]) ↑T.consistent ↔ Theory.Consistent V T
        source
        noncomputable def PointwiseComposition.FFL.FirstOrder.Theory.consistentWith {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] :
        Π₁.Semisentence 1

        The consistent With construction in FFL.FirstOrder.Theory.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          instance PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.consistentWith.defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] :
          Π₁-Predicate T.ConsistentWith via T.consistentWith
          source
          instance PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.consistentWith.definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] :
          Π₁-Predicate T.ConsistentWith
          source
          @[reducible, inline]
          noncomputable abbrev PointwiseComposition.FFL.FirstOrder.Theory.consistentWithPred {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] (σ : Sentence L) :
          ArithmeticSentence

          The consistent With Pred construction in FFL.FirstOrder.Theory.

          Equations
          Instances For
            source
            noncomputable def PointwiseComposition.FFL.FirstOrder.Theory.consistentWithPred' {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] (σ : Sentence L) :
            Π₁.Sentence

            The consistent With Pred' construction in FFL.FirstOrder.Theory.

            Equations
            Instances For
              source
              @[reducible, inline]
              abbrev PointwiseComposition.FFL.FirstOrder.Theory.Con {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] :
              ArithmeticTheory

              The Con construction in FFL.FirstOrder.Theory.

              Equations
              Instances For
                source
                @[reducible, inline]
                abbrev PointwiseComposition.FFL.FirstOrder.Theory.Incon {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] :
                ArithmeticTheory

                The Incon construction in FFL.FirstOrder.Theory.

                Equations
                Instances For
                  source
                  @[instance_reducible]
                  noncomputable instance PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.instΔ₁Con {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] :
                  Theory.Δ₁ T.Con
                  Equations
                  source
                  @[instance_reducible]
                  noncomputable instance PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.instΔ₁Incon {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] :
                  Theory.Δ₁ T.Incon
                  Equations
                  source
                  theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.consistent_eq (T : ArithmeticTheory) [Theory.Δ₁ T] :
                  ↑(Theory.consistent T) = (Theory.standardProvability T).con
                  source
                  @[simp]
                  theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.standard_consistent (T : ArithmeticTheory) [Theory.Δ₁ T] :
                  Theory.Consistent ℕ T ↔ Entailment.Consistent T
                  source
                  instance PointwiseComposition.FFL.FirstOrder.Arithmetic.instModelsSetStrucORingSentenceStrNatUnionSetCon (T : ArithmeticTheory) [𝐈Σ₁ ≼ T] [Theory.Δ₁ T] [ℕ↓[ℒₒᵣ] ⊧* T] :
                  ℕ↓[ℒₒᵣ] ⊧* T ∪ Theory.Con T