Supporting results for pointwise provable equality.

Right compatibility forces every true Pi-one sentence to be provable. The witnesses search for PA proofs of the negation of the proposed sentence. Only PA standard soundness is used; no soundness or consistency of T is assumed.

theorem PointwiseComposition.FailureOfComposition.PiOneCharacterization.graph_noncongruence_of_true_unprovable_pi_one (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (σ : FFL.FirstOrder.ArithmeticSentence) (hσ : FFL.FirstOrder.Arithmetic.Hierarchy Π 1 σ) (htrue : ℕ↓[ℒₒᵣ] ⊧ σ) (hnot : T ⊬ σ) : ∃ (F : ProofSearch.Graph) (H : ProofSearch.Graph) (G : ProofSearch.Graph), ProofSearch.Functional F ∧ ProofSearch.Functional H ∧ ProofSearch.Functional G ∧ ProofSearch.Pointwise T F H ∧ ¬ProofSearch.Pointwise T (ProofSearch.comp F G) (ProofSearch.comp H G)

A true Pi-one sentence omitted by T gives functional graphs witnessing failure of right compatibility.

theorem PointwiseComposition.FailureOfComposition.PiOneCharacterization.rightCompatible_implies_piOneComplete (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (h : RightCompatible T) : PiOneComplete T

No consistency or effective presentation of T is needed for necessity.