@DavidReed I think I need to read through it many times. Like many number theory proofs, this one once again stuff in an integral and then somehow showed that it violate an ineuquality. I never understood how all this magic works because all the steps of the motivations are so mysterious

@famesyasd Basically, let S = { g : n in nat and g in func({0..n},A) and g(0) = c and forall k in {1..n} ( g(k) = F(g(k−1)) ) }. Then prove that any two members f,g of S agree, namely if f in func({0..m},A) and g in func({0..n},A) such that m ≤ n, then forall k in {0..m} ( f(k) = g(k) ). Then you can 'glue' all the members of S to get the desired function. In ZFC, you would do this by constructing their union, since each function is just a set of pairs.

I can walk you throw it

It requires something like 2n+2 integration by parts

I'll type it up for you an in easier form

This is where a good choice of notation can really help condense the proof

@user21820 Does it bother you that will consider two different meta functions to be the same function within the system.

ZFC

set theory in general really

For instance $f,g : \{1\} \to {\0\}$ by f(x):= 0 and g(x):= 15*x - 15

are different functions, as their algorithms are fundamentally different, but set theory will consider them both to be the same function

@DavidReed Why should it bother you? A function in ZFC and many other foundational systems is essentially just its extension and not any of the many possible intensions (philosophically speaking). If we want to talk about programs (and differences between programs that have the same output behaviour), we simply talk about programs suitably encoded (say as strings).

For example proving the deduction theorem often resorts to principles of induction but I don't see where this "fits" within a system of logic

is induction something you can "derive" from the rules of logic or is it something we assume is true on a metalogical level?

@user21820 so, I have defined multiplication as follows:

and indeed, you do not need uniqueness of h to prove properties of * but you need it to prove uniqueness of the function values

also, there is a thing in my textbook he defines ordering through sets (\in etc) can I just stick with no sets notation? cause I'm sick of it :) I mean I've seen someone define order as forall m,n in N m > n \iff \exists b in N m = n + b and m != n