This is the seventh part of a series developed through the Department of Philosophical Theology at the Institute of Lutheran Theology’s Christ School of Theology, exploring major results in modern logic and their significance for philosophical and systematic theology.
Once logic had become sufficiently exact to distinguish formal derivation from semantic consequence, and once Gödel had shown both the completeness of first-order logic and the incompleteness of sufficiently strong formal theories, another question became unavoidable: Which logical and mathematical problems can, in principle, be solved by a completely mechanical procedure? The question was not merely whether human beings happen to know an efficient method, nor whether some proof might be extremely difficult to discover. It concerned something considerably more fundamental. Is there, for a given class of problems, an effective procedure which, if followed correctly and for a finite number of steps, will always yield the right answer?
During the 1930s Alonzo Church and Alan Turing, working independently and by strikingly different routes, gave mathematically precise accounts of what such an effective procedure would amount to. Church employed the lambda calculus and the notion of recursive functions; Turing imagined what are now called Turing machines, highly idealized devices capable of manipulating symbols according to finitely specified rules. Although the formalisms differed, they identified the same class of functions. This convergence was sufficiently remarkable that the resulting conception came to be expressed in the Church–Turing thesis: everything that can be calculated by an effective mechanical procedure is computable by a Turing machine, or equivalently by one of the other standard formal models of computation.
The thesis is important partly because it is not itself a theorem in the ordinary sense. The informal notion of an effective procedure is not independently given as a mathematically defined object against which one can simply prove that Turing computability is extensionally equivalent. Rather, the thesis proposes that the mathematically exact notion captures the pretheoretical notion of mechanical calculability. Its strength arises from the convergence of many independently developed formal characterizations—Turing machines, recursive functions, lambda definability, register machines, and others—which all identify the same class of computable functions.
This matters because, once effective calculability had been formalized, one could ask with precision whether important logical problems were decidable. A decision procedure for a class of statements is an effective method which, for any statement in the class, eventually terminates and answers correctly either yes or no. Thus, if there were a decision procedure for first-order validity, one could feed any first-order sentence φ into the procedure and eventually receive the correct verdict:
φ is logically valid,
or
φ is not logically valid.
At first this hope did not appear unreasonable. After all, Gödel had proved first-order logic complete. If
⊨ φ,
then
⊢ φ.
Every logically valid first-order sentence therefore has a formal proof. One might consequently suppose that validity is mechanically decidable: enumerate possible proofs until a proof of φ is found. But this establishes only half of what a decision procedure would require. If φ is valid, proof search will eventually succeed; if φ is not valid, however, a blind search for a proof need never terminate. We would then have no general means of knowing whether the sentence lacked a proof or whether its proof simply had not yet appeared.
This distinction is the difference between being recursively enumerable and being decidable. A proof system may provide a method that eventually recognizes all the positive cases without providing a method that always settles both positive and negative cases. First-order validity has precisely this character. Valid sentences can be effectively enumerated because formal proofs can be mechanically checked and systematically generated. What Church and Turing showed, however, is that there is no algorithm that decides, for every first-order sentence, whether that sentence is logically valid.
This result answers negatively the famous Entscheidungsproblem associated with Hilbert and Ackermann. The hope had been for a general mechanical procedure by which questions of logical validity could be settled. Church and Turing showed that no such procedure exists for full first-order logic. The limitation here is therefore not one imposed by insufficient ingenuity, inadequate computing power, or the practical difficulty of extremely large calculations. There can be no algorithm of the stipulated kind at all.
Turing's route to this conclusion is especially instructive because it turns upon the possibility of machines representing the behavior of other machines. A Turing machine is an idealized computing device consisting, in its simplest description, of a potentially unbounded tape divided into cells, a read-write head, and a finite set of instructions determining what the machine does according to the symbol it encounters and its current state. Despite the austerity of this arrangement, Turing showed that machines of this type can represent any effectively calculable procedure.
More remarkably, he showed that there can be a universal machine capable of simulating any other Turing machine when given an appropriate description of that machine and its input. Once machines and their inputs can themselves be represented symbolically, however, questions about computation can be transformed into questions about the behavior of encoded machines. This makes possible one of the central results in the theory of computation: the undecidability of the halting problem.
Suppose we ask whether there is a machine H which, when given the description of any machine M together with an input w, always correctly determines whether M eventually halts when run on w. Symbolically, we may represent the hoped-for procedure as follows:
H(M, w) = YES
if M halts on w,
and
H(M, w) = NO
if M does not halt on w.
Turing showed that no such general machine can exist. The proof proceeds by constructing, from the hypothetical halting-decider H, another machine whose behavior becomes contradictory when it is given its own description as input. The exact construction matters, but the deeper lesson is already visible: once sufficiently rich systems can encode descriptions of their own operations, diagonal forms of self-reference again appear, much as they had in Gödel's incompleteness argument and in the semantic paradoxes that motivated Tarski.
The family resemblance among these results should not obscure their differences. Gödel's first incompleteness theorem says that sufficiently strong, consistent, effectively axiomatized formal systems contain statements that cannot be proved within those systems. Tarski's undefinability result establishes limitations upon defining truth for sufficiently expressive languages within those same languages. Church and Turing establish limitations upon algorithmic decision. These are distinct theorems with distinct conclusions, even though each reveals, from a different direction, that formalization does not culminate in a universal procedure by which every relevant question can mechanically be settled.
That distinction is particularly important in theology, where the phrase “limits of reason” can become so elastic that nearly any formal result is made to support nearly any desired theological conclusion. Church and Turing do not show that human reason is intrinsically incapable of knowing God, that faith begins where logic fails, that mystery lies beyond computation, or that theological truth transcends all formal representation. None of those claims follows from the mathematics. What the results establish is much more exact: there are rigorously specified classes of formal problems for which no general algorithmic decision procedure exists.
This precision is itself theologically useful, because theology has often been tempted both to overestimate and to underestimate what formal reasoning can do. On the one hand, one may imagine that if theological propositions are stated with sufficient logical precision, doctrinal questions could eventually become matters of mechanical derivation. On the other hand, one may react against formalization by claiming that theology, because it concerns divine mystery, lies fundamentally beyond logical treatment. The Church–Turing results support neither conclusion. They tell us instead that formal procedures have determinate powers and determinate limitations, which should be investigated rather than rhetorically exaggerated.
Suppose, for example, that a theological theory T is formalized in some sufficiently expressive language and that we ask whether a sentence φ follows from T. If the language is first-order, then by completeness,
T ⊨ φ if and only if T ⊢ φ.
This tells us something profound: semantic consequence and formal derivability coincide. But it does not follow that there is a single algorithm which, for every T and every φ, will always terminate and decide whether T ⊨ φ. Completeness guarantees the existence of proofs for consequences; undecidability denies a universal terminating decision method for every case. The difference is easy to overlook but essential to an adequate philosophy of logic.
The theological significance becomes clearer if we distinguish deduction from decision. A deductive system provides rules by which conclusions may be derived from premises. A decision procedure provides an effective method which determines, for every candidate case, whether the relevant relation holds. Theology can therefore profit enormously from formal deduction without supposing that all questions internal to a sufficiently expressive theological system will thereby become algorithmically decidable.
Consider a simple doctrinal reconstruction. Suppose T contains axioms concerning divine attributes, creaturely dependence, incarnation, or sacramental presence. The formal system may permit us to derive consequences not immediately obvious in the ordinary-language formulations. It may expose hidden inconsistency, clarify the scope of quantifiers, distinguish competing interpretations, or show that certain propositions follow only when additional assumptions are introduced. None of this requires the theological theory to possess a complete mechanical decision procedure.
Indeed, the absence of such a procedure may help us understand why formal reasoning and conceptual judgment remain distinct. Algorithms operate on formally specified structures according to explicit rules. But the construction of the formal representation itself—deciding what counts as a primitive term, which distinctions are semantically important, how a doctrine is to be interpreted, and whether a formal consequence corresponds to the intended theological claim—already requires judgments that are not supplied by the algorithm simply because the algorithm is formally impeccable.
Here again the preceding results in this series converge. Löwenheim–Skolem taught us that a theory may possess many nonisomorphic models. Compactness showed that local satisfiability does not necessarily secure the global structure one had intended. Tarski distinguished truth, satisfaction, object language, and metalanguage. Church and Turing now show that even where the syntax and semantics have been specified with extraordinary exactness, one cannot assume that every resulting question falls under a universal mechanical method of decision.
There is, consequently, a modest but important lesson for theological method. Formalization can sharpen theological reasoning without converting theology into computation. The theologian who uses formal logic responsibly should therefore ask not merely whether an argument has been symbolized, but what class of formal problem has been produced, what can be mechanically determined within that class, what can only be semi-decided or recursively enumerated, and what interpretive judgments preceded the formalization in the first place.
The result is neither a triumphalist rationalism nor an invocation of mystery against reason. It is a more discriminating account of reason itself. Church and Turing teach us that a mechanical procedure is a precisely characterizable thing and that, once characterized, its limitations can themselves be proved. Logic therefore acquires one of its most striking forms of self-knowledge: it can determine not merely what follows from what, but something about what no general calculating procedure can decide.
Why It Matters for Theology
Church and Turing leave philosophical theology with several durable lessons. First, formal derivability must be distinguished from algorithmic decidability. A system may have precise proof rules even though no general procedure can decide every relevant consequence question. Second, the absence of a decision procedure is not an invitation to irrationalism; it is itself a formally demonstrable limitation within a precisely defined domain. Third, theological formalization remains useful even when it does not yield mechanical settlement of every question, since formal systems can still clarify consequence relations, reveal inconsistency, distinguish interpretations, and expose hidden assumptions.
Finally, these results remind theology that formal methods do not eliminate judgment. Before any algorithm can operate, a language must be chosen, symbols interpreted, axioms selected, and the intended relation between the formal structure and theological reality specified. Computation begins only after much of the most important conceptual work has already been done.
The deeper lesson, then, is not that reason fails, but that reason comes to understand the forms of its own effectiveness. Church and Turing showed that there are questions which no universal mechanical procedure can decide, and in doing so they transformed the meaning of logical limitation. The limitation is not a retreat from rigor. It is one of rigor's greatest achievements.
Bibliographical Note
Alonzo Church's 1936 paper “An Unsolvable Problem of Elementary Number Theory” gave one of the first precise demonstrations that certain effectively posed problems are undecidable. Alan Turing's “On Computable Numbers, with an Application to the Entscheidungsproblem,” published in 1936–1937, introduced the machine model now bearing his name and established the undecidability of central computational problems. For the historical background, Hilbert and Ackermann's formulation of the Entscheidungsproblem remains important, while modern introductions to computability theory ordinarily treat Turing machines, recursive functions, the Church–Turing thesis, the halting problem, and the undecidability of first-order validity together.
No comments:
Post a Comment