What exactly is a judgement?

Question

Before formulating my question, let me briefly sum up what I know about the topic (feel free to correct me if something I claimed is false!). This is for you good to see what my state of knowledge is, and maybe some people could learn something.

This is what I know

An interesting problem in logic is: how can one precisely define a relation $\Gamma\vdash\phi$ between a set $\Gamma$ of formulae and a single formula $\phi$, that formalizes the intuitive notion of "there is a proof of $\phi$ with the axioms $\Gamma$". There are different calculi that solve this problem, for example Hilbert systems and calculi of natural deduction. Without question the more natural solution is a natural deduction calculus which tries to model logical reasoning as it's done by mathematicians. This calculus operates with sequents which are ordered pairs $(\Gamma, \phi)$ and tries to define what a derivable sequent is. This is done through inference rules, which tell us how to get from given sequents to other sequents. For example the rule $$\frac{(\Gamma\cup\{\psi\}, \phi)}{(\Gamma, \psi\rightarrow\phi)}$$ tells us that if $(\Gamma\cup\{\psi\}, \phi)$ is a derivable sequent, then so is $(\Gamma, \psi\rightarrow\phi)$. One can state a bunch of these rules and then define that a sequent is derivable iff it can be shown to be so by a finite number of applications of the given rules. Now we can define our syntactic consequence relation $\vdash$ as follows:

$$\Gamma\vdash\phi\quad:\Leftrightarrow\quad \text{the sequent $(\Gamma, \phi)$ is derivable.}$$ When I learned this it was quite confusing to me that $\Gamma\vdash\phi$ can denote two different things:

1. The statement that says that the sequent $(\Gamma, \phi)$ is derivable.

2. The sequent $(\Gamma, \phi)$ itself is sometimes denoted $\Gamma\vdash\phi$. Thus the inference rule above can also be written like that:

$$\frac{\Gamma\cup\{\psi\}\vdash \phi}{\Gamma\vdash \psi\rightarrow\phi}.$$

My question

What exactly is a judgement? Looking into wikipedia

In mathematical logic, a judgment or assertion may be thought of as a statement or enunciation in the meta-language. For example, typical judgments in first-order logic would be that a string is a well-formed formula, or that a proposition is true. Similarly, a judgment may assert the occurrence of a free variable in an expression of the object language, or the provability of a proposition. In general, a judgment may be any inductively definable assertion in the metatheory.

If I understand it correctly then judgement is not a technically defined term but is used to describe meta-statements about a formally defined logic. But it seems to me that this interpretation isn't compatible with many things I read. For example on the wikipedia page about natural deduction linked to above it says:

The general form of an inference rule is:

$$\frac{J_1\quad J_2\quad\cdots\quad J_n}{J}$$

where each $J_i$ is a judgment.

But in my way of thinking sequents are not judgement. In particular, I think that the rule $$\frac{(\Gamma\cup\{\psi\}, \phi)}{(\Gamma, \psi\rightarrow\phi)}$$ does not state that if $(\Gamma\cup\{\psi\}, \phi)$ then $(\Gamma, \psi\rightarrow\phi)$ (because this wouldn't make sense, the sequent $(\Gamma\cup\{\psi\}, \phi)$ is a mathematical object and can't imply something; to say "if $3$ then $5$" is bullshit too) but instead I think that this rules says that if the sequent $(\Gamma\cup\{\psi\}, \phi)$ happens to be derivable then $(\Gamma, \psi\rightarrow\phi)$ is derivable.

Also, wikipedia says:

The most important judgments in logic are of the form "$A$ is true".

Shouldn't it be "valid" instead of "true"? The formulae $A$ could be true in some models but false in others, right? So what does it me for a formula $A$ to be "true"?

The nlab and wikipedia tell me that "$P$ prop" is a judgement too which says that $P$ is a well-formed formula. Wikipedia for example gives this inference rule

$${\frac {A{\hbox{ prop}}\qquad B{\hbox{ prop}}}{(A\wedge B){\hbox{ prop}}}}$$

I wonder why they used the vertical line here. I thought above and under the vertical line there should be mathematical objects, and the rule tells us that if the objects above are derivable in a certain calculus then the mathematical object(s) under the vertical line are derivable objects in the particular calculus. But "$P$ prop" is in my way of thinking not a mathematical object, but a statement in the meta-language. Thus if one was to give a calculus that defines which words over the alphabet are well-formed then the rule should be

$${\frac {A\qquad B}{(A\wedge B)}}$$

which says that

$A, B\text{ well-formed}\implies (A\wedge B)\text{ well-formed}$

The nlab page also talks about judgements $(x:X)⊢(ϕ\text{ prop})$ (here $\vdash$ obviously means $\vdash$ in the second meaning explained above). This is a judgement in a judgement. Is this allowed? It says that the statement that $\phi$ is well-formed is a consequence of the typing judgement $x:X$, right?

---

Could you please clarify my confusions and explain to me what exactly a judgement is?

Answer 1

I highly recommend reading Martin-Löf's paper referenced by Ulrik Buchholtz in the comments to your question. Apart from that, here are a couple of point that might help, some of which were already made by Andreas Blass in his answer.

