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. (Author: /u/TezlaKoil. All rights reserved.)