The evidence for an assertion is called a proof. Proving a proposition
is the way of knowing it.13 When we judge that
an expression is a proposition, we specify what counts as a proof of it. For
the propositions
it
is easy to specify this. To prove
we could cite an axiom, that is, we
say it is self-evident. As we said before,
has no proofs. To
prove
we prove P and prove Q. To prove
we either
prove P or prove Q. To prove
we exhibit an
element a of A and prove P(a).
To say what it means to prove
we need to understand logical
consequence or what is the same in this article, hypothetical proof. We
write this as hypothetical judgmenthypothetical judgement
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
we need
to understand hypothetical judgments of the form
which means that assuming we have proofs pi of Pi, we can find a proof
q of Q.
To prove
we need the hypothetical judgment
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
where Hi can be either a proposition or
a type declaration such as
.
This account of provability gives what we call a semantics of evidence.
Depending on the interpretation of the functionality, judgments like
or
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.