ExtendedIncompletenessInQ0

// Define Computably Enumerable (aka recursively enumerable) predicates.
CESet : (Nat -> o) -> o
CESet := \p. exists f \in PRF2Set. p = (\n. exists m:Nat. 0 < f n m)

// Standard Model
  
interpT : (Nat -> Nat) -> Term -> Nat
interpT := \v. TermR_(Nat) v 0 (\t. S) (\t. \s. \n, \m. n + m) (\t. \s. \n. \m. n * m)

interpF : (Nat -> Nat) -> Formula -> o
interpF := \v. \f. FormulaR_((Nat -> Nat) -> o)
                     (\t. \s. \v. interpT v t = interpT v s)
                     (\v. F)
                     (\f. \g. \r. \s. \v. r v /\ s v)
                     (\f. \g. \r. \s. \v. r v => s v)
                     (\f. \n. \r. \s. \v. forall m \in NatSet. r (\x. if x = n then m else v x))

isTrue : Formula -> o
isTrue := \f. f \in FormulaSet /\ freeVarFormula f = empty /\ interpF (\x. x) f

// Statement of essential incompleteness of arithmetic
ExtendedEssentialIncompletenessOfRA : o
ExtendedEssentialIncompletenessOfRA := forall t : Theory. (t c= FormulaSet /\ RA c= proves t /\ (proves t) \in CESet) =>
  exists g \in FormulaSet. freeVarFormula g = empty /\
                           ((proves t g \/ proves t (not g)) => proves t = FormulaSet) /\
                           (~(isTrue g) => proves t = FormulaSet)

IncompletenessOfArithmeticInQ0

// Section: Primitive
// 'a' stands for any type

Q_a : a -> a -> o

iota : (i -> o) -> i

// Section: Logic

// Notation
A = B := Q A B

// Notation
A <=> B := Q_o A B

T : o
T := Q_o = Q_o

F : o
F := \x : o. T = \x : o. x

// Notation
forall x : a. A := (\x : a. T) = (\x : a. A)

// Notation
A /\ B := (\g : o -> o -> o. g T T) = (\g : o -> o -> o. g A B)

// Notation
A => B := A = (A /\ B)

// Notaton
~A := A = F

// Notation
A \/ B := ~(~A /\ ~B)

// Notation
exists x : a. A := ~(forall x : a. ~A)

// Notation
A =/= B := ~(A = B)

// Recursive Notation
iota x : i. A := iota (\x. A)
iota x : o. A := (\x. x) = (\x. A)
iota f : a -> b. A := \x : a. iota z : b. exists f : a -> b. A /\ f x = z

//Notation
if A then B else C := iota x. (A /\ x = B) \/ (~A /\ x = C)
  
// Section: sets / predicates

//Notation
A \in B := B A

//Notation
A \notin B := ~(A \in B)

//Notation
{A} := Q A

//Notation
A \intersect B := \x. x \in A /\ x \in B

//Notation
A \union B := \x. x \in B \/ x \in B

//Notation
A c= B := \x. x \in A => x \in B

//Notation
A \ B := A \intersect (\x. x \notin B)

//Notation (usually i occurs in A)
{ A | i <- B } := \x. exists i \in B. x = A

//Notation
forall x \in A. B := forall x. x \in A => B

//Notation
exists x \in A. B := exists x. x \in A /\ B

empty_a : a -> o
empty_a := \x. F

BigUnion_a : ((a -> o) -> o) -> a -> o
BigUnion_a := \p. \a. exists s \in p. a \in s

// Section: Natural numbers.

// Type defintion
Nat := (i -> o) -> o

0 : Nat
0 := Q (\x. F)

S : Nat -> Nat
S := \n. \p. exists x. p x /\ n (\y. y =/= x /\ p y)

NatSet : Nat -> o
NatSet := \n. forall p : Nat -> o. (p 0 /\ forall m : Nat. p m => p (S m)) => p n

R : (Nat -> Nat -> Nat) -> Nat -> Nat -> Nat
R := \h. \g. \n. iota m : Nat. forall w : Nat -> Nat -> o. (w 0 g /\ forall x : Nat. forall y : Nat. w x y => w (s x) (h x y)) => w n m

1 : Nat
1 := S 0

2 : Nat
2 := S 1

3 : Nat
3 := S 2

4 : Nat
4 := S 3

//Notation
A + B := R (\x. S) A B

//Notation
A * B := R (\x. \y. (A + y)) 0 B

