induction (vs recursion) in proof This post is about "proof by induction". I want to understand if I've been doing it right. I'm a little confused by something I read in a textbook. My background in math doesn't go beyond undergraduate classes (basic analysis, algebra).
On pg47 of Handbook of Analysis and its Foundations, Schechter writes: "Induction is a method for proving statements about objects that have
already been defined; recursion is a method for defining new objects." He gives this principle:

Principle of Countable Induction. Suppose $1\in T\subseteq\mathbb{N}$
  and $T$ has the property that whenever $n\in T$ then also $n + 1\in T$. Then $T = \mathbb{N}$.

Suppose I wanted to prove the statement "every infinite set has a countable subset". Here is how I would do it: Suppose $S$ is our infinite set. We know $S\neq\emptyset$, so there exists some $x_1\in S$. Suppose $x_1,x_2,\dots,x_{k}\in S$ ($k=1,2,\dots$) have been picked. There exists some $x_{k+1}\in S$ such that $x_{k+1}\neq x_i$ (for $i=1,2,\dots,k$). "By induction", I've defined a sequence of distinct terms in $S$, which shows $S$ has a countable subset. 
My question is this: based on the quote from Schechter, am I actually using induction in my proof? What is the set $T$? It seems $T$ would be the domain of the sequence. If I wanted to be more explicit in my proof, I would say let $f$ be a function with domain $T$. Define $f(1)=x_1$ (so $1\in T$), and so on. So in my proof I'm defining the contents of $T$. $T$ isn't defined in advance, which is something that is required? 
The author also gives another principle:

Principle of Countable Recursion. Let $T$ be a set, and let $p$ be
  some map­ping from $\{$finite sequences in T$\}$ into $T$. Then there
  exists a unique sequence $(t_1,t_2, t_3,\dots)$ in $T$ that satisfies
  $t_n= p(t_1 , t_2 ,\dots, t_{n - 1})$ for all $n$.

But this is foreign to me.
 A: Strictly, you've built your sequence by recursion. However, recursion and induction are extremely tightly intertwined, and mathematicians are often sloppy about which word they use. It is further complicated by the fact that there are a couple of different kinds of induction: the principle you state is "the principle of mathematical induction", but there are also well-founded induction, structural induction, and so on. All these have the same flavour but are slightly different. (Well-founded induction corresponds to strong induction in $\mathbb{N}$.)
The "definition of functions by recursion" is also known as "the inductive definition of functions", and its validity is proved by induction. It has as a special case what you term the Principle of Countable Recursion, which is proved by induction using the following steps:

Define an attempt to be a sequence $(t_1, \dots, t_n)$ such that $t_n = p(t_1, t_2, \dots, t_{n-1})$, and say there is an attempt defined at $n$ if there is $(t_1, \dots, t_m)$ an attempt with $m \geq n$.
  
  
*
  
*Show (by induction) that for all $n$, if there are two attempts defined at $n$, then they agree on their first $n$ elements.
  
*Show (by induction) that for every $n$, there is an attempt defined at $n$.
  
*Conclude that the union over $n \in \mathbb{N}$ of all attempts defined at $n$ is a unique sequence satisfying $t_m = p(t_1, \dots, t_{m-1})$ for all $m$.
  

The principle doesn't really have a nice formulation. Wherever it turns up, its definition is really disgusting. The way you should think about it is "if I have a recursive definition of a function - that is, a specification of the value $t_n$ in terms of previous values $t_1, \dots, t_{n-1}$ - then there is a bona fide function $i \mapsto t_i$ which implements that recursive definition".
In your proof that every infinite set $T$ has a countable subset, you are not strictly using induction. Instead, you are defining by recursion a function $\mathbb{N} \to T$. However, you do use induction if you want to show that the countable subset is not finite (that is, where you show that your definition is of an injective function). Induction is what justifies your word "distinct".
Basically, you use recursion to define a function or sequence or object, and then to prove any properties about it, you use induction.
A: From the title of the question, it seems that you're worried about the difference between what is called "Induction" and what is called "Recursion". Coming from a background using a theorem prover (Coq), I can tell you that they are essentially the same thing. The key property of both is that you're only allowed prove/define a new thing in terms of previously proven/defined things. For induction, this means you can prove $P_{n+1}$ given $P_1, \dots, P_n$. For recursion, this means in your definition of $F_{n+1}$, only occurrences of $F_1, \dots, F_n$ can appear. For induction, you are proving something. For recursion, you are defining something. However, what you're doing is essentially the same, especially if you take the constructivist point of view that Coq takes and note that proving a theorem is really just defining a proof. Still, the difference is valid, insofar as mathematicians generally do not consider "proofs" as objects in the same sense as they do matrices, vectors, sequences, numbers, sets etc. I will not answer the rest of your question as I see a new answer come through by Patrick Stevens which seems to do this.
If you're really interested in the link between proofs as objects, I'd recommend reading about the Curry Howard Isomorphism. But it's pretty heavy unless you're really into it.
