nLab judgment

Judgments

Context

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels

semantics

Foundations

foundations

The basis of it all

 Set theory

set theory

Foundational axioms

foundational axiom

Removing axioms

Judgments

Idea

In mathematics and especially in formal logic, by a judgement [Frege (1879, §2)] one means the assertion [Russell & Whitehead (1910, p. xviii)] or validation [Kochen (1961, p. 2)] of a proposition PP, hence the claim (or even the specification) of a proof of PP [Church (1940, §5)].

To bring out the subtle (cf. jstor:43154266) but crucial distinction — eloquently amplified by Martin-Löf (1996, lectures 1-2) — between the notion of a proposition PP as such and the judgement/assertion/validation/proof of its truth, it is tradition to prefix the latter with the symbol “\vdash”, known as the Urteilsstrich (German: “judgement stroke”) of [Frege (1879, §2)] (see the historical pointers below), as:

(1)P. \vdash \; P \,.

For example, the Riemann hypothesis certainly is a proposition, but it remains open whether we may truthfully assert or validate it, hence we cannot yet judge that it holds true: No proof is known, even though it seems likely to be in fact true.

In other words, the judgement symbols “P\vdash \, P ” convey that we know (a proof of, hence the truth of) PP [Martin-Löf (1996, lectures 1-2)].

As such, judgements may be formalized as “meta-proposition”, namely propositions but in an ambient meta-language (the deductive system or logical framework) rather than to the object language in which the given PP itself is formulated. (More specifically, any deductive system includes, as part of its specification, which strings of symbols are to be regarded as the judgments. Some of these symbols may themselves express a proposition in the object language, but this is not necessarily the case.)

More generally, one considers hypothetical judgements (maybe first made explicit in [Church (1940, §5)]) which are such assertions/validations but conditioned on premises, hence claims/specifications of proofs based on assumptions AA: Writing

(2)AP A \;\;\vdash\;\; P

is to express the judgement that given any assertion/validation/proof of AA we know how to produce (from that) a validation/proof of PP.

In systems of (dependent) type theory (where such notation seems to go back to Hofmann (1995, p. 31), cf. below) this is quite literally the case in that the categorical semantics of such a hypothetical judgement is a given by a function (and typically a computable function, hence an algorithm) which maps proofs of AA to proofs of PP.

More generally yet, in type theory the propositions AA and PP appearing here are allowed to be any (dependent) types (see at propositions as types). In this generality, the denotational semantics of hypothetical judgements (2) is given by (computable) functions/morphisms with domain AA and codomain PP. In programming languages based on such type theories this translates to the denotation of an actual program which produces data of data type PP when run on input data of data type AA.

Judgements are themselves subject to a calculus of natural deduction by which further judgements may be inferred from given ones. For example the notation

AP 1,AP 1AP 1×P 2 \frac{ A \;\;\vdash\;\; P_1 ,\, \;\;\;\;\;\;\; A \;\;\vdash\;\; P_1 }{ A \;\;\vdash\;\; P_1 \times P_2 }

traditionally expresses that whenever we can assert both P 1P_1 as well as P 2P_2 assuming a validation of AA (hence: given a pair of functions with domain type AA), then with that same assumption we find assertion/validation/proof of their logical conjunction P 1×P 2P_1 \times P_2 (namely a function with codomain to their product type).

Finally, to make explicit which particular assumptions a hypothetical judgement really depends on, it is common to adjoin a generic context symbol Γ\Gamma to the hypothesis on the left hand side of the Urteilsstrich: Notation such as

Γ,a:Ap a:P \Gamma ,\,\;\; a \colon A \;\;\; \vdash \;\;\; p_a \,\colon\, P

expresses the judgement that PP may be asserted given validation of Γ×A\Gamma \times A, but that in doing so only the validation of AA is actually made use of, while Γ\Gamma may be any context of assumptions (whose validation might however be used in previous/further deduction steps).

Examples

In first-order logic

In first-order logic, a paradigmatic example of a judgement is the judgement that a certain string of symbols is a well-formed proposition. This is often written as “PpropP \;prop”, where PP is a metavariable standing for a string of symbols that denotes a proposition.

Another example of a judgement is the judgement that these symbols form a proposition proved to be true. This judgment is often written as “PtrueP\;true”.

Neither of these judgements is the same thing as the proposition PP itself. In particular, the proposition is a statement in the logic, while the judgement that the proposition is a proposition, or is provably true, is a statement about the logic. However, often people abuse notation and conflate a proposition with the judgment that it is true, writing PP instead of PtrueP\;true.

In type theory

The distinction between judgements and propositions is particularly important in intensional type theory.

The paradigmatic example of a judgment in type theory is a typing judgment. The assertion that a term tt has type AA (written “t:At:A”) is not a statement in the type theory (that is, not something which one could apply logical operators to in the type-theoretic system) but a statement about the type theory.

