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.