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?

2 Answers 2

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).