Judgment (mathematical logic)
Encyclopedia
In mathematical logic
, a judgment can be for example an assertion about occurrence of a free variable in an expression of the object language, or about provability of a proposition
(either as a tautology
or from a given context); but judgments can be also other inductively definable assertions in the metatheory
. Judgments are used for example in formalizing deduction systems: 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.
A characteristic feature of the various variants of Hilbert-style deduction system
s 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, no 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
, 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
.
Mathematical logic
Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...
, a judgment can be for example an assertion about occurrence of a free variable in an expression of the object language, or about provability of a proposition
Proposition
In logic and philosophy, the term proposition refers to either the "content" or "meaning" of a meaningful declarative sentence or the pattern of symbols, marks, or sounds that make up a meaningful declarative sentence...
(either as a tautology
Tautology (logic)
In logic, a tautology is a formula which is true in every possible interpretation. Philosopher Ludwig Wittgenstein first applied the term to redundancies of propositional logic in 1921; it had been used earlier to refer to rhetorical tautologies, and continues to be used in that alternate sense...
or from a given context); but judgments can be also other inductively definable assertions in the metatheory
Metatheory
A metatheory or meta-theory is a theory whose subject matter is some other theory. In other words it is a theory about a theory. Statements made in the metatheory about the theory are called metatheorems....
. Judgments are used for example in formalizing deduction systems: a logical axiom expresses a judgment, premises of a rule of inference
Rule of inference
In logic, a rule of inference, inference rule, or transformation rule is the act of drawing a conclusion based on the form of premises interpreted as a function which takes premises, analyses their syntax, and returns a conclusion...
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.
A characteristic feature of the various variants of Hilbert-style deduction system
Hilbert-style deduction system
In logic, especially mathematical logic, a Hilbert system, sometimes called Hilbert calculus or Hilbert–Ackermann system, is a type of system of formal deduction attributed to Gottlob Frege and David Hilbert...
s is that the context is not changed in any of their rules of inference, while both natural deduction
Natural deduction
In logic and proof theory, natural deduction is a kind of proof calculus in which logical reasoning is expressed by inference rules closely related to the "natural" way of reasoning...
and sequent calculus
Sequent calculus
In proof theory and mathematical logic, sequent calculus is a family of formal systems sharing a certain style of inference and certain formal properties. The first sequent calculi, systems LK and LJ, were introduced by Gerhard Gentzen in 1934 as a tool for studying natural deduction in...
contain some context-changing rules. Thus, if we are interested only in the derivability of tautologies, no 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
Deduction theorem
In mathematical logic, the deduction theorem is a metatheorem of first-order logic. It is a formalization of the common proof technique in which an implication A → B is proved by assuming A and then proving B from this assumption. The deduction theorem explains why proofs of conditional...
) must be proven as a metatheorem
Metatheorem
In logic, a metatheorem is a statement about a formal system proven in a metalanguage. Unlike theorems proved within a given formal system, a metatheorem is proved within a metatheory, and may reference concepts that are present in the metatheory but not the object theory.- Discussion :A formal...
in Hilbert-style deduction system
Hilbert-style deduction system
In logic, especially mathematical logic, a Hilbert system, sometimes called Hilbert calculus or Hilbert–Ackermann system, is a type of system of formal deduction attributed to Gottlob Frege and David Hilbert...
, while it can be declared explicitly as a rule of inference
Rule of inference
In logic, a rule of inference, inference rule, or transformation rule is the act of drawing a conclusion based on the form of premises interpreted as a function which takes premises, analyses their syntax, and returns a conclusion...
in natural deduction
Natural deduction
In logic and proof theory, natural deduction is a kind of proof calculus in which logical reasoning is expressed by inference rules closely related to the "natural" way of reasoning...
.
In type theory
Type theory
In mathematics, logic and computer science, type theory is any of several formal systems that can serve as alternatives to naive set theory, or the study of such formalisms in general...
, some analogous notions are used as in mathematical logic
Mathematical logic
Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...
(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
Simply typed lambda calculus
The simply typed lambda calculus , a formof type theory, is a typed interpretation of the lambda calculus with only one type constructor: \to that builds function types. It is the canonical and simplest example of a typed lambda calculus...
.