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 Sources
1. Entscheidungsproblem (Wikipedia)
Negative answerQuote, Negative answer
A negative answer to the Entscheidungsproblem was then given by Alonzo Church
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.