Judgments and proofs

Knowledge arises when we judge a proposition to be true. A proposition Pbecomes an assertionassertion when we judge it to be true or assert it. In Principia this judgment is called an assertion and is written $\vdash P$.

Normally we assert a proposition when we know it to be true, but people also make so-called ``blind assertions'' which are made without this knowledge but happen to be true because someone else knows this or the person ``speaking blindly'' discovers it later. (These ``blind assertions'' normally make a person, especially students in exams, anxious.)

Assertions are not the only form of knowledge. We follow Per Martin-Löf [80] and speak also of judgments of the form $P \in Prop$ that we discussed above. These are typing judgmentstyping judgment. They also convey knowledge and need to be made evident, but we consider them as a different category of knowledge from assertions. Indeed, we see that knowing these judgments is part of knowing truth judgments because we must know that the object P we are asserting is a proposition before (or as) we judge it to be true.¹¹

In section 2.1 we treated this notion in the background with the notation $P \in Prop$, $P \in A \rightarrow Prop$, without explaining judgments in general. In most logic textbooks this judgment is reduced to a question of correct parsing of formulas, i.e., is made syntactic and is thus prior to truth. But we follow Russell and Martin-Löf in believing it to be a semantic notion that can be treated in other ways when we formalize a theory.

For the predicate calculus, we leave most of these typing judgments implicit and adopt the usual convention that all the formulas we examine represent well-formed propositions. In the full typed logic this condition cannot be checked syntactically, and explicit typing judgments must be made.

In general, to make a judgment is to know it or for it to be evident. It does not make sense for a judgment to be evident without a person knowing it. However, we recognize that there are propositions which are true but were not known at a previous time. So at any time there are propositions which are not known, but will be asserted in the future.