The Coq mailing list

[Ken Kubota <mail AT kenkubota.de>]

________________________________________________________________________________

SampleProofTheoremV by Russell O'Connor
________________________________________________________________________________

[In the following, all occurrences of "substitueFormula" were replaced by 
"substituteFormula".]


[...] formal proof of a statement like

(1)   forall R exists r forall x   PRR1(R) -> [ Rx -> [ proofB[Sb(r,u,Z(x))] 
] ]

but done in Q0 instead of informal mathematics.  However, to get us started 
we can just try proving a single instance of this more general theorem in Q0.

(2)  exists r forall x   PRR1([\x.x>1]) -> [ [\x.x>1]x -> [ 
proofB[Sb(r,u,Z(x))] ] ]

The sad bit is that this single instance is much much easier to prove 
directly than the general theorem is, so my proof of the single instance 
probably won't be too illuminating.

First, let me partially formalize statement (1) in Q0.

PRR1 : (Nat -> o) -> o
PRR1 := ... to be defined later ...

PR1isExpressible : o
PR1isExpressible
forall R : Nat -> o. PRR1(R) =>
 exists r \in FormulaSet. exists u \in Nat.
   forall x \in NatSet.
     (R x => proves RA (substituteFormula r (at u (natToTerm x)))) /\
     (~R x => proves RA (not (substituteFormula r (at u (natToTerm x)))))

(everything else should be defined [below])

The simpler instance is stated in Q0 as follows

GT1isExpressible : o
GT1isExpressible :=
 exists r \in FormulaSet. exists u \in Nat.
   forall x \in NatSet.
     (x > 1 => proves RA (substituteFormula r (at u x))) /\
     (~x > 1 => proves RA (not (substituteFormula r (at u (natToTerm x))))) /\

Unfortu[na]tely I've lopped off the PRR1 bit which is probably what 
inter[e]sted you, because now the proof is too easy.

Take r to be (some 1 (equal (var 0) (plus (var 1) (succ (succ zero)))))
Take u to be 0.
Let x be any value in NatSet.
We need to show that

(a) (x > 1) => proves RA (substituteFormula (some 1 (equal (var 0) (plus (var 
1) (succ (succ zero))))) (at 0 (natToTerm x))))
and
(b) ~(x < 1) => proves RA (not (substituteFormula (some 1 (equal (var 0) 
(plus (var 1) (succ (succ zero))))) (at 0 (natToTerm x))))

First thing I'd like to note is that we can use the definition of 
substituteFormula to prove that

(substituteFormula (some 1 (equal (var 0) (plus (var 1) (succ (succ zero))))) 
(at 0 (natToTerm x))))
=
(some 0 (equal (natToTerm x) (plus (var 0) (succ (succ zero)))))

I also need a lemma that says
(forall x \in NatSet. freeVarTerm (natToTerm x) = empty)

This reduces our goal to

(a) (x > 1) => proves RA (some 0 (equal (natToTerm x) (plus (var 0) (succ 
(succ zero)))))
and
(b) ~(x < 1) => proves RA (not (some 0 (equal (natToTerm x) (plus (var 0) 
(succ (succ zero))))))

Let's do (b) first because it is easier. We know x \in NatSet and that ~(x < 
1) holds.  So x = 0 or x = 1.

