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
In Branch
Source Wolfram MathWorld: Church's Theorem
Proved By
Source Entscheidungsproblem (Wikipedia)
Source Entscheidungsproblem (Wikipedia)
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)
Proved By: Alan Turing, Lead section
Such an algorithm was proven to be impossible by Alonzo Church and Alan Turing in 1936.
Proved By: Alonzo Church, Lead section
Such an algorithm was proven to be impossible by Alonzo Church and Alan Turing in 1936.
In Group: Computability and Complexity Theory, Lead section
Such an algorithm was proven to be impossible by Alonzo Church and Alan Turing in 1936.
Proved By: Alan Turing, Lead
Such an algorithm was proven to be impossible by Alonzo Church and Alan Turing in 1936.
View the SourceWolfram MathWorld: Church's Theorem
Wolfram MathWorldIn Branch: Logic and Foundations, Subject classificationsQuote, In Branch: Logic and Foundations, Subject classifications
Foundations of Mathematics Logic
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.