Supporting results for pointwise provable equality.

Graph witnesses for the second-incompleteness obstruction.

theorem PointwiseComposition.FailureOfComposition.proofBot_consistency_bridge (T : FFL.FirstOrder.ArithmeticTheory) [FFL.FirstOrder.Theory.Δ₁ T] : 𝐏𝐀 ⊢ ∀¹ ∼↑(FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.sigma (ProofSearch.proofTarget T ⊥))/[FFL.FirstOrder.Semiterm.bvar 0] ⇔ₗ ↑(FFL.FirstOrder.Theory.consistent T)/[]

theorem PointwiseComposition.FailureOfComposition.numeral_nonproof_of_consistency (T : FFL.FirstOrder.ArithmeticTheory) [FFL.FirstOrder.Theory.Δ₁ T] [FFL.Entailment.Consistent T] (n : ℕ) : 𝐏𝐀 ⊢ ↑(ProofSearch.notProofTarget T ⊥)/[↑n]

theorem PointwiseComposition.FailureOfComposition.graph_noncongruence_via_godel (T : FFL.FirstOrder.ArithmeticTheory) [FFL.FirstOrder.Theory.Δ₁ T] [FFL.Entailment.Consistent T] [𝐏𝐀 ≼ T] : ∃ (F : ProofSearch.Graph) (I : ProofSearch.Graph) (G : ProofSearch.Graph), ProofSearch.Functional F ∧ ProofSearch.Functional I ∧ ProofSearch.Functional G ∧ ProofSearch.Pointwise T F I ∧ ¬ProofSearch.Pointwise T (ProofSearch.comp F G) (ProofSearch.comp I G)

The second-incompleteness route to noncongruence for functional graphs.

theorem PointwiseComposition.FailureOfComposition.pa_graph_noncongruence_via_godel : ∃ (F : ProofSearch.Graph) (I : ProofSearch.Graph) (G : ProofSearch.Graph), ProofSearch.Functional F ∧ ProofSearch.Functional I ∧ ProofSearch.Functional G ∧ ProofSearch.Pointwise 𝐏𝐀 F I ∧ ¬ProofSearch.Pointwise 𝐏𝐀 (ProofSearch.comp F G) (ProofSearch.comp I G)

theorem PointwiseComposition.FailureOfComposition.no_graph_quotient_composition_via_godel (T : FFL.FirstOrder.ArithmeticTheory) [FFL.FirstOrder.Theory.Δ₁ T] [FFL.Entailment.Consistent T] [𝐏𝐀 ≼ T] : ProofSearch.NoQuotientComposition T