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:

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

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?