We can define an iterated forcing of length $\alpha$ by induction as follows:

Let $P_0=\emptyset$ .

Let $\hat{Q}_0$ be a forcing notion.

For $\beta\leq\alpha$ , $P_\beta$ is the set of all functions $f$ such that $\operatorname{dom}(f)\subseteq\beta$ and for any $i\in\operatorname{dom}(f)$ , $f(i)$ is a $P_i$ -name for a member of $\hat{Q}_i$ . Order $P_\beta$ by the rule $f\leq g$ iff $\operatorname{dom}(g)\subseteq\operatorname{dom}(f)$ and for any $i\in\operatorname{dom}(f)$ , $g\upharpoonright i\Vdash f(i)\leq_{\hat{Q}_i}g(i)$ . (Translated, this means that any generic subset including $g$ restricted to $i$ forces that $f(i)$ , an element of $\hat{Q}_i$ , be less than $g(i)$ .)

For $\beta<\alpha$ , $\hat{Q}_\beta$ is a forcing notion in $P_\beta$ (so $\Vdash_{P_\beta} \hat{Q}_\beta$ is a forcing notion).

Then the sequence $\langle \hat{Q}_\beta\rangle_{\beta<\alpha}$ is an iterated forcing.

If $P_\beta$ is restricted to finite functions that it is called a finite support iterated forcing (FS), if $P_\beta$ is restricted to countable functions, it is called a countable support iterated function (CS), and in general if each function in each $P_\beta$ has size less than $\kappa$ then it is a $<\kappa$ -support iterated forcing.

Typically we construct the sequence of $\hat{Q}_\beta$ 's by induction, using a function $F$ such that $F(\langle \hat{Q}_\beta\rangle_{\beta<\gamma})=\hat{Q}_\gamma$ .