In mathematical logic, a judgment expresses an assertion about provability, it is used as an auxiliary concept for formalizing foundations of several different deduction systems. This concept is defined differently in the various deduction systems: it is “exploited” to different extents. This basic diversity among the various calculi allows such difference, that the same basic thought (e.g. deduction theorem) must be proven as a metatheorem in Hilbert-style deduction system, while it can be declared explicitly as a rule of inference in natural deduction. As mentioned, the notion of “judgment” is defined differently in various calculi. As for grasping what is common in the way they are used: in all the three calculi mentioned above, a logical axiom expresses a judgment, premises of a rule of inference are formed as a sequence of judgments, and their conclusion is a judgment as well. Also the result of a proof expresses a judgment, and the used hypotheses are formed as a sequence of judgments. In Hilbert-style deduction system, judgments are simply formulae themselves, but in natural deduction, a judgment expresses explicitly an assertion about deducibility of a formula from a given context. In sequent calculus, a judgment (called a sequent) is even more complex. This more sophisticated “architecture” enables the latter two systems of deduction to declare such laws explicitly which are only hidden implicit (as metatheorems) in Hilbert-style deduction system. 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 exploited also in foundation of type theory as well. See for example simply typed lambda calculus.
External links
- Judgments in formal systems. Everything2.
- Pfenning, Frank (2004 Spring). "Natural Deduction", 15-815 Automated Theorem Proving.
- Martin-Löf, Per (1983). On the meaning of the logical constants and the justifications of the logical laws. Siena Lectures.
