Editing Entscheidungsproblem (section)

== Negative answer<!--'Church's theorem' redirects here--> ==
Before the question could be answered, the notion of "algorithm" had to be formally defined. This was done by [[Alonzo Church]] in 1935 with the concept of "effective calculability" based on his [[lambda calculus|λ-calculus]], and by Alan Turing the next year with his concept of [[Turing machine]]s. Turing immediately recognized that these are equivalent [[model of computation|models of computation]].

A negative answer to the {{lang|de|Entscheidungsproblem}} was then given by Alonzo Church in 1935–36 ('''Church's theorem'''<!--boldface per WP:R#PLA-->) and independently shortly thereafter by Alan Turing in 1936 ([[Turing's proof]]). Church proved that there is no [[computable function]] which decides, for two given λ-calculus expressions, whether they are equivalent or not. He relied heavily on earlier work by [[Stephen Cole Kleene|Stephen Kleene]]. Turing reduced the question of the existence of an 'algorithm' or 'general method' able to solve the {{lang|de|Entscheidungsproblem}} to the question of the existence of a 'general method' which decides whether any given Turing machine halts or not (the [[halting problem]]). If 'algorithm' is understood as meaning a method that can be represented as a Turing machine, and with the answer to the latter question negative (in general), the question about the existence of an algorithm for the {{lang|de|Entscheidungsproblem}} also must be negative (in general). In his 1936 paper, Turing says: "Corresponding to each computing machine 'it' we construct a formula 'Un(it)' and we show that, if there is a general method for determining whether 'Un(it)' is provable, then there is a general method for determining whether 'it' ever prints 0".

The work of both Church and Turing was heavily influenced by [[Kurt Gödel]]'s earlier work on his [[Gödel's incompleteness theorem|incompleteness theorem]], especially by the method of assigning numbers (a [[Gödel numbering]]) to logical formulas in order to reduce logic to arithmetic.

The ''{{lang|de|Entscheidungsproblem}}'' is related to [[Hilbert's tenth problem]], which asks for an [[algorithm]] to decide whether [[Diophantine equation]]s have a solution.  The non-existence of such an algorithm, established by the work of [[Yuri Matiyasevich]], [[Julia Robinson]], [[Martin Davis (mathematician)|Martin Davis]], and [[Hilary Putnam]], with the final piece of the proof in 1970, also implies a negative answer to the ''Entscheidungsproblem''.