Well, i'm fine too, and i'm actually a young developper, and one of my aims are to get a graduate of mathematics, but from now i'm studying logic (i'm a rookie in math and logic)
And i would like to understand the fundamentals of mathematics
Ah I see. If you're serious about learning logic (and have a little bit of background in mathematics), I recommend you read the links from my profile page, and especially focus on Stephen Simpson's notes in my list of references.
I didn't personally learn from his notes, but it was the best online introductory material I found so far that has significant content.
Before that, let me make my point clear. Even if your question didn't ask for uniqueness, you would be unable to prove the recursion theorem if we skip Step 2, unless we have axiom of choice.
Hmm the only way you can completely grasp it is to write down the full theorem in formal form and observe the quantifier structure. Why don't you try that now?
The problem with many textbooks is that they use "let" in an inconsistent manner, so beware.
More or less yes. Basically although there are infinitely many possible moves I can make on my first move, you have an abstract way of handling any of them.
Excellent.
Okay with this now? Then we can go back to the recursion theorem.
yes, you're meaning, a proof is a way of saying, despite you gave me a x, i can say that the predicate is true only referring to properties of x that it shares with other elements of the set N
so that means that the predicate will be true for every element in N
Let P(n) assert that exists y ( n = 2y or n = 2y+1 ). Note that 0 = 2*0 or 0 = 2*0+1. Thus exists y ( 0 = 2y or 0 = 2y+1 ). Thus P(0). Given any n in N such that P(n): | ... | P(n+1). Therefore forall n in N ( P(n) ).
Stupid chat. I can't indent properly. See the vertical bars? It means that those two lines are under the "Given any n in N such that P(n):"
Recursion theorem asserts forall set E , forall function g : E->E , forall c in E ( exists function f : N->E ( f(0) = c and forall n in N ( f(n+1) = g(f(n)) ) ) ).
Proof goes like this: Given set E and function g : E->E and c from E: | [Steps 1,2,3,4]
Step 1 proves forall k in N ( exists h : {0..k}->E ( h(0) = c and forall n in N[<k] ( h(n+1) = g(h(n)) ) ) )
Step 2 proves forall k in N ( forall h,h' : {0..k}->E ( h(0) = c and forall n in N[<k] ( h(n+1) = g(h(n)) ) ) and ( h'(0) = c and forall n in N[<k] ( h'(n+1) = g(h'(n)) ) ) implies h = h' )
See why I separated the two steps? First one is for existence, second one is for uniqueness.. Together Steps 1,2 prove forall k in N ( exists unique h : {0..k}->E ( h(0) = c and forall n in N[<k] ( h(n+1) = g(h(n)) ) ) )
Step 3 first does for each k in N let h[k] : {0..k}->E such that ( h(0) = c and forall n in N[<k] ( h(n+1) = g(h(n)) ) ) ) Note that this is valid because we proved uniqueness. Here I'm reusing the variable name "h" and this time it is a sequence, which is nothing more than a function with domain N.
Okay I think it's not a good idea to reuse variable names formally.. I'm going to deviate from my post and use H here. The reason is that what I just wrote above is not allowed unless you have uniqueness.
In ZF we cannot just define a sequence H on N, such that H(n) satisfies some property for each n in N, just by showing the existence of such an object for each n in N.
Something like that. Precisely, for each specific k in N you can produce a h witnessing P(k). But you can't produce a function H such that for each k in N we have H(k) witnessing P(k).
Unless you can uniquely identify the witness for each k, or you have the axiom of choice.
Specifically Step 1 showed that for each k in N there is some ordered pair in H with first entry k, while Step 2 showed that for each k in N there are no two different ordered pairs in H with first entry k.
Not quite. We say that f is a function from S to T when f(x) in T for any x in S. S is the domain and T is the codomain. Technically in set theory there's no such thing as codomain because all the set of pairs can tell you is the range.
