Re:A Formal Proof of Complexity Bounds on Diophantine Equations
by marcodavid on Saturday May 24, 2025 @06:22PM
(#44084141)
An even crazier consequence was pointed out by J.P. Jones in 1982. He explained:
"Via Gödel numbering, the theorems of an axiomatizable theory T become in effect an recursively enumerable set. The search for proofs becomes the search for solutions of a Diophantine equation. [...]
"Theorem. For any axiomatizable theory T and any proposition P, if P has a proof in T, then P has another proof consisting of 100 additions and multiplications of integers."
"Via Gödel numbering, the theorems of an axiomatizable theory T become in effect an recursively enumerable set. The search for proofs becomes the search for solutions of a Diophantine equation. [...]
"Theorem. For any axiomatizable theory T and any proposition P, if P has a proof in T, then P has another proof consisting of 100 additions and multiplications of integers."
See https://www.jstor.org/stable/2273588