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 human-readable.
-- Scroll down to the {- PROOF -} section for the actual proof.

{- SYNTACTIC SUGAR -}

-- Contradictions are not true.
data Contradiction : Set where

-- 'A' is false if assuming 'A' leads to a contradiction.
_is-false : Set → Set
A is-false = A → Contradiction

-- syntax for writing contradictions
contradiction:_and_ : ∀ {A : Set} → 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 : Set) : Set 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 → Set) where

  -- We define the meaning of the sentences.
  _is-true : Statement → Set
  ∙      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 asserts: "if this sentence is true, then 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 : Set
  Machine-is-consistent = ∀ {S : Statement} → S is-printed → S is-true

  -- Complete means: "every true statement is printed"
  Machine-is-complete : Set
  Machine-is-complete = ∀ {S : Statement} → S is-true → S is-printed
  
  -- Theorem (Incompleteness). The machine is not both consistent and complete.
  Incompleteness: : (Machine-is-consistent and Machine-is-complete) is-false
  Incompleteness: (both printed-is-true and true-is-printed) = contradiction where
  -- Proof:
    -- 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:
        Göd-is-printed and                      -- it is printed
        printed-is-true (Göd-is-printed)        -- but by completeness, this means that it is true,
                                                -- which means it's not printed.

    -- Step 2. Yet 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, since it is not printed

    -- At this point, we have proved that there is a sentence which is true,
    -- but not printed.
    
    -- Step 3. So by completeness, the Gödel sentence it IS printed.
    Göd-is-printed : Gödel-sentence is-printed
    Göd-is-printed = true-is-printed (Göd-is-true) -- the Gödel sentence is printed, since it is true
                                                   -- and by completeness, true things are printed

    -- Step 4. Which is a contradiction.
    contradiction = contradiction:
      Göd-is-printed and
      Göd-is-not-printed
  -- Therefore, no machine is both consistent and complete.
  -- Qed.