Judgment (mathematical logic)

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.

The same cannot be done with the other two deductions systems: as context is changed in some of their rules of inferences, they cannot be formalized so that hypothetical judgments could be avoided—not even if we want to use them just for proving derivability of tautologies.

In type theory, some analogous notions are used as in mathematical logic (giving rise to connections between the two fields, e.g. Curry–Howard correspondence).

The abstraction in the notion of judgment in mathematical logic can be exploited also in foundation of type theory as well.