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


---

# Agent Instructions: Querying This Documentation

If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question.

Perform an HTTP GET request on the current page URL with the `ask` query parameter:

```
GET https://mandober.gitbook.io/math-debrief/300-logic/terms/judgment.md?ask=<question>
```

The question should be specific, self-contained, and written in natural language.
The response will contain a direct answer to the question and relevant excerpts and sources from the documentation.

Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.
