"Interpretation" versus "judgement" versus "assertion"? I believe "assertion" and "judgment" mean the same thing (at least according to Per Martin Lof). I understand that they are meta statements (above that of say formal propositions). How, if at all, do these meanings differ from that of "interpretation", which is also on top of a proposition?
 A: In "mainstream" treatment of mathematical logic, The Turnstile symbol is used in:

$\Gamma \vdash \alpha$

to mean that formula $\alpha$ is derivable from the set $\Gamma$ of premises according to the rules of the logical calculus (aka: proof system), i.e. using logical axioms and Modus Ponens or e.g. Natural Deduction rules.
It derives from Frege (1879) : "...Frege's symbol came to be called the assertion sign.  Frege's notation for a judgement $\vdash A$ can then be read I know $A$ is true."
The Double turnstile symbol is used in:

$\Gamma \vDash \alpha$

to mean that $\alpha$ is a logical consequence of the set $\Gamma$ of premises.
This second notion is defined using the concept of interpretation: the set of the interpretations that make all members of $\Gamma$ true is a subset of the set of the interpretations that make $\alpha$ true.
The two relations are very different but strictly linked: a calculus is said to be sound and complete when:

$\Gamma \vDash \alpha \text {  iff  } \Gamma \vdash \alpha$.

In other words, the caluclus is able to derive from a set of premises all and only the logical consequences of the said premises.
If so, we are licensed to read the judgment $\Gamma \vdash \alpha$ both as "formula $\alpha$ is derivable from premises $\Gamma$" and as "formula $\alpha$ is true in every model of $\Gamma$".

Things are a little bit different with a different approach; see e.g. Per Martin-Lof's Intuitionistic type theory (1984):

[page 2] When we hold a proposition to be true, we make a judgement: $A$ is a proposition, "proposition $A$ is true" is a judgement.


In particular, the premisses and conclusion of a logical inference are judgements.

And

[page 6] a proposition is true if it has a proof, that is, if a proof of it can be given.

A: An interpretation is a situation in which a statement can become true or false.
The claim that the statement is true in that situation is a judgement.
E.g., "$P$ means 'is even' and $a$ means '1'" is an interpretation.
"Under the interpretation where $P$ means 'is even' and $a$ means '1', the statement $P(a)$ is false" is a judgement or assertion.
There are plenty kinds of assertions other than truth under an interpretation, e.g. "$X$ is provable", "$X$ logically entails $Y$", $X$ is a formula", etc.
