Documentation

LeanPool.PointwiseComposition.FailureOfComposition.CraigPresentation

Supporting results for pointwise provable equality.

A decidable presentation of an r.e. arithmetic theory. Each axiom is padded by a tautology carrying a PA derivation that its original code belongs to the represented axiom set. The derivation checker and syntax operations are provably Delta-one over IΣ1.

source
noncomputable def PointwiseComposition.FailureOfComposition.CraigPresentation.axiomFormula (T : FFL.FirstOrder.ArithmeticTheory) :
FFL.FirstOrder.ArithmeticSemisentence 1

The axiom Formula construction in FailureOfComposition.CraigPresentation.

Equations
Instances For
    source
    def PointwiseComposition.FailureOfComposition.CraigPresentation.padded (σ : FFL.FirstOrder.ArithmeticSentence) (d : ℕ) :
    FFL.FirstOrder.ArithmeticSentence

    The padded construction in FailureOfComposition.CraigPresentation.

    Equations
    Instances For
      source
      def PointwiseComposition.FailureOfComposition.CraigPresentation.padGraph :
      Σ₁.Semisentence 3

      The pad Graph construction in FailureOfComposition.CraigPresentation.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def PointwiseComposition.FailureOfComposition.CraigPresentation.checkSigma (T : FFL.FirstOrder.ArithmeticTheory) :
        Σ₁.Semisentence 2

        The check Sigma construction in FailureOfComposition.CraigPresentation.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          noncomputable def PointwiseComposition.FailureOfComposition.CraigPresentation.checkPi (T : FFL.FirstOrder.ArithmeticTheory) :
          Π₁.Semisentence 2

          The check Pi construction in FailureOfComposition.CraigPresentation.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            noncomputable def PointwiseComposition.FailureOfComposition.CraigPresentation.characteristic (T : FFL.FirstOrder.ArithmeticTheory) :
            ∆₁.Semisentence 1

            The characteristic construction in FailureOfComposition.CraigPresentation.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              theorem PointwiseComposition.FailureOfComposition.CraigPresentation.characteristic_proper {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (T : FFL.FirstOrder.ArithmeticTheory) :
              FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.ProperOn M (characteristic T)
              source
              def PointwiseComposition.FailureOfComposition.CraigPresentation.presentation (T : FFL.FirstOrder.ArithmeticTheory) :
              FFL.FirstOrder.ArithmeticTheory

              Axioms accompanied by numerical PA derivations of their membership in the represented r.e. axiom set. The padding carries the derivation code.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                theorem PointwiseComposition.FailureOfComposition.CraigPresentation.presentation_weaker (T : FFL.FirstOrder.ArithmeticTheory) (hT : REPred (AxiomCodes T)) :
                presentation T ≼ T

                Every padded axiom is provable in the original theory.

                source
                theorem PointwiseComposition.FailureOfComposition.CraigPresentation.original_weaker (T : FFL.FirstOrder.ArithmeticTheory) (hT : REPred (AxiomCodes T)) :
                T ≼ presentation T

                Every original axiom has a padded representative from which it follows.

                source
                theorem PointwiseComposition.FailureOfComposition.CraigPresentation.characteristic_mem_iff (T : FFL.FirstOrder.ArithmeticTheory) (hT : REPred (AxiomCodes T)) (φ : FFL.FirstOrder.Proposition ℒₒᵣ) :
                (FFL.FirstOrder.Semiformula.Evalb ![⌜φ⌝]) ↑(characteristic T) ↔ ∃ τ ∈ presentation T, φ = FFL.FirstOrder.Rewriting.emb τ
                source
                @[reducible, inline]
                noncomputable abbrev PointwiseComposition.FailureOfComposition.CraigPresentation.presentationDelta1 (T : FFL.FirstOrder.ArithmeticTheory) (hT : REPred (AxiomCodes T)) :
                FFL.FirstOrder.Theory.Δ₁ (presentation T)

                The padded presentation has a characteristic formula whose Sigma-one and Pi-one forms are provably equivalent in IΣ1.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  theorem PointwiseComposition.FailureOfComposition.CraigPresentation.exists_craig_presentation (T : FFL.FirstOrder.ArithmeticTheory) (hT : REPred (AxiomCodes T)) :
                  ∃ (S : FFL.FirstOrder.ArithmeticTheory), Nonempty (FFL.FirstOrder.Theory.Δ₁ S) ∧ S ≼ T ∧ T ≼ S

                  Every arithmetic theory with r.e. axiom codes has an equivalent Delta-one presentation. No soundness or consistency assumption on T is used.