triangle : Nat -> Nat
triangle := R (\x. \y. (S x) + y) 0

pair : Nat -> Nat -> Nat
pair := \n. \m. triangle (n + m) + m

//Notation
A <= B := exists n \in NatSet . A + n = B

//Notation
mu n. A := iota n : Nat. n \in NatSet /\ n \in A /\ forall m \in A. n <= m


// Section: Syntactic Logic

// Type defintion
Term := Nat

var : Nat -> Term
var := \n. 1 + 4*n

zero : Term
zero := 0

succ : Term -> Term
succ := \t. 1 + 4*t + 1

plus : Term -> Term -> Term
plus := \t. \s. 1 + 4*(pair t s) + 2

mult : Term -> Term -> Term
mult := \t. \s. 1 + 4*(pair t s) + 3

TermSet : Term -> o
TermSet := \t. forall p : Term -> o.
  ((forall n \in NatSet. p (var n)) /\
   p zero /\
   (forall t : Term. p t => p (succ t))
   (forall t : Term. forall s : Term. (p t /\ p s) => p (plus t s)) /\
   (forall t : Term. forall s : Term. (p t /\ p s) => p (mult t s))
  ) => p t

TermR_a : (Nat -> a) -> a -> (Term -> a -> a) -> (Term -> Term -> a -> a -> a) -> (Term -> Term -> a -> a -> a) -> Term -> a
TermR_a := \v. \z. \c. \p. \m. \r. iota x : a. forall w : Term -> a -> o.
 ((forall n \in NatSet. w (var n) (v n)) /\
  w zero z /\
  (forall t : Term. forall y : a. w t y => w (succ t) (c t y)) /\
  (forall t : Term. forall s : Term. forall y : a. forall z : a. (w t y /\ w s z) => w (plus t s) (p t s y z)) /\
  (forall t : Term. forall s : Term. forall y : a. forall z : a. (w t y /\ w s z) => w (mult t s) (m t s y z))
 ) => w r x
  
freeVarTerm : Term -> Nat -> o
freeVarTerm := TermR_(Nat -> o) (\n. {n}) empty (\t. \p. p) (\t. \s. \p. \q. p \union q) (\t. \s. \p. \q. p \union q)

subTerm : Term -> (Nat -> Term) -> Term
subTerm := \r. \l. TermR_(Term) l zero (\t. succ) (\t. \s. plus) (\t. \s. mult) r

at :: Nat -> Term -> Nat -> Term
at := \n. \t. \m. if m = n then t else (var m)

// Type definition
Formula := Nat

equal : Term -> Term -> Formula
equal := \t. \s. 1 + 4*(pair t s)

falsum : Formula
falsum := 0

conj : Formula -> Formula -> Formula
conj := \f. \g. 1 + 4*(pair f g) + 1

impl : Formula -> Formula -> Formula
impl := \f. \g. 1 + 4*(pair f g) + 2

all : Nat -> Formula -> Formula
all := \n. \f. 1 + 4*(pair n f) + 3

FormulaSet : Formula -> o
FormulaSet := \f. forall p : Formula -> o.
  ((forall t \in Term. forall s \in Term. p (equal t s)) /\
   p falsum /\
   (forall f : Formula. forall g : Formula. (p f /\ p g) => p (conj f g)) /\
   (forall f : Formula. forall g : Formula. (p f /\ p g) => p (impl f g)) /\
   (forall n \in NatSet. forall f : Formula. p f => p (all n f))
  ) => p f

not : Formula -> Formula
not := \f. impl f falsum

disj : Formula -> Formula -> Formula
disj := \f. \g. not (conj (not f) (not g))

iff : Formula -> Formula -> Formula
iff := \f. \g. conj (impl f g) (impl g f)

some : Nat -> Formula -> Formula
some := \n. \f. not (all n (not f))

FormulaR_a : (Term -> Term -> a) -> a -> (Formula -> Formula -> a -> a -> a) -> (Formula -> Formula -> a -> a -> a) -> (Formula -> Nat -> a -> a) -> Formula -> a
FormulaR_a := \e. \m. \c. \i. \l. \r. iota x : a. forall w : Formula -> a -> o.
   ((forall t \in TermSet. forall s \in TermSet. w (equal t s)) /\
    w falsum m /\
    (forall f : Formula. forall g : Formula. forall y : a. forall z : a. (w f y /\ w g z) => w (conj f g) (c f g y z)) /\
    (forall f : Formula. forall g : Formula. forall y : a. forall z : a. (w f y /\ w g z) => w (impl f g) (i f g y z)) /\
    (forall n \in NatSet. forall f : Formula. forall y : a. w f y => w (all n f) (l f n y))
   ) => w r x

