The following writeup follows the notes by Lance Fortnow in http://oldblog.computationalcomplexity.org/media/ladner.pdf

Ladner's Theorem: If P=/=NP then there exist
NP intermediate languages.

Proof: Let (M_i)_i be an enumeration of polytime Turing machines, ie M_i is a
deterministic Turing machine running in time <= (n+2)^i and P =
{L(M_i) | i:N}.

Notice that for every polynomial p(n) there exists i such that p(n) <=
(n+2)^i.

Similarly, let (f_i)_i be an enumeration of all polytime computable
functions where again f_i(x) runs in time <= (|x|+2)^i so that in
particular |f_i(x)|<=(|x|+2)^i.


We seek a language A such that

1) A:NP

For each i: 
2.i)  A =/= L(M_i), 
3.i)  the function f_i is not a reduction SAT <= A, ie
   for each i there exists x such that either
    x:SAT and f_i(x) not in A or
    x not in SAT and f_i(x) in A

The conditions 2.i together ensure that A is not in P
The conditions 3.i together ensure that A is not NP-hard. 

We build A in the form

A = {x | x:SAT & f(|x|) even}

where f(n) can be computed in time polynomial in n. This will
guarantee A:NP since A <= SAT. 

We define f recursively by f(0)=f(1)=2 and if f(k) is defined for all
k<=n then f(n+1) is given as follows:

We introduce the abbreviation A_f = {x | x:SAT & f(|x|) even} where f
stands for the current function in the recursion.


1) If (2+log log n)^f(n) >= log n then f(n+1)=f(n).

Eventually, we will leave case 1 because (2+x)^d (for fixed d)
grows slower than 2^x. 

Otherwise, ie if (2+log log n)^f(n) < log n, then

2) if  f(n)=2i for some i then we make sure that
   condition 2.i will be satisfied:

    Check whether there exists an x with |x| <= log log n such that either 
    a)  M_i(x) accepts and x not in A_f or
    b)  M_i(x) rejects and x in A_f

If such x exists then f(n+1)=f(n)+1 else f(n+1)=f(n). We show below
that we will eventually get out of this case as well.

3)  if f(n)=2i+1 for some i then we make sure that
    condition 3.i will be satisfied:

    Check whether there exists an x with |x| <= log log n such that either 
    a)  x in SAT and f_i(x) not in A_f 
    b)  x not in SAT and f_i(x) in A_f

If such x exists then f(n+1)=f(n)+1 else f(n+1)=f(n). As before, we
will eventually find such x.

This completes the recursive definition of f and hence A = A_f.


We begin now by checking that all calls to f within A_f will be on
arguments for which f is already defined.

Indeed, in case 2 we call f on arguments |x| with |x| <= log log n <= n
thus we're fine. In case 3 we call f also on arguments |f_i(x)| with |x|<=log n.

We then have |f_i(x)| <= (2+|x|)^i <= (2+log log n)^f(n) < log n <= n,
so again it is ok.

This ensures that the definition of f terminates.

We now bound the runtime of f(n). Suppose we find a polynomial p(n)
bounding the time it takes to compute f(n+1) from f(i) for i<=n. Then,
by setting up a table for f we can compute f itself in time
sum_{i=1}^n p(i) which is again a polynomial in n (of degree
deg(p)+1).

Let us thus show that such a polynomial exists. In case 1 this is
obvious. In case 2 we need to consider O(2^(log log n))  = O(log n)  many
different inputs x of length <= log log n.  For each of those we have
to run M_i which takes time (2+|x|)^i <= (2 + log log n)^i < log n each and
also perform a SAT test which takes time O(2^|x|) = O(2^log log n) =
O(log n). Thus, we need time O((log n)^2) for all this.

In case 3 the situation is similar, but the SAT tests are run on
inputs of size (2+|x|)^i thus requiring time O(2^(2+log log n)^i) =
O(2^log n) = O(n) which is again polynomial in n.

Finally, we must argue that unless P=NP indeed A is different from
each L(M_i) and none of the f_i is a reduction from SAT to A. By
construction of A this is the case if f(n)=2i and f(n)=2i+1,
respectively. So, we must argue that, indeed, the range of f covers
all natural numbers >= 2. This is tantamount to showing that each case
is eventually left as announced above. For case 1 we have already
argued this. For case 2, suppose that f(n)=2i for all n>=n0 so we are
stuck in case 2. This means that f(i) is odd for only finitely many i
so that L(M_i) differs from SAT on only finitely many inputs (those x
for which f(|x|) is odd). That, however, would imply SAT in P since
L(M_i):P thus P=NP.

Suppose, on the other hand, f(n)=2i+1 for all n>=n0 so we are stuck in
case 3. In this situation, A will be a finite set and f_i : SAT <= A
which again would imply P=NP because every finite set is in P.