module SimpleIncompleteness where
-- Based on http://blog.plover.com/math/Gdl-Smullyan.html and cafe_anon's Coq proof.
-- The following section contains a bunch of declarations that make the proof more human-readable.
-- Scroll down to the {- PROOF -} section for the actual proof.
{- SYNTACTIC SUGAR -}
Proposition : Set₁
Proposition = Set
-- Contradictions are not provable from true assumptions.
data Contradiction : Proposition where
-- 'A' is false if assuming 'A' leads to a contradiction.
_is-false : Proposition → Proposition
A is-false = A → Contradiction
contradiction:_and_ : ∀ {A : Proposition} → A → A is-false → Contradiction
contradiction: a and ¬a = ¬a a
-- 'A and B' is true if both 'A' and 'B' are true
data _and_ (A B : Proposition) : Proposition where
both_and_ : A → B → A and B
{- PROOF -}
-- A valid Statement is either empty, or it starts with PR, N or P.
data Statement : Set where
∙ : Statement
P_ : Statement → Statement
N_ : Statement → Statement
PR_ : Statement → Statement
-- a followed-by b means the statements a and b written after each other
_followed-by_ : Statement → Statement → Statement
∙ followed-by b = b
(P a) followed-by b = P (a followed-by b)
(N a) followed-by b = N (a followed-by b)
(PR a) followed-by b = PR (a followed-by b)
-- The following applies to any machine that prints Statements.
module Machine (_is-printed : Statement → Proposition) where
-- We define the meaning of the sentences.
_is-true : Statement → Proposition
∙ is-true = ∙ is-printed -- a ∙ does not mean anything by itself
(P *) is-true = * is-printed
(N *) is-true = (* is-true) is-false
(PR *) is-true = (* followed-by *) is-printed
-- The Gödel sentence is true if and only if it is not printed
Gödel-sentence : Statement
Gödel-sentence = N PR N PR ∙
-- Consistent means: "every printed statement is true"
Machine-is-consistent : Proposition
Machine-is-consistent = ∀ {S : Statement} → S is-printed → S is-true
-- Complete means: "every true statement is printed"
Machine-is-complete : Proposition
Machine-is-complete = ∀ {S : Statement} → S is-true → S is-printed
-- Theorem (Incompleteness): No machine is both consistent and complete.
Incompleteness: : (Machine-is-consistent and Machine-is-complete) is-false
-- Proof.
Incompleteness: (both printed-is-true and true-is-printed) = contradiction where
-- We assume for a contradiction that there is a machine that is both consistent and complete.
-- Step 1. The Gödel sentence is not printed.
Göd-is-not-printed : (Gödel-sentence is-printed) is-false
Göd-is-not-printed = λ Göd-is-printed → -- assuming that the Gödel sentence is printed
contradiction: -- leads to a contradiction since
Göd-is-printed and -- printed things are true (by consistency)
printed-is-true (Göd-is-printed) -- but if the Gödel sentence is true
-- then it is not printed
-- Step 2. The Gödel sentence is true.
Göd-is-true : Gödel-sentence is-true
Göd-is-true = Göd-is-not-printed -- the Gödel sentence is true if and only if
-- it is not printed, and we just proved
-- that it is not printed (Step 1).
-- At this point, we have proved that there is a sentence which is true,
-- but not printed. This contradicts completeness.
-- Step 3. By completeness, every true sentence (incl. the Gödel sentence) IS printed.
Göd-is-printed : Gödel-sentence is-printed
Göd-is-printed = true-is-printed (Göd-is-true)
-- Step 4. Which is a contradiction.
contradiction = contradiction: Göd-is-printed and Göd-is-not-printed
-- Therefore, our assumption must have been false. No machine is both consistent and complete.
-- Qed.