Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
// 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)
// 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)
// 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)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.