Supporting results for pointwise provable equality.

Classification of the least composition congruence on program indices. Sigma-one soundness gives equality of denoted partial functions; otherwise the generated relation is universal. No effective presentation is required.

theorem PointwiseComposition.FailureOfComposition.ProgramIndices.extensional_implies_generated (A : Arithmetization) (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (e d : ℕ) (h : A.evaluation e = A.evaluation d) : GeneratedRel A T e d

theorem PointwiseComposition.FailureOfComposition.ProgramIndices.generated_iff_extensional_of_sound (A : Arithmetization) (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (hT : GeneratedCongruence.SigmaOneSound T) (e d : ℕ) : GeneratedRel A T e d ↔ A.evaluation e = A.evaluation d

theorem PointwiseComposition.FailureOfComposition.ProgramIndices.generated_universal_of_not_sound (A : Arithmetization) (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (hT : ¬GeneratedCongruence.SigmaOneSound T) (e d : ℕ) : GeneratedRel A T e d

theorem PointwiseComposition.FailureOfComposition.ProgramIndices.generated_congruence_classification (A : Arithmetization) (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] : (GeneratedCongruence.SigmaOneSound T → ∀ (e d : ℕ), GeneratedRel A T e d ↔ A.evaluation e = A.evaluation d) ∧ (¬GeneratedCongruence.SigmaOneSound T → ∀ (e d : ℕ), GeneratedRel A T e d)

The two cases of the generated-congruence theorem, with equality of actual partial-function denotations in the sound case.

theorem PointwiseComposition.FailureOfComposition.ProgramIndices.generated_iff_extensional_or_unsound (A : Arithmetization) (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (e d : ℕ) : GeneratedRel A T e d ↔ A.evaluation e = A.evaluation d ∨ ¬GeneratedCongruence.SigmaOneSound T

theorem PointwiseComposition.FailureOfComposition.ProgramIndices.generated_quotient_subsingleton_iff_not_sound (A : Arithmetization) (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] : Subsingleton (Quotient (generatedSetoid A T)) ↔ ¬GeneratedCongruence.SigmaOneSound T

The quotient by the generated congruence has exactly one element if and only if the ambient theory fails Sigma-one soundness.