```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.

_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
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.