Supporting results for pointwise provable equality.
Productiveness supplies a true unprovable divergence sentence. Searching for PA proofs of its halting counterpart gives a Delta-one witness predicate. Internal Sigma-one completeness connects absence of those proofs to divergence. This proof does not invoke the second incompleteness theorem. The proof-search witnesses are a variant of v36's direct computation search.
theorem
PointwiseComposition.FailureOfComposition.graph_noncongruence_of_unprovable_divergence
(T : FFL.FirstOrder.ArithmeticTheory)
[𝐏𝐀 ≼ T]
(hex : ∃ (d : ℕ), ¬diagonalHalts d ∧ T ⊬ ∼diagonalHaltingFormula/[↑d])
:
∃ (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)
theorem
PointwiseComposition.FailureOfComposition.graph_noncongruence_via_productiveness
(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)
theorem
PointwiseComposition.FailureOfComposition.pa_graph_noncongruence_via_productiveness :
∃ (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_of_re_theorem_codes
(T : FFL.FirstOrder.ArithmeticTheory)
[FFL.Entailment.Consistent T]
[𝐏𝐀 ≼ T]
(hT : REPred (TheoremCodes T))
:
R.e. is stated directly for the complete theorem-code set. This theorem has no Delta-one presentation or soundness assumption on T.