How to designate that a proposition is semantically true? The question is more about mathematical notation I guess. In logic we can designate that a conclusion $B$ is (syntactically) deducible from the premises $A$ by:
$A_1...A_i ⊢ B$
If the above is true the syllogism then is called valid (regardless premises are true or false in a real sense). For example:
Humans are gods $A_1$
Gods can fly $A_2$
Humans can fly $B$
Yes, that looks logically correct but hurts the eyes. Then, to say the syllogism is sound we also need to designate that the premises are semantically true (or true in a real sense; at least by beliefs of the author). 
I though I could do it by double turnstile:
$ ⊨ A $
As it turns out, that means something different. Particularly (as wiki says), $A$ is tautology or "the expression $A$ is a semantic consequence of the empty set". 
This isn't the case as well if I understood it correctly:
$ A ⊨ B $
If $A$ is true in a (any?) given interpretation then $B$ is also true. Or maybe if $A$ is semantically true then $B$ is also semantically true? Here things become vague to me.
So how then I could notationally express that $A$ is true in a real sense?
 A: The "double turnstile" symbol $\vDash$ expresses the fact that a formula $A$ is valid, i.e. true in every interpretation.
In the context of propositional logic $\vDash A$ reads : "$A$ is a tautology". 
In the context of propositional logic, the semantical concept of interpretation can be formalized with truth valuations (or : assignments).
In this case we can write $v(A)= \text T$ or $[[A]]_v = \text T$ to express the fact that valuation $v$ satisfies formula $A$, i.e. that $A$ is evaluated to $\text {TRUE}$ by $v$.

As you say, the double turnstile symbol can be used also to mean logical consequence :

$A \vDash B$

reads : "there is no interpretation in which $A$ is true and $B$ is false" or, alternatively, "every interpretations that makes $A$ true, makes true also $B$."
A: First, some terminological issues. $A\vdash B$ usually means $A$ is provable or derivable from $B$. This is a purely syntactic property that is about building formal proofs and does not require knowing whether anything is "true" or not. Validity usually means that a formula is semantically true in all models and is written $\vDash B$ with $A\vDash B$ as shorthand for "$\mathfrak M\vDash A$ implies $\mathfrak M\vDash B$" for all models $\mathfrak M$ with $\mathfrak M\vDash A$ meaning "$A$ is semantically true in model $\mathfrak M$". "Syllogism" has a fairly specific meaning and is relatively archaic at this point. You'll rarely find it used in a modern logic textbook except in a "history of logic" section. You are also using "sound" in the more philosophical sense. This unfortunately conflicts with "sound" in the mathematical logic sense which becomes relevant... now. $\vdash$ and $\vDash$ are (for a given logic) usually sound and complete. Soundness means "$\vdash B$ implies $\vDash B$", i.e. what we can prove is valid. Completeness means "$\vDash B$ implies $\vdash B$", i.e. we can prove everything that is valid. Soundness and completeness together mean that $\vdash$ and $\vDash$ are the same relation on formulas which is why the terminology often gets muddled. However, soundness and completeness are non-trivial (meta-)theorems (particularly completeness), and you need to understand what $\vdash$ and $\vDash$ mean on their own before you can prove them.
To actually start addressing your question, it doesn't make sense in mathematical logic to talk about a formula just being "true". You can talk about it being provable (i.e. a theorem) or being valid. Validity, as I mentioned before, is defined in terms of a notion of semantic truth, and the key thing here is that truth is with respect to a model written $\mathfrak M\vDash B$ which means $B$ is true in the model $\mathfrak M$. Validity can then be written as "for all models $\mathfrak M$, $\mathfrak M\vDash B$". For propositional logic, the models are often called "valuations" or "(truth) assignments" as in Mauro ALLEGRANZA's answer. In this case, they consist entirely of assignments of truth values to atomic propositions which can then be lifted to assignments of truth values to all formulas via the interpretation of the connectives.
The closest thing to what you want is therefore something like $\mathfrak M\vDash B$ for some particular model $\mathfrak M$.
There is nothing in mathematical logic to say that some formula is "true in reality". Whether something is "true in reality" is not a mathematical question but a physical or maybe a philosophical one. Even semantics in mathematical logic interprets things into mathematical structures, typically sets, so semantic truth is just a statement about certain mathematical structures.
If a mathematical logician wanted to say something about a formula being "true in reality" (which would be a very odd thing for them to do), they'd just say it in natural language.
