What is a judgment? I have a hard time trying to understand the concept of a judgment in natural deduction. One distinguishes between propositions and judgments. As I understand it, propositions are just well-formed formulae, and judgments are statements about propositions that are formulated in the metatheory we are working with. Thus under this interpretation "the formula $\phi$ has no free variables" and "there is a formal proof of $\phi$" are judgments, whereas formulae $\phi$ such as $\forall x\forall y(x = y)$ and $\exists x (R(x))$ are propositions. Now, the nlab says:

One writes $⊢J$ to mean that $J$ is a judgment that is derivable, i.e. a theorem of the deductive system.

But that contradicts my understanding of judgment (that I described above). Here, I would say that $J$ is a proposition (and not a judgment), and that $⊢J$ is a judgment. Could you clarify?
Also I wonder: if one writes down a sequent $\Phi\vdash \phi$ of the natural deduction calculus, is this a mathematical object, or a statement in the metatheory?
 A: The nlab article seems a bit off.  I suspect it's more due to trying to explain too much in too little space so things get mixed together.  I completely agree with you and I would call the whole expression "$\vdash J$" a judgement and not just $J$.  I elaborate on what's going on in a different answer and the my blog post referenced within.  The sequent you list would also be a judgement.  In fact, the claim that some piece of syntax is a well-formed formula would be yet another judgement.
Typically (though not always) judgements are inductively defined relations and, taking a set theoretic view, a derivation is then an element of the judgement.  What this means is something like $\vdash P \to P$ is actually a predicate and when we say that judgement holds we mean in the semantics of the meta-logic that $\exists d. d \in (\vdash P \to P)$.  From a different perspective, a derivation is a witness or a constructive proof that the judgement is satisfied.  These relations are defined over the syntax, i.e. the (raw) terms, of the object language being described (e.g. propositional logic) and perhaps other sets, e.g. the naturals.
The answer and blog post referenced spells this all out in examples in a machine-checked formal language.
Edit: Uff, after reading the page in detail, they aren't actually inconsistent with the sentence from the question (though they do dramatically but explicitly change the meaning of "$\vdash$" when they talk about hypothetical/generic judgements).  That said, the way the page is written makes it extraordinarily easy to be misled.  If you want to say "$M:A$" is a judgement meaning $M$ has type $A$, fine.  If you want to say "$\vdash M : A$" asserts the derivability of this judgement, fine. However, if you actually need generic judgements then the "$\vdash$" in the generic judgement, e.g. "$x : A \vdash x : A$", is something else entirely, and the occurrences of "$x:A$" on the left or right in the generic judgement are not themselves judgements nor have any meaning on their own.  The "$\vdash$" in the generic judgement is not some kind of operator.  The page doesn't claim otherwise (actually it does a bit...), but it strongly encourages this kind of misunderstanding.  There are remarks on the pages it references that state most of what I've said, e.g. here and here.  (Note, the first of these uses "$\vdash$" in the latter sense, and the second in the former sense.) In both of these remarks they point out that sometimes we can make this pun work.  LF heavily relies on this pun in practice, but it's failure is part of why systems like NLF, LLF, and CLF exist.
The upshot is "$\vdash$" is used in (at least) two very different ways, both of which are present on that page.  In some cases these two meanings can roughly coincide, but that is in no way guaranteed nor do I recommend it as a way of understanding either use of the notation in general (though it can be a powerful technique when applicable).
A: So I originally typed up most of this as my own question but I think maybe you might find this a little helpful.
If you use a tool like Ott it extracts grammar and judgments to inductive definitions. This can be useful but this isn't actually the standard semantics for judgments.
Usually judgements are interpreted in a way much weaker than an inductive definition more like a tagless final or PHOAS style which allows various tricks with higher order abstract syntax that would be inconsistent with the use of inductive definitions.
For example, if you have a grammar and judgements for the simply typed lambda calculus like so:
$$ \begin{align}
& t &  \mathrel{::=} \Box \mid t \rightarrow t \\
& e &  \mathrel{::=} x_n \mid e_0 \, e_1 \mid \lambda x_n \colon t. e \\
& \Gamma & \mathrel{::=} \bullet \mid \Gamma , x_n \colon t
\end{align}$$
$$
\begin{align}
 &\fbox{$\Gamma \vdash e \colon t$} \\
