formalizing the least upper bound axiom Is the least upper bound axiom the following:
$P(S)\implies (\exists u\in\mathbb{R})(U(u,S)\land L(u,S))\tag{1}$
or
$P(S)\iff (\exists u\in\mathbb{R})(U(u,S)\land L(u,S))\tag{2}$
where 
$P(x) \iff$ $x$ is a nonempty subset of real numbers and $x$ is bounded above
$U(x, X) \iff$ $x$ is an upper bound of $X$
$L(u,X)\iff$ $u$ is least among upper bounds of $X$
(or neither)? And how do you know? 
(and if it's (1), then how do we conclude a set $S$ is nonempty if "$\sup{S}$ exists" is known?)
 A: The interpretation of the L(u,X) predicate as a conditional in terms U(u,X) is really weird ... 
Why not say that L(u,X) means u is a least upper bound of X
Then let's first define what it means for something to be a set of real numbers with a real number upper bound:
$\forall X (P(X) \leftrightarrow (\exists x x \in X \land X \subseteq R \land \exists x (x \in R \land U(x,X)))$
Now, let's define what a least upper bound for any such set is:
$\forall X (P(X) \rightarrow \forall y (L(y,X) \leftrightarrow (U(y,X) \land \forall x (U(x,X) \rightarrow y \leq x))))$
And finally, we can express the least upper bound axiom, which says that if a set has an upperbound, then it has a least upper bound:
$\forall X (P(X) \rightarrow \exists y L(y,X))$
or, alternatively, we can avoid using the P(X) predicate altogether: 
$\forall X (X \subseteq R \rightarrow (\exists x \: U(x,X) \rightarrow \exists y L(y,X)))$
In other words, the least upper bound property is expressed more like your 1) (i.e. using a $\rightarrow$ instead of a $\leftrightarrow$) ... though there is really no need to include the U(y,X) predicate.
OK, but then you ask: how then can we prove that X is non-empty if it has a least upper bound?
Well, informally: For x to be an upper bound for any set (empty or not) X, x needs to be greater or equal to all elements of X.  But that is trivially true for any x if X is empty. So, if X is empty, then any real number x will be an upper bound. But, that means that an empty set X cannot have a least upper bound, for if y would be a least upper bound for X, then it would be the smallest of all upper bounds, but that is impossible, since y-1 would also be an upper bound (since, again, every real number is an upper bound for empty set X, so y-1 as well). In sum: if X is empty, X has no upper bound. The contrapositive of this is that if X does have a least upper bound, then X is not empty.
Now, for this proof, you need a definition of what an upper bound is! I suggest:
$\forall X (X \subseteq R \rightarrow \forall x (U(x,X) \leftrightarrow (x \in R \land \forall y (y \in X \rightarrow y \leq x)))$
So from this definition alone, you should be able to prove:
$\forall X (\neg \exists x x \in X \rightarrow \forall x (x \in R \rightarrow U(x,X))$ (i.e. every real number is an upper bound for an empty set)
And using the definition of the least upper bound as provided earlier, you can then prove that:
$\forall X (\neg \exists x x \in X \rightarrow \neg \exists x L(x,X))$ (i.e. an empty set has no least upper bound)
the contrapositive of which is:
$\forall X (\exists x L(x,X) \rightarrow \exists x x \in X)$ (i.e. any set with a least upper bound is non-empty)
as desired.
