Proving Hahn-Banach theorem directly Is is possible to find an example of nonreflexive Banach space for which one can establish Hahn-Banach theorem directly (not referring to the axiom of choice)?
 A: You can do it when the Banach space $E$ is separable (i.e. $\overline {\{x_n\}}=E$ for some sequence). Here a sketch of the way following the "Cours de Theorie de l'Approximation" of Professor P.J.Laurent (Grenoble University).
Let $V$ be a vector subspace of $E$ and $f\in V^*$ with $$||f||=\sup_{||x||\le 1;\space x\in V} |f(x)|$$ We have to show $\exists F\in E^*$ /  $F_{|V}=f$ and $||F||_E=||f||_V$.
Proof.-Let $x_0\in E \setminus V$ and $V_1=\{x+t_0x_0;\space x\in V,t_0 scalar\}$ (all $y\in V_1$ has a unique form $y=x+t_0x_0$). We extend $f$ to the linear variety $V_1$ preserving norm.
►Put $$\tilde f(y)=f(x)+\lambda t_0$$ $\tilde f$ is a linear functional for $V_1$ that coincides with $f$ over $V$ and choosing convenient $\lambda$ one can get equality of norms.
►►► $\big\{\big\{$To have $||\tilde f||_{V_1}\le||f||_V$ (i.e. the equality) choose $\lambda$ such that $|\tilde f|\le ||f||_V\cdot ||y||$ for all $y$ (i.e. for all $t_0$ and $x$, $$|f(x)+\lambda t_0|\le ||f||_V\cdot ||x+t_0x_0||\\ |f(\frac{x}{t_0})+\lambda|\le ||f||_V\cdot ||\frac{x}{t_0}||\\-||f||_V\cdot ||x+x_0||-f(x)\le \lambda\le ||f||_V\cdot ||x+x_0||-f(x)$$ In order to have a fixed $\lambda$ such that this be verified for all $x\in V$ one needs that for all $x’, x’’$
$$-||f||_V\cdot ||x’+x_0||-f(x’)\le ||f||_V\cdot ||x’’+x_0||-f(x’’)\\f(x’’)-f(x’)\le ||f||_V\cdot (||x''+x_0||+||x'+x_0||)$$ This is verified because of
$$f(x''-x')\le ||f||_V\cdot ||x''-x'||\le ||f||_V\cdot(||x''+x_0||+||x'+x_0||)\big\}\big \}$$
Thus we can find out a (continuous) linear form $\tilde f$ over $V_1$, extension of $f$ and such that $||\tilde f||_{V_1}=||f||_V$◄◄◄
►On the other hand, since $E$ is separable there is a countable subset of $E$, dense in $E$; we choose elements of this subset which does not belong to $V$, say $x_0,x_1,x_2,\ldots$; besides we consider the following successive linear varieties $$V_1=V_0+t_0x_0,\text{for all} \space t_0\\V_2=V_1+t_1x_1, ,\text{for all} \space t_1\\V_3=V_2+t_2x_2,\text{for all}\space t_2\\.....$$
($x_n$ can be eliminated if $x_n\in V_n$)
►We form the union $H=\cup_n V_n$ which is clearly dense in $E$.
Over each $V_n$ is defined a (continuous) linear form $f_n$, extension of $f$ that preserves the norm.
►Let $h$ be the (continuous) linear form defined as follows:
If $x\in H$ then there is $n$ such that $x\in V_n$ so we put $h(x)=f_n(x)$. It is clear that $$||h||_H=||f||$$
►Hence we can define $F$ by continuity: if $x\in H$ there is a sequence $\{x_n\}\subset H$ converging to $x$. Put $$F(x)=\lim_{x\to \infty} h(x_n)$$
Since for all $n$ one has $$|h(x_n)|\le ||h||\cdot ||x_n||$$
It follows $$\lim_{x\to \infty} |h(x_n)|=|F(x)|\le ||h||\cdot ||x_n||$$
Hence $$||F||\le ||h||$$ consequently $$\color{red}{||F||=||f||}$$
This proof is valid for all separable Banach, be it reflexive or not. In particular it is known $C([0,1],\mathbb R)$ is separable and non reflexive so it is an example as the O.P. asked.
