Statement
"For every computer system, there is a sentence which is undecidable for the computer, but the human sees that it is true, therefore proving the sentence via some non-algorithmic method."
Thanks!
Statement
"For every computer system, there is a sentence which is undecidable for the computer, but the human sees that it is true, therefore proving the sentence via some non-algorithmic method."
Thanks!
The argument runs as follows:
Suppose there exists a Turing-machine $T$, such that $T$ stops on input $I$ if and only if $I$ is (the encoding of) a theorem, which can be proven by a human being. Then you can build a machine $T'$ such that $T'$ stops if and only if $T$ with input "$T'$ stops" does not stop. Since $T$ is correct, it cannot happen that $T$ stops for a false statement, hence $T'$ stops, and $T("T'\mbox{ stops}")$ does not. So we (human beings) have proven that $T'$ stops, but $T$ cannot prove this. Hence there are statements, provable by human beings, which are not provable by Turing machines.
The mistake in this argument is that we not only assume that $T$ has the desired property, but also that we know that $T$ has these properties. To show that $T'$ stops, we have to know that $T$ is correct. But if the correctness of $T$ relies on an unprovable but true statement, then we cannot prove that $T'$ stops.
The moral of this fallacy is that if you talk about computability, you have to be extremely precise. "Problem X is not decidable" is useful as a mnemonic, but not sufficient for a statement. For example it is well known that the solvability of diophantine equations is not decidable. Still, for every diophantine equation one of the algorithms Print "solvable" or Print "unsolvable" gives the correct answer. So just as above with the machine $T$, there is an algorithm, but we cannot prove that it is correct.
Real world examples, where lack of precision leads to confusion are e.g. the difference between König's Lemma and Weak König's Lemma, or the statement that the Cayleygraph of a weakly convex group is computable.