@user21820 I'm proving the recursion theorem right now, basically what you do there is constructing h similar to how N was constructed, right?

@famesyasd Well to prove the full recursion theorem you need to construct finite approximations and so on.

@user21820 hmm, what I did I did in a same way as to how N was constructed. You define Recursive(b) analogically to Inductive(b) and the define Hoar(x) analogically to Natural number(n) and then define h to be the set of all Hoar(x)

Hoar is some random name

I'm not sure what you mean. You'd have to state your particular version of recursion theorem. I suspect that it is a weaker version than the one I'm referring to.

And I got to go so I'll look at it next time.

@user21820 Given any F : A -> A and a in A there exists single h : N -> A such that 1) h(0) = a and 2) forall n in N h(S(n)) = F(h(n))

I'm almost 100% sure that what I did is correct

we can immediately prove that Rec_F,a(h) and that forall b Rec_F,a(b) -> h subset b from that we conclude similar induction principle: forall b if b subset h and Rec_F,a(b) then b = h

@famesyasd Okay that's a weaker version. The fact that you already have a function F from A to A makes it significantly weaker, and indeed you can do something like the construction of N from the axiom of infinity. Maybe you can ask someone else here to check your proof, since I'm going off. Anyway the full recursion theorem is actually a meta-theorem:

> Given any 2-parameter sentence Q you can prove (in ZFC) "forall f ( if f is a function with domain N[<n] for some natural n then there is a unique x ( Q(f,x) ) ) implies exists f ( f is a function with domain N and forall n in N ( Q( f on N[<n] , f(n) ) )".

okay

I change my mind about yours sufficing. Yours is not exactly a recursion theorem, because each element in the sequence is only determined by the preceding one.

The recursion theorem that should suffice for ordinary mathematics is:

> Given any F in func( { g : n in N and g in func(N[<n],A) } , A ), there is a unique h in func(N,A) such that forall n in N ( h(n) = F( h on N[<n] ) ).

Note that this vacuously subsumes the 'base case'.

Here N[<n] = { k : k in N and k<n }.

Okay see you next time!

bye!

@user21820 so another variant may skip some steps instead of only decreasing by one, right? that's the difference