Suppose x = 0.  Then we have to prove
goal:  (proves RA (not (some 0 (equal (natToTerm 0) (plus (var 0) (succ (succ 
zero))))))

Using a lemma that natToTerm 0 = zero we can reduce this proving
goal:  (proves RA (not (some 0 (equal zero (plus (var 0) (succ (succ 
zero))))))

expanding the definition of some we get

goal:  (proves RA (not (not (all 0 (not (equal zero (plus (var 0) (succ (succ 
zero))))))))

Using a lemma that says that
forall f \in FormulaSet. (proves RA (not (not f)))=(proves RA f)

we can reduce this to showing

goal:  (proves RA (all 0 (not (equal zero (plus (var 0) (succ (succ 
zero))))))))

So we can reduce or goal to

goal:  (proves RA (not (equal zero (plus (var 0) (succ (succ zero)))))))

One of the formulas in LA is
all 1 (all 2 (impl (equal (var 1) (var 2))
   (impl (all 0 (not (equal zero (var 1))))
         (all 0 (not (equal zero (var 2)))))))

so we know that
(proves RA
 all 1 (all 2 (impl (equal (var 1) (var 2))
    (impl (all 0 (not (equal zero (var 1))))
          (all 0 (not (equal zero (var 2))))))))

from the universal instantiation lemma which says
forall f \in FormulaSet. forall n \in NatSet. forall t \in TermSet.
 proves RA (all n f) => proves RA (substituteFormula f (at n t))

we can conclude

(proves RA
 (impl (equal (succ (plus (var 0) (succ zero)))) (plus (var 0) (succ (succ 
zero))
   (impl (all 0 (not (equal zero (succ (plus (var 0) (succ zero)))
         (all 0 (not (equal zero (plus (var 0) (succ (succ zero)))

One of the axioms of RA is

(all 0 (all 1 (equal (plus (var 0) (succ (var 1))) (succ (plus (var 0) (var 
1))))))

So by using the universal [i]nstantiation theorem we get
(proves RA (equal (plus (var 0) (succ (succ zero))) (succ (plus (var 0) (succ 
zero))))

We have another lemma that says
forall t \in TermSet. forall s \in TermSet.  (proves RA (equal t s))=(proves 
RA (equal s t))

which lets us deduce that
(proves RA (equal (succ (plus (var 0) (succ zero))) (plus (var 0) (succ (succ 
zero)))))

So by the modus ponens closure property that defines proves, we can conclude 
that

(proves RA
   (impl (all 0 (not (equal zero (succ (plus (var 0) (succ zero)))
         (all 0 (not (equal zero (plus (var 0) (succ (succ zero))))

Another axiom of RA is
all 0 (not (equal (succ (var 0)) zero))

So that plus universal instantiation lets us show that

(proves RA (not (equal (succ (plus (var 0) (succ zero))) zero)))

And another lemma that says
forall t \in TermSet. forall s \in TermSet.  (proves RA (not (equal t 
s)))=(proves RA (not (equal s t)))

so we can conclude that

(proves RA  (not (equal zero (succ (plus (var 0) (succ zero))))))

Buy the universal gen[er]alization lemma we conclude

(proves RA (all 0 (not (equal zero (succ (plus (var 0) (succ zero)))))))


Using the modus ponens closure property that defines proves we can conclude 
t[ha]t

(proves RA
         (all 0 (not (equal zero (plus (var 0) (succ (succ zero))))

which was our goal.

[...]

I'll let you do the case where x = 1.

Now back to part (a)

goal: (x > 1) => proves RA (some 0 (equal (natToTerm x) (plus (var 0) (succ 
(succ zero)))))

Assuming that x > 1 that means there is some y \in NatSet such that
x = S (S y)

So this reduces our goal to

goal: proves RA (some 0 (equal (natToTerm (S (S y))) (plus (var 0) (succ 
(succ zero)))))

We can prove that (natToTerm (S (S y))) = succ (succ (natToTerm y)), so our 
goal is further reduced to

goal: proves RA (some 0 (equal (succ (succ (natToTerm y))) (plus (var 0) 
(succ (succ zero)))))

[...] the rest of the p[r]oof [...] to basical[l]y goes like this:

You can show

(proves RA (equal (succ (succ (natToTerm y))) (plus (natToTerm y) (succ (succ 
zero))))

and from this you can prove taht

(proves RA (some 0 (equal (succ (succ (natToTerm y))) (plus (var 0) (succ 
(succ zero)))))

which is the desired result.

At some point you have to use induction on 'y' to do these sorts of proofs, 
but you might be able to get away without induction here because we were 
lucky.

________________________________________________________________________________

ExtendedIncompletenessInQ0 by Russell O'Connor
________________________________________________________________________________

// 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)

________________________________________________________________________________

PrimitiveRecursiveFunctions by Russell O'Connor
________________________________________________________________________________

// 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, repres[en]ted 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, repres[en]ted 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 combin[a]tion of one program taking n inputs (base case), f, and
// a second programming taking n + 2 inputs (recur[s]ive 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 inte[r]preter 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 repre[se]n[ ]table by an arith[ ]metic formula.
PRFRepresentable : o
PRFRepr[e]sentable : 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 argume[nt]s
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 PRFRepr[e]sentable that every member of 
PRF2Set is representable by an arith[ ]metic 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)

________________________________________________________________________________

IncompletenessOfArithmeticInQ0 by Russell O'Connor
________________________________________________________________________________

// 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[l] 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 (Robins[ ]on) 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)

________________________________________________________________________________