Church's theorem and the decision problem

« ¸-definable, that is, not definable in the ¸-calculus, a logical calculus invented by Church ( Lambda calculus ). To conclude that the set of valid formulas in first-order logic is not 'effectively' decidable, we need two additional facts.

We need to equate validity in first-order logic with provability in a particular formal system, a result proved already by Gödel , but about which Church had some qualms due to the non-constructive nature of the proof.

We also need to equate the mathematical notion of ¸-definability (or the provably equivalent notions of recursiveness and Turing computability) with the intuitive notion of effective computability.

This second equality is Church's thesis ( Church's thesis ).

Assuming Church's thesis, Church's theorem constitutes a negative solution to the problem of giving a uniform procedure for deciding which formulas of first-order logic are valid. The particular version of first-order logic which Church used to prove his theorem included, as part of the language, the equality symbol, a constant and several function symbols.

However, such a rich vocabulary is not actually necessary.

Even first-order logic with a single dyadic predicate symbol is undecidable.

(This is in sharp contrast to the decidability of the special case where the language consists solely of monadic predicates, a result first proved by Löwenheim (1915 ).) Also, despite Church's qualms about the non-constructiveness of Gödel's completeness proof, Church's theorem is rather sturdy.

It is known that, for Gödel's completeness result to hold, one must allow formulas with non-recursive models to be considered to be satisfiable.

However, even if one restricts the possible models - for example, if one confines oneself to finite models or to constructive (recursive) models - the set of valid formulas remains non-recursive, and Church's theorem remains true, although first-order logic is no longer complete relative to these restricted classes of models. Hilbert's Entscheidungsproblem as formulated by Hilbert and Ackermann inquired about the decision problem for logic as such.

This would also include second-order logic, whose undecidability follows of course from that of the (weaker) first-order logic.

But here a slightly more complex situation prevails.

First-order logic, while not decidable, is none the less semi-decidable in that we do have a procedure to enumerate the set of all valid formulas.

What prevents first-order logic from being decidable is that we do not have a procedure to enumerate the complementary set of all formulas which are not valid, that is, of all formulas whose negations are satisfiable (have at least one true interpretation).

However, second-order logic is not even semi-decidable, a fact which is already implicit in Gödel's incompleteness result for arithmetic, and which pre-dated Church's theorem by about five years ( Gödel's theorems ).

Thus, at the time that Church proved his theorem, only the question for first-order logic was really open. Note that a positive solution to the Entscheidungsproblem would not have required a mathematical definition of effectiveness.

It would have sufficed to present a method for deciding which formulas of first-order logic were valid and to rely on our mathematical intuition to see that the method qualified as a genuine algorithm.

However, a. »