Supporting results for pointwise provable equality.

Characterization of congruence by Pi-one completeness.

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

For a consistent extension of PA, right composition is compatible exactly when every true Pi-one sentence is provable. No enumerability is assumed.

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

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

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

The four statements in the manuscript's characterization theorem.

theorem PointwiseComposition.FailureOfComposition.PiOneCharacterization.quotient_composition_exists_iff_congruence (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] : (∃ (C : Quotient (ProofSearch.pointwiseSetoid T) → Quotient (ProofSearch.pointwiseSetoid T) → Quotient (ProofSearch.pointwiseSetoid T)), ∀ (F G : ProofSearch.FunctionalGraph), C ⟦F⟧ ⟦G⟧ = ⟦ProofSearch.functionalComp F G⟧) ↔ CompositionCongruence T

theorem PointwiseComposition.FailureOfComposition.PiOneCharacterization.no_quotient_composition_iff_not_piOneComplete (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] [FFL.Entailment.Consistent T] : ProofSearch.NoQuotientComposition T ↔ ¬PiOneComplete T