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 A∨B prop, provided that A prop and B prop. As a rule of inference,
A prop B prop
---------------------------
A∨B 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, A∨B true whenever A true (in words "there exists
a proof of A∨B, whenever there
exists a proof of A"). As a rule of inference,
A true
-------------------
A∨B 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
H1⋯Hm ⊢ 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):T1→T2
which says that we may conclude that (λx:T1.E)
has the type T1→T2
(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.