# 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.

Judg"ment (?), n. [OE. jugement, F. jugement, LL. judicamentum, fr. L. judicare. See Judge, v. i.]

1.

The act of judging; the operation of the mind, involving comparison and discrimination, by which a knowledge of the values and relations of thins, whether of moral qualities, intellectual concepts, logical propositions, or material facts, is obtained; as, by careful judgment he avoided the peril; by a series of wrong judgments he forfeited confidence.

I oughte deme, of skilful jugement, That in the salte sea my wife is deed. Chaucer.

2.

The power or faculty of performing such operations (see 1); esp., when unqualified, the faculty of judging or deciding rightly, justly, or wisely; good sense; as, a man of judgment; a politician without judgment.

He shall judge thy people with righteousness and thy poor with judgment. Ps. lxxii. 2.

Hernia. I would my father look'd but with my eyes. Theseus. Rather your eyes must with his judgment look. Shak.

3.

The conclusion or result of judging; an opinion; a decision.

She in my judgment was as fair as you. Shak.

Who first his judgment asked, and then a place. Pope.

4.

The act of determining, as in courts of law, what is conformable to law and justice; also, the determination, decision, or sentence of a court, or of a judge; the mandate or sentence of God as the judge of all.

In judgments between rich and poor, consider not what the poor man needs, but what is his own. Jer. Taylor.

Most heartily I do beseech the court To give the judgment. Shak.

5. Philos. (a)

That act of the mind by which two notions or ideas which are apprehended as distinct are compared for the purpose of ascertaining their agreement or disagreement. See 1. The comparison may be threefold: (1) Of individual objects forming a concept. (2) Of concepts giving what is technically called a judgment. (3) Of two judgments giving an inference. Judgments have been further classed as analytic, synthetic, and identical.

(b)

That power or faculty by which knowledge dependent upon comparison and discrimination is acquired. See 2.

A judgment is the mental act by which one thing is affirmed or denied of another. Sir W. Hamilton.

The power by which we are enabled to perceive what is true or false, probable or improbable, is called by logicians the faculty of judgment. Stewart.

6.

A calamity regarded as sent by God, by way of recompense for wrong committed; a providential punishment.

"Judgments are prepared for scorners." Prov. xix. 29. "This judgment of the heavens that makes us tremble."

Shak.

7. Theol.

The final award; the last sentence.

Judgment, abridgment, acknowledgment, and lodgment are in England sometimes written, judgement, abridgement, acknowledgement, and lodgement.

Judgment is used adjectively in many self-explaining combinations; as, judgment hour; judgment throne.

Judgment day Theol., the last day, or period when final judgment will be pronounced on the subjects of God's moral government. -- Judgment debt Law, a debt secured to the creditor by a judge's order. -- Judgment hall, a hall where courts are held. -- Judgment seat, the seat or bench on which judges sit in court; hence, a court; a tribunal. "We shall all stand before the judgment seat of Christ." Rom. xiv. 10. -- Judgment summons Law, a proceeding by a judgment creditor against a judgment debtor upon an unsatisfied judgment.

Arrest of judgment. Law See under Arrest, n. -- Judgment of God, a term formerly applied to extraordinary trials of secret crimes, as by arms and single combat, by ordeal, etc.; it being imagined that God would work miracles to vindicate innocence. See under Ordeal.

Syn. -- Discernment; decision; determination; award; estimate; criticism; taste; discrimination; penetration; sagacity; intelligence; understanding. See Taste.

Also sp. judgement.