freeVarFormula : Formula -> Nat -> o
freeVarFormula := FormulaR_(Nat -> o) (\t. \s. freeVarTerm t \union freeVarTerm s) empty (\f. \g. \p. \q. p \union q) (\f. \g. \p. \q. p \union q) (\f. \n. \p. p \ {n})

fresh : (Nat -> o) -> Nat
fresh := \p. mu x. ~p x

subFormula : Formula -> (Nat -> Term) -> Formula
subFormula := FormulaR_((Nat -> Term) -> Formula)
   (\t. \s. \l. equal (subTerm t l) (subTerm s l))
   (\l. falsum)
   (\f. \g. \r. \s. \l. conj (r l) (s l))
   (\f. \g. \r. \s. \l. impl (r l) (s l))
   (\f. \n. \r. \l. (\z. all z (r (\m. if m = n then var z else l m))) (fresh (BigUnion {freeVarTerm (l i) | i <- freeVarFormula f})))

// Type definition
Theory := Formula -> o

// Close a set of formulas under universal generalization.
gen :: (Formula -> o) -> Theory
gen := \q. \f. forall p : Formula -> o. (q c= p /\ (forall n \in NatSet. forall g : Formula. p g => p (all n g))) => p f

// Logical Axioms for syntactic formulas
LA : Theory
LA := gen (\f. (exists a \in FormulaSet. exists b \in FormulaSet. f = impl a (impl b a)) \/
               (exists a \in FormulaSet. exists b \in FormulaSet. exists c \in FormulaSet. f = impl (impl a (impl b c)) (impl (impl a b) (impl a c))) \/
               (exists a \in FormulaSet. exists b \in FormulaSet. f = impl (conj a b) a) \/
               (exists a \in FormulaSet. exists b \in FormulaSet. f = impl (conj a b) b) \/
               (exists a \in FormulaSet. exists b \in FormulaSet. f = impl a (impl b (conj a b))) \/
               (exists a \in FormulaSet. f = impl falsum a) \/
               (exists a \in FormulaSet. exists b \in FormulaSet. f = impl (impl (impl a b) a) a) \/
               (exists n \in NatSet. exists. a \in FormulaSet. exists t \in TermSet. f = impl (all n a) (subFormula a (at n t))) \/
               (exists n \in NatSet. exists. a \in FormulaSet. exists b \in FormulaSet. f = impl (all n (impl a b)) (impl (all n a) (all n b))) \/
               (exists n \in NatSet. exists. a \in FormulaSet. n \notin freeVarFormula a /\ f = impl a (all n a)) \/
               (exists n \in NatSet. f = equal (var n) (var n)) \/
               (exists n \in NatSet. exists m \in NatSet. exists z \in NatSet. exists a \in FormulaSet.
                     f = impl (equal (var n) (var m)) (impl (subFormula a (at z (var n))) (subFormula a (at z (var m))))))


// Close a set of formulas under modus ponens
proves : Theory -> Formula -> o
proves := \t. \f. forall p : Formula -> o. (t c= p /\ LA c= p /\ (forall f : Formula. forall g : Formula. (p f /\ p (impl f g)) => p g)) => p f

// Section Goedel

// Axioms of Robinson Arithmetic
RA : Theory
RA := \f. f = all 0 (not (equal (succ (var 0)) zero)) \/
          f = all 0 (all 1 (impl (equal (succ (var 0)) (succ (var 1))) (equal (var 0) (var 1)))) \/
          f = all 0 (or (equal (var 0) zero) (some 1 (equal (var 0) (succ (var 1)))))
          f = all 0 (equal (plus (var 0) zero) (var 0)) \/
          f = all 0 (all 1 (equal (plus (var 0) (succ (var 1))) (succ (plus (var 0) (var 1))))) \/
          f = all 0 (equal (mult (var 0) zero) zero) \/
          f = all 0 (all 1 (equal (mult (var 0) (succ (var 1))) (plus (mult (var 0) (var 1)) (var 0))))

natToTerm : Nat -> Term
natToTerm := R (\x. succ) zero

