What is, formally, to define a function by induction? Let me be more specific:
Given the context of a function as a relation between 2 sets with specific properties, what is formally happening when I define a function by induction?
EXAMPLE: (from Lang's Algebra)

Proposition 1.3. Every infinite set contains a denumerable subset.
Proof. Let $S$ be an infinite set. For every non-empty subset $T$ of $S$, we select a definite element $a_T$ in $T$. We then proceed by induction. We let $x_1$ be the chosen element $a_S$. Suppose that we have chosen $x_1, ..., x_n$ having the property that for each $k=2,...,n$ the element $x_k$ is the selected element in the subset which is the complement of $\{x_1,...,x_k\}$. We let $x_{k+1}$ be the selected element in the complement of the set $\{x_1,...,x_n\}$. By induction, we thus obtain an association $n \rightarrow x_n$ for all positive integers $n$, and since $x_n\neq x_k$ for all $k<n$ it follows that our association is injective, i.e. gives an enumeration of a subset of S.

 A: The principle of mathematical induction is equivalent to the principle of recursion on $\mathbb N$, and each is equivalent to the claim that every non-empty set $S\subseteq N$ has a smallest element (i.e., that $\mathbb N$ is well-ordered). Each of these claims/principles appear to be very self-evident, which is perhaps the reason why it is unclear why these principles are named principle, instead of just "proof techniques" or "facts about $\mathbb N$".  
Now, a function is a relation satisfying a certain property. However, a recursive description of a function requires a small leap of faith in order to be convinced that it actually defines a function. The reason is that for the function to be defined the relation needs to simply exist as an object. However, the recursive description of a function does not on its own produce such an object. Rather, it relies on a more dynamic process whereby one gives on extending the domain of the function, one element at a time, until finally the domain is the entire set $\mathbb N$. This is not a very precise notion, albeit very intuitive. 
Recalling that any proof of definition in mathematics must be finite (at least in the classical logical system) the problem becomes clear. The recursive description of a function will require infinitely many lines to write in order to actually define the function. What is intuitively clear is that nothing is stopping us from writing any finite initial segment of such a definition, but we can never actually finish it off. That is where the principle of recursion comes in. It says that we accept it as a finite definition, replacing the infinite definition just because we are convinced that we can write any finite initial segment of it. 
A similar situation holds true with the principle of induction. It accepts a prescription for obtaining any finite initial segment of infinitely many proofs for infinitely many claims,  as a proof of all of the claims. 
When going past countable sets things get more subtle. The extension of the principle of induction/recursion to sets of arbitrary cardinality is related to the axiom of choice. 
A: Formally speaking when we define something by induction, or recursion (in Hebrew, for example, the two terms are practically exchangeable in most contexts), is this.

Suppose that $f\colon A\to A$ then for $a\in A$ there exists a unique $F\colon\Bbb N\to A$ such that $F(0)=a$ and $F(n+1)=f(F(n))$.

When you define a sequence by a formula such as $a_{n+1}=2(a_n)^3+1$, you define the function $f$ and by setting $a_0=0$ you define $a$. From this point $F$ is uniquely defined and allows us to actually obtain the sequence that we want.
A: 
Proposition: Given a set $X$, a $f: X \rightarrow X$, and $a \in X$
$\exists ! u: \mathbb{N} \rightarrow X$ such that:
(1) $u(1)=a$
(2) $\forall n \in \mathbb{N}~~ (~~u(s(n))=f(u(n))~~)$

Proof:
UNIQUENESS - Let $u, v$ be two functions that satisfy the properties. Define $X:=\{x \in \mathbb{N}: u(n)=v(n)\}$
$u(1)=a=v(1) \implies 1 \in X$
$n \in X \implies u(n)=v(n) \implies f(u(n))=f(v(n)) \implies u(s(n))=v(s(n)) \implies s(n) \in X$
$\implies X=\mathbb{N} \implies \forall n \in \mathbb{N}: (~~ u(n)=v(n)~~ ) \implies u=v$
EXISTENCE - Define $C:=\{ A \subset \mathbb{N}\times X : (~~(1,a) \in A \wedge ( \forall (n,x) \in \mathbb{N} \times X ~~ (~~(n,x) \in A \implies (~~ s(n), f(x) ~~) \in A ~~)~~)$
And let $\displaystyle u:= \bigcap _{A \in C} A: A \subset \mathbb{N} \times X$
Let $D:=\{n \in \mathbb{N}: \exists ! x \in X (~~ (n,x) \in u~~ )\}$
We shall prove by induction.

(i) $1 \in D \rightarrow$
Existence: $(1,a) \in D$
Uniqueness: Suppose that $\exists b \neq a : (~~(1,a) \in u \wedge (1,b) \in u ~~)$
Let $A_1$ be a set of $C$, and define:
$Ã:=A_1 \backslash \{(1,b)\}$
We have that: $(n,x) \in Ã \implies (n,x) \in A_1 \implies (~~(s(n), f(x))~~) \in A_1$
Because $s(n) \neq 1$, $(~~(s(n),f(x))~~) \neq (1,b)$. And then:
$(~~(s(n), f(x))~~) \in A_1 \implies (~~s(n), f(x)~~) \in Ã \implies Ã \in C$
$(1,b) \notin Ã \implies (1,b) \notin u$
CONTRADICTION

Now, we shall prove that $u \in C$:
We have trivially that $(1,a) \in u$.
$(n,x) \in u \implies \forall A (~~(n,x) \in A~~) \implies \forall A (~~(s(n), f(x)) \in A ~~) \implies ((s(n), f(x)) \in u$
Therefore, $u \in C$

(ii) $n \in D \implies s(n) \in D$
Existence: $n \in D \implies \exists  x \in X (~~(n, x) \in u~~) \implies (s(n),f(x)) \in u \implies \exists y \in X (s(n), y) \in u \implies s(n) \in D$
Uniqueness:
Suppose there exists $f(x) \neq f(y)$ such that $(s(n), f(x)) \wedge (s(n),f(y)) \in u $
Define $ü:= u\backslash \{(s(n), f(y))\}$
$(m,z) \in ü \implies (m,z) \in u \implies (s(m), f(z)) \in u$
We wish to prove that $\forall (m,z) \in u~~ (~~(s(m), f(z)) \neq (s(n), f(y))~~)$.
Suppose it was not so. More specifically, suppose $\exists (m,z) \in u~~(~~(s(m), f(z)) = (s(n),f(y)~~)$
$s(m)=s(n) \implies m=n$
$\exists ! x \in X (~~(n,x) \in u~~) \implies (m,z)=(n,x) \implies (s(m), f(z))=(s(n), f(x)) \implies f(z)=f(x) \implies f(x)=f(y)$ CONTRADICTION
Therefore, $\forall (m,z) \in u~~ (~~(s(m), f(z)) \neq (s(n), f(y))~~)$.
So: $(m,z) \in ü \implies (m,z) \in u \implies (s(m), f(z)) \in u \implies  (s(m), f(z)) \in ü \implies ü \in C$
CONTRADICTION
A: Defining a function by induction
gives a way of computing the function
for all the values in a discrete domain.
Example: $f(1) = 1$, $f(n) = f(n-1)+2n-1$
for integer $n > 1$
defines a function which takes values
at the positive integers.
The relation here is
$R(n, m) $ is true
if and only if
$n$ is a positive integer
and $m = f(n)$
and false otherwise.
A: The purpose of this answer is to apply Asaf'a formalization to the proof of Lang's Proposition 1.3. It might be of interest since another step in a formal proof needs to be made explicit. On occasion, you may need to cross your t's and dot your i's to formally deploy the recursive definition of a function.
The AoC is used to demonstrate the following.
Proposition 1: Let $S$ be an infinite set and let $\mathscr F(S)$ be the finite nonempty subsets of $S$. Then there exists a mapping $\mathcal F$ from $\mathscr F(S)$ to itself satisfying the following
$\tag 1 \text{For all } F \in  \mathscr F(S) \text{,} \; F \subset \mathcal F(S) \text{ and } \, \mathcal F(F) \setminus F \;  \text{ is a singleton set}  $
We continue, using the framework provided by Proposition 1.
Proposition 2: Let $F_0$ be any singleton subset of $S$. Then there exists a function $D: \mathbb N \to \mathscr F(S)$ satisfying 
$\tag 2 D(0) = F_0$
$\tag 3 D(n+1) = \mathcal F(D(n))$
The sequence of sets forms a chain $F_n \subsetneq F_{n+1}$ where for any  $n \gt 0$, $\; F_n \setminus F_{n-1}$ is a singleton.
Proof: The function $D$ is inductively defined and the statements follow from properties of the function $\mathcal F$.
Exercise: Define an injective function $f: \mathbb N \to S$.
