Judgments
https://en.wikipedia.org/wiki/Judgment_(mathematical_logic)
A judgment or assertion is a statement in the metalanguage. In general, a judgment may be any inductively definable assertion in the metatheory.
For example, typical judgments in first-order logic would be that a string is a well-formed formula, 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.
Judgments are used in formalizing deduction systems:
a logical axiom expresses a judgment
premises of a rule of inference are formed as a sequence of judgments
their conclusion is a judgment
thus, hypotheses and conclusions of proofs are judgments as well
A judgment is an evident object of knowledge, if one has a proof of it. In mathematical logic however, evidence is often not directly observable, but rather deduced from more basic judgments - this process of deduction is what constitutes a proof.
The most important judgments in logic are of the form "A is true", where A stands for any proposition; therefore, the truth of a judgment depends on a more primitive judgment, that which asserts that "A is a proposition".
Of course, if A is not a proposition, the logic is outta window, so we'll assume that we're dealing with freaking propositions, that are syntactically valid and obtained by translating declarative statements with a truth value from some natural language.
Besides the everlasting judgement "A is true", many other judgments have been studied, including:
"A is false" in classical logic
"A is true at time t" in temporal logic
"A is necessarily true" or "A is possibly true" in modal logic
"A is achievable from the available resources" in linear logic
"program M has type τ" in type theory
References
https://en.wikipedia.org/wiki/Judgment_(mathematical_logic) https://en.wikipedia.org/wiki/Natural_deduction https://en.wikipedia.org/wiki/Rule_of_inference https://en.wikipedia.org/wiki/Sequent_calculus
Last updated