next up previous
Next: Heyting's semantics Up: Typed logic Previous: Theory structure

Proofs as objects

The notion of proof plays a fundamental role in logic as we have seen here. Hilbert's proof theory is a study of proofs, and for philosophical reasons he conceived of it as a constructive theory, and a metatheory.23 Given the central role of proofs in all of mathematics, it is not a great leap to begin thinking about proofs as mathematical objects with the same ``reality'' as numbers. This viewpoint is central to intuitionistic and constructive mathematics, and it seems to be coherent classically as well. De Bruijn designed the Automath formalisms around notion of formal proofs as objects, and ordinary objects such as functions could depend on proofs. In order to treat what was called classical mathematics he had to add a principle of irrelevance of proofsirrelevance of proofs. 24 However, to bring proof expressions fully into the mathematics as objects means more than allowing them into the language. As the proof irrelevance principle shows, they can be regarded as part of the underlying linguistic apparatus.25 To make proofs explicit objects with a referential character, we must define equality on them (the kind of equality called book equality in Automath as opposed to definitional equality which holds for all terms whether referential or not).

There are two sources to guide the discovery of equality rules for proof objects.proof equality We can turn to intuitionistic mathematics and its semantics for the logical operators or we can look to proof theory and the reduction (or normalization rules). Neither account is definitive for classically conceived mathematics. In the case of using intuitionistic reasoning as a guide, we must handle classical rules, such as contradiction, or classical axioms like the law of excluded middle ``magic''. There are various ways to approach this with promising results ([4,88,49]). The subject is still very active.

Another approach is suggested by the normalization theorems for classical and constructive logics natural deduction systems, or N-systems (due to [98]), and the body of results on cut elimination in the sequent calculi, or L-systems (arising from [47]). Unfortunately, the results give somewhat conflicting notions of proof equality (c.f. [120,121,114]). It is perhaps premature to suggest the appropriate classical theory, so instead we will sketch the constructive ideas and leave the technical details to section 3 where we will explore carefully Martin-Löf's interpretation in which the computational content of a proof is taken as the object.

Another prerequisite to treating proofs as objects is that we understand the domain of significance, the type of assertions about proofs. This is another point that is not entirely clear. For instance, the views of [69], [105], and [109,110] differ sharply from those of [80,81] and [48].

One of the key points is whether we understand a proof p as a proof of a proposition P, $p\ proves\ P$, or whether provability is a relation on proofs so that Proves(p, P)) is the appropriate relationship. In the latter case there arises the danger of an infinite regress since we will require a proof p' of $(p\ Proves\ P)$. At some level it seems that provability must be a basic judgment, like the typing judgment $t \in T$.

If we start with the view of the relationship $p\ proves\ P$ as a typing judgment, then we are led to the view that the type of a proof is the proposition that it proves. Thus propositions play the role of types according to the propositions_as_types principlepropositions as types.

This principle is designed into Automath (but can be regarded as ``linguistic''), and it is the core of both Martin-Löf type theory ([80,82,81,89]) and Girard type theory ([108,28,50]). According to this principle, a proposition Pis provable (constructivists would say true) iff there is a proof pwhose type is P, that is

\begin{displaymath}\vdash P\ \ \ \ \ \ \mbox{iff}\ \ \ \ \ \ \mbox{for some $p$ ,}\ \vdash p
\in P \end{displaymath}

Indeed, on this interpretation and recognizing that proof expressions p denote proofs, we can see the sequent notation     $\bar{H} \vdash P$by p    as just another way of writing $\bar{H} \vdash p \in P$.

The     $\bar{H} \vdash P$ by p    judgment form can be considered implicit. Attention is focused on P, and the main concern is that there is some inhabitant. The $\bar{H} \vdash p \in P$ form is explicit, and attention is focused on the actual proof. The rules could all be presented in either implicit (logical) form or explicit (type theoretic) form. Consider the $\forall\!L$ and $\forall\!R$ rules, for example. Here is an implicit form.

$H, f\!:\!\forall x\!:\!A.\ P(x,) \bar{J} \vdash G\ \ $ by $\ \
\forall\!L(f; a; y.\ g[y])$
$H, f\!:\!\forall x\!:\!A.\ P(x), \bar{J}, y\!:\!P(a) \vdash G\ \ $ by $\ \ g[y]$
$\bar{H} \vdash A\ \ $ by $\ \ a$
 
$H \vdash\ \forall x\!:\!A.\ P(x)\ \ \ \ $ by $\ \ \forall\!R(x.\ p[x])$
$\ \ \ \ \ H, x\!:\!A \vdash P(x)\ \ $ by $\ \ p[x]$
Here is the explicit form of the $\forall\!L$ rule.
$\bar{H}, f\!:\!\forall x\!:\!A.\ P(x), \bar{J} \vdash \forall\!L(f; a;
y.\ g[y]) \in G$
$\bar{H}, f\!:\!\forall x\!:\!A.\ P(x), \bar{J}, y\!:\!P(a) \vdash
g[y] \in G$
$\bar{H} \vdash a
\in A$

We will discover in section 3.7 that there is a reasonable notion of reduction on proof expressions (which can either be considered as computation or definitional equality) and that this gives rise to a minimal concept of equality on proofs that is sufficient to give them the status of mathematical objects.


next up previous
Next: Heyting's semantics Up: Typed logic Previous: Theory structure
James Wallis
1999-09-17