Often, type theories include only a particular small set of judgments, such as:

  • typing judgments (written t:At:A, as above)

  • judgments of typehood (usually written AtypeA \;type)

  • judgments of equality between typed terms (written say (t=t):A(t=t'):A)

(In a type theory with a type of types, judgments of typehood can sometimes be incorporated as a special case of typing judgments, writing A:TypeA:Type instead of AtypeA\;type.)

These limited sets of judgments are often defined inductively by giving type formation/term introduction/term elimination- and computation rules (see natural deduction) that specify under what hypotheses one is allowed to conclude the given judgment.

These inductive definitions can be formalized by choosing a particular type theory to be the meta-language; usually a very simple type theory suffices (such as a dependent type theory with only dependent product types). Such a meta-type-theory is often called a logical framework.

Hypothetical and generic judgments

It may happen that a judgment JJ is only derivable under the assumptions of certain other judgments J 1,,J 2J_1,\dots, J_2. In this case one writes

J 1,,J nJ. J_1,\dots,J_n \;\vdash J.

Often, however, it is convenient to incorporate hypotheticality into judgments themselves, so that J 1,,J nJ J_1,\dots,J_n \;\vdash J becomes a single hypothetical judgment. It can then be a consequence of other judgments, or (more importantly) a hypothesis used in concluding other judgments. For instance, in order to conclude the truth of an implication ϕψ\phi\Rightarrow\psi, we must conclude ψ\psi assuming ϕ\phi; thus the introduction rule for implication is

ϕψϕψ \frac{\phi \;\vdash\; \psi}{\vdash\; \phi\Rightarrow\psi}

with a hypothetical judgment as its hypothesis. See natural deduction for a more extensive discussion.

In a type theory, we may also consider the case where the hypotheses J 1J_1 are typing judgments of the form x:Ax:A, where xx is a variable, and in which the conclusion judgment JJ involves these variables as free variables. For instance, JJ could be ϕprop\phi\;prop, where ϕ\phi is a valid (well-formed) proposition only when xx has a specific type XX. In this case we have a generic judgement, written

(x:X)(ϕprop). (x \colon X) \;\vdash\; (\phi \; prop).

which expresses that assuming the hypothesis or antecedent judgement that xx is of type XX, as a consequence we have the succedent judgement that ϕ\phi is a proposition. If on the right here we have a typing judgment

(x:X)(t:A) (x \colon X) \;\vdash\; (t \colon A)

we have a term in context.

For more about the precise relationship between the various meanings of \vdash here, see natural deduction and logical framework.

While this may seem to be a very basic form of (hypothetical/generic) judgement only, in systems such as dependent type theory or homotopy type theory, all of logic and a good bit more is all based on just this.

History of the notion and notation

The terminology of judgement in formal logic, and the notation

A \vdash A

for the judgement of content AA is due to Frege (1879, §2) (Frege’s das Urtheil – or das Urteil in modern German spelling – directly translates to: the judgement).

This notion and notation (often “Frege’s Urteilsstrich” – “judgement stroke”) was adopted by Russell & Whitehead (1910, p. xviii), who however speak of “assertion” instead of “judgement” — see Martin-Löf (1996, p. 6) for speculation that these authors may have wanted “to avoid any association with Kantian philosophy” (cf. below):

and then by Church (1940, §5) (without any attribution) — now allowing hypotheses/assumptions on the left of the Urteilsstrich — to mean provable under these assumptions:

Similarly, Kochen (1961, p. 2) introduced (in a context of model theory) the notation “𝔄P\mathfrak{A} \;\vDash\; P” (apparently not actively remembering its historical origin, cf. Kochen (2017)) for a notion in model theory pronounced “𝔄\mathfrak{A} validates PP” — which is at least closely related to these hypothetical judgements (and often used synonymously, e.g. here):

The need (which had been contested by some logicians such as Wittgenstein, cf. jstor:43154266) for Frege’s distinction between a proposition “AA”, as such, and its judgement/assertion/proof/validation “A\vdash A” was eloquently argued for by Martin-Löf (1984, pp. 2), (1987) and in (1996, lectures 1-2), together with a re-promotion of Frege’s Urteilsstrich notation “\vdash” (ML84, p. 2, ML96, p. 2, 6):

The notation for hypothetical judgements

(3)contextjudgement context \;\vdash\; judgement

was then (without attribution to Church or Martin-Löf) adopted for dependent type theory in Hofmann (1995, p. 31), later published as Hofmann (1997, p. 82):

This eventually became the trademark of the practice of dependent type theory (though mostly used without any attribution), e.g.: Jacobs (1998, p. 2, 121, 586); Bauer, Haselwarter & Lumsdaine (2020).

(Curiously, apparently Martin-Löf did not actually use the general notation (3) in publications: When in 1996, p. 29 it comes to hypothetical judgements, he switched to using just a vertical “|\vert” instead of “\vdash”.)

In summary:

terminologyauthor
judgementFrege (1879)
assertionRussell & Whitehead (1910)
proofChurch (1940)
validationKochen (1961)
judgementMartin-Löf (1984, 1996)
Hofmann (1995, 1997)


References

Pre-history of the notion of judgement (Urteil) in (informal) logic:

The origin of the notion of “judgement” (and of the notation “\vdash” for it) in formal logic:

and under the name “assertion” in:

Keeping the symbol “\vdash”, now allowing hypothesis on the left, but pronouning it as “proof under assumptions”:

Discussion in the context of what became known as Martin-Löf dependent type theory:

Reviewed in:

Further discussion in

Textbook acccount in a context of programming languages:

The alternative notation “\vDash” for satisfaction with closely related (if different) usage seems to originate in

whose author

cannot recollect whether [he] originated it or took it from some other paper.

according to:

See also:

Last revised on January 25, 2023 at 16:56:26. See the history of this page for a list of all contributions to it.