True propositions and proofs

One of the most interesting properties of a proposition is whether the thought it expresses is true. Here is a more concrete way to say this. To grasp the sense of a proposition is to understand what counts as evidence for its truth. To know whether a proposition is true, we must find evidence for it. Trying to find evidence is a mathematical task, and it is an abstract activity. ¹²

The evidence for an assertion is called a proof. Proving a proposition is the way of knowing it.¹³ When we judge that an expression is a proposition, we specify what counts as a proof of it. For the propositions $\top, \perp (P \& Q), (P \vee Q), \exists x\!:\!A.\ P(x)$ it is easy to specify this. To prove $\top$ we could cite an axiom, that is, we say it is self-evident. As we said before, $\perp$ has no proofs. To prove $(P \& Q)$ we prove P and prove Q. To prove $(P \vee Q)$ we either prove P or prove Q. To prove $\exists x\!:\!A.\ P(x)$ we exhibit an element a of A and prove P(a).

To say what it means to prove $(P \Rightarrow Q)$ we need to understand logical consequence or what is the same in this article, hypothetical proof. We write this as hypothetical judgmenthypothetical judgement $P \vdash Q$ which reads, assuming P is true, we can prove that Q is. What this means is that if we have a proof p of P, then we can build a proof qof Q using p.

To discuss nested implications such as $P \Rightarrow(Q \Rightarrow P)$ we need to understand hypothetical judgments of the form $P_1, \ldots, P_n \vdash Q$which means that assuming we have proofs p_i of P_i, we can find a proof q of Q.

To prove $\forall x\!:\!A. P(x)$ we need the hypothetical judgment $x\!:\!A \vdash P(x)$ which says that given any a of type A, we can find a proof of P(a). Combining these two forms of hypothetical judgments we will need to consider $H_1, \ldots, H_n \vdash P$ where H_i can be either a proposition or a type declaration such as $x\!:\!A$.

This account of provability gives what we call a semantics of evidence. Depending on the interpretation of the functionality, judgments like $P \vdash Q$ or $x\!:\!A \vdash P(x)$ we can explain both classical and constructive logic in this way. These ideas will become clearer as we proceed.

In general, there is no systematic way to search for a proof. Indeed, the notion of proof we have in mind is not for any fixed formal system of mathematics. We are interested mainly in open-ended notions. Like the concept of a proposition, the concept of a proof is inexhaustible or open or creative. By [52] and [111] we know that for any consistent closed non-trivial formal system, we can systematically enlarge it, namely by adding a rule asserting its consistency or giving a definition of truth for that system.

For the collection of pure abstract propositions, there is a systematic way to search for a proof. If we want to describe this procedure, then it is necessary to have a representation of propositions as data that lets us access their structure. We can do this with the inductive definition of propositions given next, but it is more natural to build a representation that directly expresses the linguistic structures that we use when writing and manipulating formulas. This is the traditional approach to the study of logic and provability. We take it up in the subsections on Formulas and Formal Proofs.