A judgement is an act of knowing, or asserting a piece of knowledge about a mathematical object. For instance, a non-traditional single-sorted first-order logic could have the following kinds of judgments:

1. $t\ \mathsf{term}$, intended meaning "$t$ is a well-formed term"
2. $P\ \mathsf{prop}$, intended meaning "$P$ is a well-formed formula"
3. $\Gamma\ \mathsf{hyps}$, indented meaning "$\Gamma$ is a well-formed list of hypotheses"
4. $\Gamma \vdash P\ \mathsf{holds}$, intended meaning "formula $P$ is derivable under hypotheses $\Gamma$".

You do not normally see all of these because for first-order logic the first three are very simple and they get relegated to an informal explanation of syntax. But notice that there is a difference between the syntactic object "$P \land Q$" and the assertion "$P \land Q$ is a well-formed formula" (a judgment). If you doubt that there is a difference, consider the syntactic object "$P \land (Q \lor R$". We can speak meaningfully about it ("It's missing a closing parenthesis", "It contains two connectives."), but we do not assert "$P \land (Q \lor R$ is a well-formed formula".

Let me emphasize the difference between the sequent $$\Gamma \vdash P$$ and the judgement $$\Gamma \vdash P\ \mathsf{holds}.$$ The sequent is a syntactic object. The judgement is an assertion about the syntactic object. A lot of texts use the same notation for both, and that's where some of the confusion may be coming from. (Also note that many texsts write "$\mathsf{true}$" instead of "$\mathsf{holds}$", but I want to emphasize here that I am not talking about semantic truth, but ratehr about derivability.)

Rules of inference explain how we can build evidenece of assertions. The "syntactic" assertions, such as as "$P$ is a well-formed formula" or "variable $x$ does not occur in $P$" can be explained in terms of inference rules, but you won't see them in logic textbook, because they prefer to explain syntax in an informal way, e.g., "If $P$ is a wff and $Q$ is a wff then $P \land Q$ is a wff." If we want to, we can write down the corresponding formal rule: $$\frac{P\ \mathsf{prop} \qquad Q\ \mathsf{prop}}{(P \land Q)\ \mathsf{prop}}.$$ This says: "If $P$ is a well-formed formula and $Q$ is a well-formed formula, then $P \land Q$ is a well-formed formula." It is different from the rule $$\frac{\Gamma \vdash P\ \mathsf{holds} \qquad \Gamma \vdash Q\ \mathsf{holds}}{\Gamma \vdash P \land Q\ \mathsf{holds}}$$ which says: "If $P$ is derived from hypotheses $\Gamma$ and $Q$ is derived from hypotheses $\Gamma$, then $P \land Q$ can also be derived from hypotheses $\Gamma$."

To see why it might make sense to have formal rules for establishing that something is a wff, consider the rule: $$\frac{ }{\Gamma \vdash t = t\ \mathsf{holds}}$$ It does not say that $t$ must be a well-formed term. It would be more precise to say: $$\frac{\Gamma\ \mathsf{hyps} \qquad t\ \mathsf{term}}{\Gamma \vdash t = t\ \mathsf{holds}}$$ Now the rule is explicit: reflexivity holds only under well-formed hypotheses, and only for well-formed terms. Of course, we need to give rules for $t\ \mathsf{term}$ and $\Gamma\ \mathsf{hyps}$. They would be something like $$ \frac{ }{()\ \mathsf{hyps}} \qquad\qquad \frac{P\ \mathsf{prop} \qquad \Gamma\ \mathsf{hyps}}{(P, \Gamma)\ \mathsf{hyps}} $$ and (assuming that the language has variables $x_k$, a constant $1$ and a binary operation $+$): $$ \frac{k \in \mathbb{N}}{x_k\ \mathsf{term}} \qquad\qquad \frac{ }{1 \ \mathsf{term}} \qquad\qquad \frac{t\ \mathsf{term}\qquad u\ \mathsf{term}}{(t + u)\ \mathsf{term}} $$ I am fudging details about meta-level natural numbers that are used for indexing variable names. You can devise your own solution (for instance use unary representation of numbers, and give inference rules for such a representation).

It is perhaps silly to follow such rigorous formal discipline for first-order logic, but there are formal systems where the discipline is necessary. Dependent type theory is an example, as well as formal systems describing programming languages. These can grow quite complex, and since they also get implemented in practice, it is quite helpful to have all details written down formally.

Answer 2

I think the problem here is that different logical systems can formalize different sorts of information. For example, in traditional deductive systems, the notion of "well-formed formula" is not formalized; it's part of the meta-language. But in other systems, notably Martin-Löf type theory, that notion (or at least a very close relative of it) is included in the formal system by judgements of the form "$A$ prop".

Similar things happen with other notions. For example, the notion of substitution, i.e., "the result of substituting term $t$ for free variable $x$ in formula $\varphi$" is usually available only in the meta-language, but there are systems in which it is also formalized in the object language.

In my (admittedly limited) experience with such things, the word "judgement" is usually used for the object-language formalization of assertions that, in many other systems, would be part of the meta-language. Typical examples would be "$A$ is a proposition," "$T$ is a type," and "$X$ is defined to be $D$."