Let $A$ be aan abstract C-algebra, and let $\varphi\colon A \rightarrow \mathbb C$ be a bounded linear function. Assuming the axiom of choice, there exist unique positive bounded linear functions $\varphi_+$ and $\varphi_-$ such that $\varphi = \varphi_+ - \varphi_-$ and $\|\varphi\| = \|\varphi_+\| + \|\varphi_-\|$ (see section 3.2 of Pedersen's _C-algebras and their Automorphism Groups_). Is the axiom of dependent choices sufficient to prove this result?
I believe that the axiom of dependent choices is sufficient to establish the result if $A$ is separable or commutative. If $A$ is separable, then the usual proof still works. If $A$ is commutative, then the decomposition can be obtained by lattice-theoretic methods, such as those in Schechter's Handbook of Analysis and its Foundations. In general, the self-adjoint operators of a noncommutative C*-algebra do not form a lattice (see examples II.3.3.3 in Blackadar's book).