&\frac{x_n \colon t \in \Gamma}{\Gamma \vdash x_n \colon t}\\
& \frac{\Gamma , x_n \colon t \vdash e \colon t'}{\Gamma \vdash \lambda x_n \colon t. e \colon t \rightarrow t'}\\
&\frac{\Gamma \vdash e \colon t \rightarrow t' \qquad \Gamma \vdash e' \colon t}{\Gamma \vdash e \, e' \colon t'}
\end{align}$$
I will use very simple Coq code as an example because this is the theorem prover I personally am most familiar with but Coq is very silly for a number of reasons IMO.
A tool like Ott would extract to a tool like Coq something like
Inductive type :=
| box
| fn (t: type) (t': type).
Inductive term :=
| var (n: nat)
| lam (n: nat) (t: type) (e: term)
| app (e: term) (e': term).
Inductive env :=
| empty
| with (G: env) (n: nat) (x: type).

Inductive judge: env -> term -> type -> Prop :=
| jvar (G: env) (n: nat) (t: type):
  find n G = Some t ->
  judge G (var n) t
| jlam (G: env) (n: nat) (t: type) (t': type):
  judge (with G n t) e t' ->
  judge G (lam n t e) (fn t t')
| japp (G: env) (e: term) (e': term):
  judge G e (fn t t') -> judge G e' t ->
  judge G (app e e') t'

Where you would have to implement find yourself. Which can be useful but in general judgements are interpreted in a weaker way more like axioms or assumptions.
A more faithful interpretation of judgments might be a collection of axioms something like
Module Type STLC.
Axiom type: Set.
Axiom term: Set.
Axiom env: Set.

Axiom box: type.
Axiom fn: type -> type -> type.

Axiom var: nat -> term.
Axiom app: term -> term -> term.
Axiom lam: nat -> type -> term -> term.

Axiom empty: env.
Axiom with: env -> nat -> type -> env.

Axiom judge: env -> term -> type -> Prop.
Axiom jlam: forall (G: env) (e: term) (n: nat) (t: type) (t': type),
  judge (with G n t) e t' ->
  judge G (lam n t e) (fn t t').
Axiom japp: forall (G: env) (e: term) (e': term) (t: type) (t': type),
  judge G e (fn t t') -> judge G e' t ->
  judge G (app e e') t'.
End STLC.

I'm not quite sure how to write out the variable rule with this sort of approach. If I was going to use this sort of approach I would try to take advantage of HOAS and other features which would be inconsistent in an inductive definition.
For example if you were to axiomize the untyped lambda calculus you could take an approach like:
Module Type Lambda.
Axiom term: Set.
Axiom app: term -> term -> term.
Axiom lam: (term -> term) -> term.
Context {Setoid term).

Axiom beta: forall (f: term -> term) (x: term),
  app (lam f) x == f x
End Lambda.

The Setoid stuff is just a nice way of packaging up an equivalence relation in Coq. I didn't want to explicitly write out reflexivity, transitivity and symmetry.
So obviously there's a reason a more axiomatic approach isn't usually taken when mechanizing judgements in a theorem prover. This kind of style can definitely be a pain to work with even though it allows tricks like HOAS.
When an initial algebra exists (basically just an abstract syntax tree) the interpretation in terms of inductive types is ok because then the usual sort of collection of axioms can be defined as functions of the concrete interpretation in terms of inductively defined AST.
Module Type STLC.
  Axiom myterm: Set.
  Axiom mytype: Set.
  Axiom myenv: Set.
  Axiom myjudge: myenv -> myterm -> mytype -> Prop.
  Axiom eval_term: term -> myterm.
  Axiom eval_type: type -> mytype.
  Axiom eval_env: env -> myenv.
  Axiom eval_judge:
    forall G e t,
    judge G e t ->
    myjudge (eval_env G) (eval_term e) (eval_type t).
End STLC.

I think the long and short of it is that interpreting judgements as inductively defining grammar and relations only works if such an inductive definition is permissible (an initial algebra exists.)
If your collection of judgements doesn't work for an inductive definition then you can't interpret it that way.
The precise nature of when an inductive definition is bad depends on some tricky metatheory stuff.
You can see the cool https://counterexamples.org/strict-positivity.html for some trickery.
Not really any standard notation for obvious reasons but depending on technical details of the metatheory it should be possible to consistently interpret some non strictly positive judgements and do fun things with HOAS.
