Mind, Matter, and Meaning

Alonzo Church

Alonzo Church (1903–1995) was an American logician and mathematician whose work helped establish computability theory. His lambda calculus, undecidability results, and theory of types provide formal tools for analyzing functions, proof, and effective procedures. His contributions distinguish questions that have algorithms from questions for which no general algorithm exists; they do not by themselves establish a theory of mind.

Major Works

  • “An Unsolvable Problem of Elementary Number Theory” (1936) — effective calculability, lambda-definability, and an unsolvable problem.
  • “A Note on the Entscheidungsproblem” (1936) — the absence of a general decision procedure for first-order validity.
  • “A Formulation of the Simple Theory of Types” (1940) — a typed logical calculus.

Lambda Calculus

The lambda calculus represents abstraction and application of functions through a small formal vocabulary. The expression `λx.x` is the identity function; applying it to an expression returns that expression. More complex expressions can encode numbers and operations, and reduction rules explain how applications are evaluated.

The untyped calculus does not guarantee that every expression reaches a final result. Nonterminating reductions are possible. Its computational importance lies in the functions it can represent and compute, not a promise that all computations finish. Typed versions place constraints on admissible expressions and serve additional logical purposes.

Lambda-definable functions, general recursive functions, and Turing-computable functions coincide in the relevant mathematical sense. Equivalence between these formal systems can be proved. It supplies evidence for the claim that they capture effective computation, but that further claim connects formal definitions with an initially informal notion.

The Church–Turing Thesis

The Church–Turing thesis identifies effectively calculable functions with the functions computable by a Turing machine, equivalently by the other standard formalisms. “Effective” concerns a finite, precisely specified, step-by-step method executable without ingenuity at each step. Its original analysis concerns idealized calculation, not every possible process that can occur in nature.

The thesis is not just the proved equivalence of lambda calculus and Turing machines. The informal notion of an effective procedure is not itself one of the formal systems between which equivalence is demonstrated. Arguments for the thesis include the convergence of independently motivated formalisms and analyses of what mechanical calculation requires.

Descriptions of it as either “merely a conjecture with no support” or “a theorem proving all physical processes computable” miss this distinction. It has extensive mathematical and conceptual support within its intended domain. Broader claims require further assumptions.

Church’s Theorem and the Entscheidungsproblem

Hilbert’s Entscheidungsproblem asks for a general effective procedure deciding logical validity. Church showed that there is no such procedure for arbitrary first-order formulas. Turing’s independent work arrived at a related negative result through a different formal analysis.

Undecidability does not mean that no first-order statements can be decided, that proofs cannot be checked, or that first-order logic lacks useful automated procedures. It means there is no algorithm that always finishes and correctly decides validity for every input formula. Validities can still be effectively enumerated, and restricted fragments can be decidable.

Nor is undecidability the same as computational expense. An algorithm can exist but be infeasible for large inputs; an undecidable problem admits no total decision algorithm of the required kind. Church’s result concerns the latter boundary.

Types and Logical Structure

Church’s 1940 simple theory of types combines a hierarchy of types with lambda abstraction. Types distinguish kinds of expressions and restrict their combinations, avoiding unrestricted self-application and other constructions that create problems in untyped logical systems. This contribution matters to higher-order logic and formal reasoning as well as programming-language theory.

The typed logical project should not be conflated with the untyped calculus used in characterizing general computability. Related notation can serve different theoretical purposes.

Later Strengthenings and Disputes

A physical Church–Turing thesis concerns what physically realizable devices can compute. The extended Church–Turing thesis concerns efficient simulation and computational complexity. A Church–Turing–Deutsch principle concerns universal computation in a physical theory. Authors formulate these proposals differently, and the labels “strong” and “physical” are not uniform.

Quantum computation bears directly on efficiency claims and the physical modeling of computation. Standard quantum computation does not straightforwardly refute the original thesis about effectively calculable functions. Proposals for hypercomputation instead examine whether some nonstandard physical resources could exceed Turing computability; their physical availability is disputed.

Computation and Mind

A theory identifying mental activity with computation needs an account of which physical processes implement a computation, what representational content they carry, and which organization suffices for cognition or consciousness. Church’s formal results do not answer those questions. They also do not show that artificial systems cannot have minds.

The distinction between simulating and realizing a process likewise needs substantive criteria. A mathematical description’s computability does not automatically settle which properties its implementation shares with the described system. These are philosophical and scientific extensions of computability theory, not conclusions contained in Church’s theorem.

Further Reading

  • Church, Alonzo. “An Unsolvable Problem of Elementary Number Theory.” American Journal of Mathematics 58 (1936): 345–363.
  • Church, Alonzo. “A Note on the Entscheidungsproblem.” The Journal of Symbolic Logic 1 (1936): 40–41.
  • Church, Alonzo. “A Formulation of the Simple Theory of Types.” The Journal of Symbolic Logic 5 (1940): 56–68.
  • Copeland, B. Jack. “The Church–Turing Thesis.” Stanford Encyclopedia of Philosophy. Substantive revision 2023.
  • Mind, Matter, and Meaning — Gordon Swobe’s book-length argument about mind, consciousness, and meaning; an author position, not an endorsement by this reference page or its subjects.