codeTerm : Term -> Nat
codeTerm : TermR_(Nat) (\n. 1 + 4*n) 0 (\t. \n. 1 + 4*n + 1) (\t. \s. \n. \m. 1 + 4*(pair n m) + 2) (\t. \s. \n. \m. 1 + 4*(pair n m) + 3)

codeFormula : Formula -> Nat
codeFormula : FormulaR_(Nat) (\t. \s. 1 + 4*(pair (codeTerm t) (codeTerm s))) 0 (\f. \g. \n. \m. 1 + 4*(pair n m) + 1) (\f. \g. \n. \m. 1 + 4*(pair n m) + 2) (\f. \n. \m. 1 + 4*(pair n m) + 3)

quotF : Formula -> Term
quotF := \f. natToTerm (codeFormula f)

expressableF : (Formula -> o) -> Theory -> o
expressableF := \p. \t. exists n \in NatSet. exists f \in FormulaSet.
   {n} = freeVarFormula f /\
   (forall m \in p => proves t (subFormula f (at n (quotF m)))) /\
   (forall m \in Formula. m \notin p => proves t (not (subFormula f (at n (quotF m)))))

// Statement of the diagona lemma: https://en.wikipedia.org/wiki/Diagonal_lemma
diagonal_lemma : o
diagonal_lemma := forall t : Theory. (t c= FormulaSet /\ RA c= proves t) =>
                    forall n \in natSet. forall f \in FormulaSet. exists g \in FormulaSet.
		      freeVarFormula g = freeVarFormula f \ {n} /\
		         (proves t (iff g (subFormula f (at n (quotF g)))))

// Statement of essential incompleteness of (Robinsion) arithmetic
EssentialIncompletenessOfRA : o
EssentialIncompletenessOfRA := forall t : Theory. (t c= FormulaSet /\ RA c= proves t /\ expressibleF t t) =>
                                 exists g \in FormulaSet. freeVarFormula g = empty /\
                                   ((proves t g \/ proves t (not g)) => proves t = FormulaSet)

Primitive Recusive Functions

// We will make use of some object of type Nat that are not in NatSet

top : Nat
top := \p : (i -> o). T

bottom : Nat
bottom := \p : (i -> o). F

// Lists of natural numbers are countable, so we code them with natural numbers.

// Type Definition
ListNat := nat

nil : ListNat
nil := 0

cons : Nat -> ListNat -> ListNat
cons := \x. \l. 1 + pair x l

ListNatSet : ListNat -> o
ListNatSet := \l. forall p : ListNat -> o. (p nil /\ forall n \in NatSet. forall k. p k => p (cons n k)) => p l

ListNatR_a : a -> (Nat -> ListNat -> a -> a) -> ListNat -> a
ListNatR_a := \n. \c. \r. iota x : a. forall w : ListNat -> a -> o.
  (w nil n /\
   (forall n \n NatSet. forall l : ListNat. forall y : a. w l y => w (cons n l) (c n l y))
  ) => w r x

length : ListNat -> Nat
length := ListNatR_(Nat) 0 (\h. \t. S)

// Returns an error, represted by bottom, when passed nil
head : ListNat -> Nat
head := if (nil=l) then bottom else iota h : Nat. exists t \in ListNatSet. (cons h t)=l

// Returns an error, represted by bottom, when passed nil
tail : ListNat -> ListNat
tail := if (nil=l) then bottom else iota t : ListNat. exists h \in NatSet. (cons h t)=l

allList : (Nat -> o) -> ListNat -> o
allList := \p. ListNatR_o T (\n. \l. \r. p n /\ r)

lookup : ListNat -> Nat -> Nat
lookup := ListNatR_(Nat -> Nat) (\n. bottom) (\h. \t. \r. \n. R (\m. \z. r m) h)

// A type for primitive recursive programs (source code)
// The number of primitive recursive programs is countable, so we will represent them with natural numbers.

// Type Definition
PrimRecProg := Nat

// Type Definition
ListPrimRecProg := ListNat

// the program that takes no input and outputs 0
zeroP : PrimRecProg
zeroP := 0

// the program that takes one input and outputs the successor of the input
succP : PrimRecProg
succP := 1

// the program that takes n inputs and returns the kth input.
piP : Nat -> Nat -> PrimRecProg
piP := \n. \k. 2 + 3*(pair n k)

// the composition of m programs each taking n inputs and with program taking m inputs to make a program that takes n inputs.
composeP : PrimRecProg -> ListPrimRecProg -> PrimRecProg
composeP := \p. \lp. 2 + 3*(pair n lp) + 1

