Human computing power: Can humans decide the halting problem on Turing Machines?

Question

We know the halting problem (on Turing Machines) is undecidable for Turing Machines. Is there some research into how well the human mind can deal with this problem, possibly aided by Turing Machines or general purpose computers?

Note: Obviously, in the strictest sense, you can always say no, because there are Turing Machines so large they couldn't even be read in the life span of a single human. But this is a nonsensical restriction that doesn't contribute to the actual question. So to make things even, we'd have to assume humans with an arbitrary life span.

So we could ask: Given a Turing Machine T represented in any suitable fashion, an arbitrarily long-lived human H and an arbitrary amount of buffer (i.e. paper + pens), can H decide whether T halts on the empty word?

---

Corollary: If the answer is yes, wouldn't this also settle if any computer has a chance of passing the turing-test?

Answer 1

It is very hard to define a human mind with a such mathematical rigor as it is possible to define a Turing machine. We still do not have a working model of a mouse brain however we have the hardware capable of simulating it. A mouse has around 4 million neurons in the cerebral cortex. A human being has 80-120 billion neurons (19-23 billion neocortical). Thus, you can imagine how much more research will need to be conducted in order to get a working model of a human mind.

You could argue that we only need to do top-down approach and do not need to understand individual workings of every neuron. In that case you might study some non-monotonic logic, abductive reasoning, decision theory, etc. When the new theories come, more exceptions and paradoxes occur. And it seems we are nowhere close to a working model of a human mind.

After taking propositional and then predicate calculus I asked my logic professor:
"Is there any logic that can define the whole set of human language?"
He said:
"How would you define the following?
To see a World in a grain of sand
And a Heaven in a wild flower,
Hold Infinity in the palm of your hand
And Eternity in an hour.
If you can do it, you will become famous."

There have been debates that a human mind might be equivalent to a Turing machine. However, a more interesting result would be for a human mind not to be Turing-equivalent, that it would give a rise to a definition of an algorithm that is not possibly computable by a Turing machine. Then the Church's thesis would not hold and there could possibly be a general algorithm that could solve a halting problem.

Until we understand more, you might find some insights in a branch of philosophy. However, no answer to your question is generally accepted.

http://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems#Minds_and_machines http://en.wikipedia.org/wiki/Mechanism_(philosophy)#G.C3.B6delian_arguments

Answer 2

I think there is no way how give a definitive answer to this question, as nobody really knows the capabilities of human mind (and I doubt anyone ever will).

But there is a view that gives one possible solution or explanation to this question:

When we're searching an oracle to solve the halting problem (or decide provability of first-order logical formulas etc.), we naturally want the oracle to be correct, it must not make any mistakes. But human mind isn't consistent, it makes mistakes. Nobody can honestly say that all statements (s)he believes are true are really true. This inconsistency can be viewed as the source of the power human mind has. Due to its inconsistency, it isn't subject of limitations that follow from the halting problem, Gödel's incompleteness theorem etc. We make mistakes, we mistakenly believe in false statements, and as our knowledge grows, we correct them (and of course find new false statements we believe in). On the other hand, we want all formalizations of the notion of algorithm or all logical calculi to be consistent, so that we can prove once and for all that they're free of such mistakes. And this makes them limited.

Answer 3

Consider this from a different perspective.

• First-order logic is undecidable, that is, there is no decision procedure that determines whether arbitrary formulas are logically valid. (But the set of true first-order formulas is semi-decidable, that is if a formula is true, it's possible to find a proof by an algorithm.)
• Proof assistants help prove theorems in first-order (or even higher-order) logic. The proof assistant ensures that the proof is done correctly and can even help resolve some cases. However, human interaction is require to guide the proof assistant to the correct answer.

Proof assistants could be used to prove properties of individual Turing machines.

Answer 4

Carl Mummert's comment nailed it.

1. My understanding (correct me if I am wrong) of the Church-Turing thesis is the idea that anything that can be computed can be computed by a Turing Machine.

2. And also, if a Turing Machine could compute if another Turing Machine would halt or not on an input (halting problem), then you could also compute if another Turing Machine would not halt on a given input (just swap yes for no, and no for yes!) - significant because then you could feed this Turing Machine to itself - would it not halt on itself on the input? If yes (not halting), then no (is halting??). If no, then yes. If yes, then no. If no, then ye... hmmm.

So, 2. shows it is impossible for a Turing Machine to solve the halting problem. But I don't think there is any clear evidence to contradict 1. at this time. Every model of computation known still can solve (decide) as much as a Turing Machine can.

The burden of proof seems to be on the person coming up with a new model of computation, which has more power (that is, can decide more problems) than the classical Turing Machine.

By the way, some great lectures on this can be found here.

Answer 5

There isn't any evidence that the human brain is in fact anything more than a Turing machine. In fact, it seems like the entire universe can be simulated on a (sufficiently large) Turing machine.

Humans are "smart" because of smart algorithms that are cleverly written in neurons so computer scientists can't steal or efficiently implement them. However clever these algorithms are, they most likely cannot reliably solve the halting problem.

Answer 6

as with DCs answer (and to expand on it somewhat) there is a strong sense in which this question (combination of human and computer in finding special-case solutions to the halting problem) is related to the field of ATP, automated theorem proving and the closely related computer assisted proofs. also it has long been known there is a strong correspondence between programs and proofs in the Curry-Howard correspondence. also related/similar to this is proving program termination (eg via loop invariants or loop variants). in fact there is a deep sense in which all of mathematics is about this problem, because virtually all mathematical statements can be converted to questions about specific programs on TMs halting or not halting. see eg [2] for some further info & lots of further refs on ATP etc.

[1] is a semifamous book on the subject that examines the question in detail, relating it to the possibility artificial intelligence. briefly Penrose's idea is that true AI must be impossible because humans can come up with proofs of undecidability such as Turings halting problem or Godels incompleteness proof, whereas computers could not due to the same phenomena.

[1] Emperors new mind by Penrose

[2] adventures & commotions in ATM, vzn

Answer 7

The other answers are talking about the complexities of the human mind, which seems to me to be irrelevant.

Is it OK to rephrase the question as the following?

I interpret the undecidability of the Halting Problem to imply that there exists a set of program-input pairs for which the program DOES halt and this property can only be discovered by unabbreviated execution. It also implies another set of program-input pairs for which the program DOES NOT halt and that this property cannot be computed.

Based on that interpretation, I wonder whether there are any pairs from either set which a human could statically analyze and know with 100% accuracy - or possibly even prove, if this "big picture" intuitive perspective is such an advantage - whether those programs halt or not.

Perhaps the interpretation is incorrect - it is how I imagine @bitmask is thinking.

Regarding assisted theorem provers, from what I've read of such provers, it's not that the algorithm needs human intuition exactly, it's just that the search space is so vast as to be impractical. The human just helps narrow the search space for choices for which we don't yet have good heuristics. But I have no experience in many of these matters. Perhaps someone can comment on this as well?