There exists a functional in the dual of a Banach space that distinguishes points Let $X$ be a Banach space and $X^*$ its dual space. We will show that if $x \neq y$, then there is a $\phi \in X^*$ such that $\phi x \neq \phi y$. By way of contradiction suppose $\phi x = \phi y$ for $x\neq y$. Then, 
\begin{align*}
\phi x = \phi y &\iff \phi x - \phi y = 0 \\
&\iff \phi(x-y) = 0 \\
\end{align*}
Then, we have to have that $\phi(0) = 0$, so that $\phi(x-y) = 0 = \phi(0)$ and therefore $x-y = 0$, so that $x=y$. 
Questions: 
1) Am I allowed to assume linearity of $\phi$, i.e. does $\phi(x) - \phi(y)$ indeed equal $\phi(x-y)$ as I used for an arbitrary Banach space, $X$? 
2) Is it appropriate logic to conclude that if $\phi(x-y) = \phi(0) \Rightarrow x-y=0 \Rightarrow x=y$? 
 A: Let $S$ be the scalars. That is $S=\mathbb R$ or $S=\mathbb C.$ 
(1). If $x\ne y$ and $x, y$ are linearly dependent then WLOG $x\ne 0$ and $y=kx$ with $1\ne k\in S.$ Let $<x>$ be the $1$-dimensional vector subspace  generated by $\{x\}.$ Then $<x>$ is closed. 
Let $f(rx)=r$ for $r\in S$. Then $f\in <x>^*$ with $\|f\|=1.$ By Hahn-Banach there exists an extension $\phi\in B^*$ of  $f$.  And $\phi (x)=f(x)=1\ne k=f(y)=\phi (y).$
(2). If $x,y$ are linearly independent let $<x,y>$ be the $2$-dimensional vector subspace generated by $\{x,y\}.$ Now $<x,y>$ is closed. If $a,b,a',b'\in S$  then $$ax+by=a'x+b'y\implies (a-a')x+(b-b')y=0\implies (a=a'\land b=b')$$ because $x,y$ are linearly independent. So for $z\in <x,y>$ there are unique scalars $a,b$ such that $z=ax+by.$
Define $f(ax+by)=a$ for $ a,b\in S$. Now $<y>$ is also closed and $x\not \in <y>$ so $$0<c=\inf \{x+yd:d\in S\}.$$ So when $a\ne 0$ we have $$\|ax+by\|=|a|\cdot \|x+a^{-1}by\|\geq |a|\cdot c=|f(ax+by)|c.$$ And when $a=0$ we have $f(ax+by)=0.$ So $\|f\|\leq 1/c<\infty,$ so $f\in <x,y>^*.$
By Hahn-Banach, $f$ extends to $\phi\in B^*.$ And we have $\phi(x)=f(x)=1\ne 0=f(y)=\phi(y).$
Remark. For  Banach space $Y$ and $g\in Y^*$,   for all $x\in Y$ we have $|g(x)|=\|g\|\cdot d(x,g^{-1}\{0\})$ where $d(x,g^{-1}\{0\})=\inf \{\|x-y\|: g(y)=0\}.$ So in (2) we have $\|f\|=1/c.$
A: 1) Yes, the elements of $X^*$ are linear functionals, so you can use properties like $\phi(x-y)=\phi(x)-\phi(y)$ without justification.
2) If this were true, it would imply that $\phi$ is a one to one function. Also, since every nonzero linear functional $f: X\rightarrow \mathbb{R}$ is onto, $\phi$ is linear, one to one and onto, so $X$ and $\mathbb{R}$ are linearly isomorphic. So you can't apply the reasoning you wrote when $\dim X>1$. 
Now, about your argument, let me rewrite it a little more carefully, emphasizing with bold a detail you missed: "We will show that if $x\neq y$, then there is a $\phi\in X^*$ such that $\phi(x)\neq \phi(y)$. By way of contradiction, suppose that $f(x)=f(y)$, for every $f\in X^*$. By linearity,  $f(x-y)=0$, for every $f\in X^*$."
So to arrive to a contradiction, you need to find a $\phi \in X^*$ such that $\phi(x-y)\neq0$. This can be done by applying a consequence of the Hahn-Banach theorem. I assume that by $X^*$ you mean  the topological dual of $X$. For  the algebraic dual it's much easier to find such a $\phi$ and you certainly don't need the Hahn-Banach theorem.
