# Judgments in formal systems

In formal logic, type theory and formal programming language semantics, a judgment is an extralogical assertion about some grouping of the elements of the domain of discourse. We let the meta-variable J stand for a judgment.

In working with a formal system, we are often interested in some axiomatization of a particular judgment. Typically, such axiomatizations are presented as a collection of inference rules which have the form:

J1 ⋯ Jn
-----------------------
J

Which means that the judgment J holds, provided that all of the judgments J1 through Jn hold.

Example:

In presenting a propositional logic, two judgments are of interest: the first A prop says that the object A is a proposition. For example, in usual first order logics, one has that AB prop, provided that A prop and B prop. As a rule of inference,

A propB prop
---------------------------
AB prop

The second judgment A true says that the proposition A is true, that is that there exists a proof that A is true. For example, AB true whenever A true (in words "there exists a proof of AB, whenever there exists a proof of A"). As a rule of inference,

A true
-------------------
AB true

(Note that this is one of a pair of so-called introduction rules for disjunction. The full set of inference rules for propositional logic is beyond the scope of this w/u.)

## Hypothetical Judgments

Often one wishes to define a judgment that holds only under some set of assumptions. We will say that the judgment J is qualified by a collection of hypotheses H1 through Hm. And we write H1Hm ⊢ J. Where the symbol (⊢) (typically called turnstile) visually separates the hypotheses from the conclusion of the judgment.

Example:

In the study of programming languages, one is often most interested in the judgment E:T which asserts that the expression E of your language has type T (the judgment is usually pronounced "E is well-typed (at type T)"). However, in most realistic programming languages, the type of an expression depends on the types of the variables that appear within it. As a result, the judgment is parametrized by a collection Γ of hypotheses of the form x1:T1,…,xm:Tm. The form of the judgment then is Γ ⊢ E:T, which is pronounced "in the context Γ, the expression E has type T".

As an example, one could consider the inference rule for lambda abstraction in the (Church-style) simply typed lambda calculus:

Γ,x:T1 ⊢ E:T2
-------------------------------
Γ ⊢ (λx:T1.E):T1T2

which says that we may conclude that (λx:T1.E) has the type T1T2 (that is, that it is a function from values of type T1 to values of type T2) in the context Γ, provided that in the extended context where we carry the additional hypothesis that x has type T1 we can show that E has type T2.

## Theorems

Of course asserting that certain judgments are true is merely a game of symbol pushing unless one can answer several questions about the inference rules stated for a particular judgment: are there enough rules? indeed, are there too many rules? are the rules consistent with each other? do they "make sense"?

The particular questions one may ask depend on the particular domain one works in. In logic, for example, one may wish to relate the judgment A true with truth in some model of the logic. Then one would typically prove a soundness and a completeness theorem. In programming languages, one would show a type safety theorem that says that evaluation of well-typed expressions does not go wrong.

## Analytic and Synthetic Judgments

The logician Per Martin-Löf (actually, the idea stems from Kant) identified several classes of judgments according to the sense in which they could be understood to hold. (We have already seen hypothetical judgments as one such class). Two other classes are of particular importance:

A judgment is analytic if it "is evident by virtue of the meanings of the terms that occur in it." (Martin-Löf).

A judgment is synthetic if one must look outside of itself for evidence.

For example, the judgment A prop is analytic, because (as we've seen in the case of disjunction) we need only consider the subterms of A to determine whether A itself is a proposition.

On the other hand, the judgment A true is synthetic. That is so because the judgment merely asserts that a proof of the truth of A exists, it does not tell us how to obtain that proof.

One may ask if there is an analytic judgment for the truth of propositions. And indeed there is. The trick is to record the proof of the proposition within the judgment. If we let M stand for proof terms, the judgment has the form M:A (read "M is a proof that proposition A is true").

A remarkable gem of mathematical logic is the so-called Curry-Howard Isomorphism which states that the proof terms of intuitionistic logic are exactly the terms of the lambda calculus (the isomorphism was first observed for first-order logic and the simply-typed lambda calculus, but it extends to higher-orders).

Isn't that amazing? Your purely functional program is my constructive proof!

References:

Pfenning, Frank and Rowan Davies. A Judgmental Reconstruction of Modal Logic. In Mathematical Structures in Computer Science, 11(4):511--540, August 2001.