But wouldn’t what Peano is capable of proving about your specific algorithm necessarily be “downstream” of the output of that algorithm itself? The Peano axioms are upstream, yes, but what Peano proves about a particular function depends on what that function is.
But wouldn’t what Peano is capable of proving about your specific algorithm necessarily be “downstream” of the output of that algorithm itself? The Peano axioms are upstream, yes, but what Peano proves about a particular function depends on what that function is.