Church's Theorem

Church proved several important theorems that now go by the name Church's theorem.

One of Church's theorems states that there is no consistent decidable extension of Peano arithmetic (Wolf 2005).

Church (1936) also proved that the set of first-order tautologies with at least one at least binary predicate or at least two at least unary function symbols is not recursive.

See also

Church-Rosser Theorem, Church-Turing Thesis, Decision Problem

Portions of this entry contributed by Marcin Mostowski

Explore with Wolfram|Alpha


Church, A. "A Note on the Entscheidungsproblem." J. Symb. Logic 1, 40-41, 1936.Church, A. Introduction to Mathematical Logic. Princeton, NJ: Princeton University Press, 1996.Wolf, R. S. A Tour Through Mathematical Logic. Washington, DC: Math. Assoc. Amer., p. 146, 2005.

Referenced on Wolfram|Alpha

Church's Theorem

Cite this as:

Mostowski, Marcin and Weisstein, Eric W. "Church's Theorem." From MathWorld--A Wolfram Web Resource.

Subject classifications