Church's Theorem states that there is no algorithm that can decide, for an arbitrary sentence of first-order logic, whether that sentence is logically valid, answering in the negative the decision problem posed by David Hilbert known as the Entscheidungsproblem. Named for Alonzo Church, who proved it in 1936 using his own lambda calculus, essentially the same result was proved independently and almost simultaneously by Alan Turing using his newly defined Turing machines.
Facts
StatementThere is no algorithm that decides whether an arbitrary first-order sentence is logically valid. 1 Classification
Statement Form Connections
Has Statement Form
Entity-backed identity for the statement-form enum value this theorem already carries, resolved to a mathematics concept by an explicit value-to-entity map (phase 3 bucket conversion, docs\design_entity_backed_browse_buckets_20260928.md). The statement-form fact itself stays on the theorem unchanged.
Sources
1. Entscheidungsproblem (Wikipedia)
Negative answerQuote, Negative answer
A negative answer to the Entscheidungsproblem was then given by Alonzo Church
2. Entscheidungsproblem (Wikipedia)
A negative answer to the Entscheidungsproblem was given by Alonzo Church in 1935-36 (Church's theorem)View the Source Reader Challenges (0)
No disputes yet. Spotted an error or a better source? Open the first one.
Sign in to dispute this or suggest a correction.