In
mathematical logic
Mathematical logic is the study of Logic#Formal logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory (also known as computability theory). Research in mathematical logic com ...
, a judgment (or judgement) or assertion is a statement or enunciation in a
metalanguage. For example, typical judgments in
first-order logic would be ''that a string is a
well-formed formula
In mathematical logic, propositional logic and predicate logic, a well-formed formula, abbreviated WFF or wff, often simply formula, is a finite sequence of symbols from a given alphabet that is part of a formal language.
The abbreviation wf ...
'', or ''that a proposition is true''. Similarly, a judgment may assert the occurrence of a
free variable in an expression of the object language, or the provability of a
proposition
A proposition is a statement that can be either true or false. It is a central concept in the philosophy of language, semantics, logic, and related fields. Propositions are the object s denoted by declarative sentences; for example, "The sky ...
. In general, a judgment may be any inductively definable assertion in the
metatheory.
Judgments are used in formalizing
deduction systems: a
logical axiom expresses a judgment, premises of a
rule of inference are formed as a
sequence
In mathematics, a sequence is an enumerated collection of objects in which repetitions are allowed and order matters. Like a set, it contains members (also called ''elements'', or ''terms''). The number of elements (possibly infinite) is cal ...
of judgments, and their conclusion is a judgment as well (thus, hypotheses and conclusions of proofs are judgments). A characteristic feature of the variants of
Hilbert-style deduction systems is that the ''context'' is not changed in any of their rules of inference, while both
natural deduction and
sequent calculus contain some context-changing rules. Thus, if we are interested only in the
derivability of
tautologies, not hypothetical judgments, then we can formalize the Hilbert-style deduction system in such a way that its rules of inference contain only judgments of a rather simple form. The same cannot be done with the other two deductions systems: as context is changed in some of their rules of inferences, they cannot be formalized so that hypothetical judgments could be avoided—not even if we want to use them just for proving derivability of tautologies.
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.
In
type theory
In mathematics and theoretical computer science, a type theory is the formal presentation of a specific type system. Type theory is the academic study of type systems.
Some type theories serve as alternatives to set theory as a foundation of ...
, some analogous notions are used as in
mathematical logic
Mathematical logic is the study of Logic#Formal logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory (also known as computability theory). Research in mathematical logic com ...
(giving rise to connections between the two fields, e.g.
Curry–Howard correspondence). The abstraction in the notion of ''judgment'' in mathematical logic can be exploited also in foundation of type theory as well.
See also
*
Simply typed lambda calculus
*
Mathematical logic
Mathematical logic is the study of Logic#Formal logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory (also known as computability theory). Research in mathematical logic com ...
References
*
*
*
External links
*
*
* {{cite web , last=Martin-Löf , first=Per , author-link=Per Martin-Löf , title=On the meaning of the logical constants and the justifications of the logical laws , work=Siena Lectures , year=1983 , url=http://www.cs.cornell.edu/info/Projects/Nuprl/cs671/cs671-fa99/martin.html
Proof theory
Logical calculi
Concepts in logic