I have some error: from the below it follows that if the formal system found is distinct from the original one then it’s provable that the input algorithm does not halt (if it halts, it’s provable that it halts in Peano arithmetic)…

read more