// the combinition of one program taking n inputs (base case), f, and
// a second programming taking n + 2 inputs (recurive case), g, and
// combining them by primitive recursion to make a program, h, that takes n + 1 inputs.
// where h(0,x1,x2...xn) = f(x1,x2...xn) and h(S n,x1,x2...xn) = g(n,h(n,x1,x2...xn),x1,x2...xn)
primRecP : PrimRecProg -> PrimRecProg -> PrimRecProg
primRecP := \f. \g. 2 + 3*(pair f g) + 2

// Not all programs are well defined.  The combinators have to take the programs that have the correct number of parameters and such.
// Here we define the set of well formed programs accepting n inputs.

primRecProgSet : Nat -> PrimRecProg -> o
primRecProgSet := \n. \p. forall (w : Nat -> PrimRecProg -> o).
  (w 0 zeroP /\
   w 1 succP /\
   (forall n \in NatSet. forall k \in NatSet. k < n.  w n (pi n k)) /\
   (forall n \in NatSet. forall m \in NatSet. forall q : PrimRecProg. forall qs : ListPrimRecProg. (w m q /\ allList (w n) qs) => w n (composeP q qs)) /\
   (forall n \in NatSet. forall f : PrimRecProg. forall g : PrimRecProg. (w n f /\ w (S (S n)) g) => w (S n) (primRecP f g))
  ) => w n p

//Now we give semantics to primitive recursive programs by writing an interpreter for them.
//This intepreter needs to produce functions that take n arguments for various n, but we cannot write this directly in Q0.
//We cheat by writing functions that operate on ListNat and expect n elements in the list.
//We make note of the arity of the function by returning the arity when passed the value "top" which is of type Nat, but isn't a member of NatSet.

interpret : PrimRecProg -> ListNat -> Nat
interpret := \p. \a. if (a = top) then (iota r : Nat. primRecProgSet r p) else (iota r : List -> Nat.
  forall w : PrimRecProg -> (List -> Nat) -> o.
    (w zeroP (\l. 0) /\
     w succP (\l. S (head l)) /\
     (forall n \in NatSet. forall k \in NatSet. k < n => w (piP n k) (\l. lookup l k)) /\
     (forall n \in NatSet. forall m \in NatSet. forall q \in primRecProgSet m. forall iq : ListNat -> Nat.
        forall qs : ListPrimRecProg. forall iqs : ListNat -> ListNat.
        (forall i \in NatSet. i < length qs => lookup qs i \in primRecProgSet n) =>
        (w q iq /\ (forall i \in NatSet. i < length qs => w (lookup qs i) (\l. lookup (iqs l) i))) =>
           w (composeP q qs) (\l. iq (iqs l))) /\
     (forall n \in NatSet. forall f \in primRecProgSet n. forall if : ListNat -> Nat.
        forall g \in primRecProgSet (S (S n)). forall ig : ListNat -> Nat.
        (w f if /\ w g ig) => w (primRecP f g) (\l. R (\n. \z. g (cons n (cons z (tail l)))) (f (tail l)) (head l)))
    ) => w p r) l
    
// Now we can state what it means for every primitive recursive function to be reprenetable by an arithemetic formula.
PRFRepresentable : o
PRFReprsentable : forall n \in NatSet. forall p \in primRecProgSet n. exists f \in FormulaSet.
   (forall i \in NatSet. i \in freeVarFormula f => i < (S n)) /\
   (forall l \in ListNatSet. length l = n => forall y \in NatSet.
      (proves RA (substituteFormula f (\i. natToTerm (lookup (cons y l) i)))) <=> interpret p l=y)

// We can specialize the above general theorem to the case of Primitive Recursive Functions of 2 argumetns
PRF2Set : (nat -> nat -> nat) -> o
PRF2Set := \f. exists p \in primRecProgSet 2. forall x \in NatSet. forall y \in NatSet. interpret p (cons x (cons y nill)) = f x y.

// We can state as a corollary of PRFReprsentable that every member of PRF2Set is representable by an arithemetic formula.
PRF2Representable : o
PRF2Representable : forall f \in PRF2Set. exists f \in FormulaSet.
  (forall i \in NatSet. i \in freeVarFormula f => i < 3) /\
  (forall x \in NatSet. forall y \in NatSet. forall z \in NatSet.
    (proves RA (substituteFormula f (\i. natToTerm (if i=0 then z else if i=1 then x else if i=2 then y else 0)))) <=> f x y=z)