SEP: Let Y be a convex, located and inhabited set in $ \mathbb{R}^n$ such that $0 \notin Y$. Fix $y^1,\dots,y^l$ in Y. Then there exists and $ \xi \in Y$ such that \begin{align*} (\langle \xi, y^1 \rangle , \dots, \langle \xi , y^l \rangle ) >0, \end{align*} meaning all entries of the vector are nonnegative and at least one is greater $0$.
LLPO: $\forall x , y \in \mathbb{R} : x \ge 0 \vee x \le 0$.
I am trying to prove constructively that LLPO implies SEP.
I tried to do this by induction:
The case $n=1$ is trivial.
For the general case I tried to split $Y$ into two sets. $Y_1 = \{ y \in Y : y_n = 0\}$ and $Y_2 = \{ y \in Y : y_1 = \dots = y_{n-1} = 0\}$.
The problem however is now, that in order to apply the Induction Hypothesis, I need that $Y_1$ is convex and $ 0 \notin Y_1$. But this does not necessarily hold. Is there a more sophisticated way to solve this?
Your two sets $Y_1$ and $Y_2$ do not contain enough information to determine the set $Y$ uniquely. If $Y$ is a ball that doesn't meet any of the coordinate axes, then $Y_1=\emptyset$ and $Y_2=\emptyset$.
Here is one way to prove what you want. The key is the following lemma:
To prove this, you only need to observe that if $\langle\xi,x\rangle\leq0$ for some $x\in Y$, then the line joining $\xi$ and $x$ is also in $Y$ by convexity and you can argue that this line has a point closer to the origin than $\xi$, contradicting the choice of $\xi$. (You may argue that this is not constructive. For me this still counts as constructive: The vector $\xi$ is given explicitly. Then it is proven that the choice cannot fail the desired property. Perhaps there are more constructive variants of the same argument if that is an issue.)
In your original problem you can then define $Y'$ to be the convex hull of the points $y^1,\dots,y^l$. This defines a convex and compact set contained in $Y$. Since $0\notin Y$, we also have $0\notin Y'$. Apply the lemma to the set $Y'$ and you are done.
Some additional remarks:
Showing that the line has a closer point than $\xi$: The line is not perpendicular to $\xi$ because otherwise $\langle\xi,\cdot\rangle$ would be constant on the line. Therefore the line is not tangent to the sphere $S(0,|\xi|)$ but actually goes inside it. To see this more rigorously, you can take the direction vector $v=x-y$ of the line and see that the condition on the inner products implies $\langle\xi,v\rangle<0$. Thus the function $t\mapsto|\xi+tv|^2$ has a negative derivative at $t=0$, showing that it takes lower values than $|\xi|$. You can also use tools from linear algebra.
The convex hull of a finite set is always compact. However, for this argument it is enough that it's closed. The proofs I have seen are somewhat involved, although the result is easy to believe. Perhaps you could somehow argue that the convex hull is a finite intersection of finitely many closed half spaces (from which closedness follows easily)? (Also, I would argue that the construction is explicit, and non-constructive arguments are only used to show that it cannot fail. I see compactness falling in this category. What constructivity means is a matter of taste.)
The proof I presented is constructive in the following sense: It provides a method (which can be implemented numerically) to find such a vector $\xi$, given the points and the set. In my field (inverse problems) this is understood as a constructive proof. The proof that the suggested method works may use any logical tools. I know that in many other fields constructivity means other things, and in some respects this proof will almost certainly not count as constructive. This answer is from my perspective, which is all I can do, as no specific meaning for constructivity was given in the question.