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
References 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. https://mathworld.wolfram.com/ChurchsTheorem.html

Subject classifications