I wanted to prove in RCA0 that:
If f:A→A be a function and i∈A, then for all n, fⁿ(i) exists.
To reach that, I proved another theorem. I wrote my proof but I'm not sure it's rigorous. If you read it, please tell me it is, or it is not.
Theorem:
Suppose f:A→A be a function and i∈A. Then for all n, there is a unique sequence a s.t lh(a)=n+1 and ∀k<n ( a(k+1)=f(a(k)) )
Proof:
Let P be this formula: P(n): ∃x [ x∈seq ∧ lh(x)=n+1 ∧ x(0)=i ∧ ∀k<n ( x(k+1)=f(x(k)) ) ] We use sigma0-1 induction to prove ∀n P(n). P(0) is obviously true. Suppose that P(n) holds. So there is a sequence x satisfies the conditions. Define sequence y like this: lh(y)=n+2 and ∀k<n+1 ( y(k)=x(k) ) and y(n+1)=f(y(n)) So y satisfies the conditions and P(n+1) holds. So, by induction, ∀n P(n).
For uniqness, suppose x and y are two different sequence satisfy the conditions for n. let m<n+1 be a number s.t ¬( x(m)=y(m) ). Without loss of generality, let m be the least element by this property. So x(m-1)=y(m-1). Then f(x(m-1))=f(y(m-1)) that means x(m)=y(m). Contradiction.
For arbitrary n, define fⁿ(i)=a(n). So we've proved that for all n, fⁿ(i) exists.