Documentation

LeanPool.PointwiseComposition.FailureOfComposition.PiOneIndexCharacterization

Supporting results for pointwise provable equality.

The Pi-one characterization at program indices. Realization transports the functional graph statements to every index in the given arithmetization; standard adequacy identifies graph equality with equality of partial functions. No effective presentation of the ambient theory is required.

source
def PointwiseComposition.FailureOfComposition.ProgramIndices.RightCompatible (A : Arithmetization) (T : FFL.FirstOrder.ArithmeticTheory) :
Prop

Right composition fixes the inner program and replaces the outer one.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def PointwiseComposition.FailureOfComposition.ProgramIndices.CompositionCongruence (A : Arithmetization) (T : FFL.FirstOrder.ArithmeticTheory) :
    Prop

    Composition respects pointwise equality in both arguments.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def PointwiseComposition.FailureOfComposition.ProgramIndices.ExtensionalIndex (A : Arithmetization) (e d : ℕ) :
      Prop

      The two programs denote the same standard partial function.

      Equations
      Instances For
        source
        def PointwiseComposition.FailureOfComposition.ProgramIndices.AgreesWithExtensional (A : Arithmetization) (T : FFL.FirstOrder.ArithmeticTheory) :
        Prop

        Pointwise provability coincides with equality of denoted partial functions.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem PointwiseComposition.FailureOfComposition.ProgramIndices.extensionalIndex_iff (A : Arithmetization) (e d : ℕ) :
          ExtensionalIndex A e d ↔ PiOneCharacterization.Extensional (A.graph e) (A.graph d)

          Adequacy turns equality of denotations into standard graph equality.

          source
          theorem PointwiseComposition.FailureOfComposition.ProgramIndices.rightCompatible_of_graph (A : Arithmetization) (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (h : PiOneCharacterization.RightCompatible T) :
          RightCompatible A T

          The composition graph equations transport compatibility to indices.

          source
          theorem PointwiseComposition.FailureOfComposition.ProgramIndices.rightCompatible_iff_graph (A : Arithmetization) (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] :
          RightCompatible A T ↔ PiOneCharacterization.RightCompatible T

          Realization makes compatibility at indices sufficient for all functional Sigma-one graphs.

          source
          theorem PointwiseComposition.FailureOfComposition.ProgramIndices.pointwiseIndex_comp_left (A : Arithmetization) (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (f g h : ℕ) (hgh : PointwiseIndex A T g h) :
          PointwiseIndex A T (A.compIndex f g) (A.compIndex f h)

          Left composition is compatible for every extension of PA.

          source
          theorem PointwiseComposition.FailureOfComposition.ProgramIndices.congruence_iff_rightCompatible (A : Arithmetization) (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] :
          CompositionCongruence A T ↔ RightCompatible A T

          Automatic left compatibility supplies the other argument of composition.

          source
          theorem PointwiseComposition.FailureOfComposition.ProgramIndices.compositionCongruence_iff_graph (A : Arithmetization) (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] :
          CompositionCongruence A T ↔ PiOneCharacterization.CompositionCongruence T

          The full composition property is unchanged by passing to indices.

          source
          theorem PointwiseComposition.FailureOfComposition.ProgramIndices.agreesWithExtensional_iff_graph (A : Arithmetization) (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] :
          AgreesWithExtensional A T ↔ PiOneCharacterization.AgreesWithExtensional T

          The graph and index formulations of agreement with extensional equality are equivalent; PA proofs of realization are used only via PA soundness.

          source
          theorem PointwiseComposition.FailureOfComposition.ProgramIndices.rightCompatible_iff_piOneComplete (A : Arithmetization) (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] [FFL.Entailment.Consistent T] :
          RightCompatible A T ↔ PiOneCharacterization.PiOneComplete T

          Right composition is compatible exactly for Pi-one complete theories.

          source
          theorem PointwiseComposition.FailureOfComposition.ProgramIndices.compositionCongruence_iff_piOneComplete (A : Arithmetization) (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] [FFL.Entailment.Consistent T] :
          CompositionCongruence A T ↔ PiOneCharacterization.PiOneComplete T

          Full composition congruence has the same Pi-one completeness criterion.

          source
          theorem PointwiseComposition.FailureOfComposition.ProgramIndices.agreesWithExtensional_iff_piOneComplete (A : Arithmetization) (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] [FFL.Entailment.Consistent T] :
          AgreesWithExtensional A T ↔ PiOneCharacterization.PiOneComplete T

          The fourth statement uses equality of actual partial-function denotations.

          source
          theorem PointwiseComposition.FailureOfComposition.ProgramIndices.pointwiseIndex_iff_evaluation_eq (A : Arithmetization) (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] [FFL.Entailment.Consistent T] (h : PiOneCharacterization.PiOneComplete T) (e d : ℕ) :
          PointwiseIndex A T e d ↔ A.evaluation e = A.evaluation d

          For a consistent Pi-one complete extension of PA, pointwise provability is exactly extensional equality of the interpreted programs.

          source
          theorem PointwiseComposition.FailureOfComposition.ProgramIndices.characterization (A : Arithmetization) (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] [FFL.Entailment.Consistent T] :
          (RightCompatible A T ↔ CompositionCongruence A T) ∧ (CompositionCongruence A T ↔ PiOneCharacterization.PiOneComplete T) ∧ (PiOneCharacterization.PiOneComplete T ↔ AgreesWithExtensional A T)

          All four manuscript statements, without an enumerability hypothesis.

          source
          theorem PointwiseComposition.FailureOfComposition.ProgramIndices.quotient_composition_exists_iff_congruence (A : Arithmetization) (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] :
          (∃ (C : Quotient (indexSetoid A T) → Quotient (indexSetoid A T) → Quotient (indexSetoid A T)), ∀ (e d : ℕ), C ⟦e⟧ ⟦d⟧ = ⟦A.compIndex e d⟧) ↔ CompositionCongruence A T

          An operation on the quotient inducing program composition exists exactly when the index relation is a composition congruence.

          source
          theorem PointwiseComposition.FailureOfComposition.ProgramIndices.no_index_quotient_iff_not_piOneComplete (A : Arithmetization) (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] [FFL.Entailment.Consistent T] :
          NoIndexQuotientComposition A T ↔ ¬PiOneCharacterization.PiOneComplete T

          The obstruction to quotient composition is precisely failure of Pi-one completeness, even for theories without an effective presentation.