Logicians are interested in proving results about the various logics that they have defined.  Such results are often called "meta-logical" results, as they are results about the logic in question.

One particular interesting meta-logical result is Gödel's first incompleteness result.  The theorem states that no consistent system of axioms whose theorems can be listed by an effective procedure is capable of proving all truths about the relations of the natural numbers (http://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems).  In other words, there is no computer program that can prove everything that is true about arithmetic.

The technique that Gödel developed to prove this result can also be used to prove that the halting problem is undecidable.  The halting problem (http://en.wikipedia.org/wiki/Halting_problem) is essentially the problem of deciding, given a program and an input, whether the program will eventually halt on this input or will run for ever, and Turing proved that the halting problem is not decidable

Yet another was of reformulating the problem is in terms of predicate logic:

There is no computer program that, for any set of propositions Γ and a proposition φ, will be able to determine whether φ follows from Γ or not.

In fact, predicate logic is semi-decidable: There is a computer program that will stop and say "yes" if φ actually follows from Γ, but there is no program that will say "no" if it does not.

To illustrate the problem (and note this is an illustration and not a proof), consider the following proposition:

A person is Jewish if their mother is Jewish.

Assuming that we do not know directly whether Sam is Jewish or not, we could try to determine Sam's Jewishness by figuring out whether Sam's mother is Jewish.  Again, assuming that we have no direct evidence to determine whether Sam' mother is Jewish, we could try to prove that the mother of Sam's mother is Jewish, and so on.  You see the problem.

Clearly, we are probably still interested in creating a computer program to automate reasoning in predicate logic, often referred to as an automated theorem prover for first-order predicate calculus, but we also want to make sure that the program does not run forever in the case that the proposition we want to prove does not follow.

The solution to this problem lies in the use of heuristics, rules-of-thumb that give the right answer in most cases, but that are not guaranteed to give the right answer in all cases.  The use of heuristics is prevalent in Artificial Intelligence, and one could argue that one of the reasons for the emergence of Artificial Intelligence is the fact that we are interested in finding solutions for problems for which we can prove that there are no solutions that are guaranteed to work, such as automated theorem provers for first order predicate calculus.

An example of a heuristic that we can use in our example above is to stop searching once we have applied the rule six times.  In other words, once we cannot directly determine that the mother of the mother of the mother of the mother of the mother of the mother of Sam is Jewish or not, we simply stop searching and assume that she was not Jewish, and we conclude that we cannot prove that Sam is Jewish.  You will see the problem: We would draw the wrong conclusion if there actually is information stretching back 10 generations along Sam's maternal lineage that the mother in question was Jewish.