... ¹

This work was supported in part by DARPA and the NSF.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... pearl'').²

We have released Version 4.2, see http://www.cs.cornell.edu/Info/Projects/NuPrl/nuprl.html. Version 5 and ``MetaPRL will be available at this World Wide Web site in 1999.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... mathematics.³

Begriffsschrift (``concept script'') analyzed the notion of a proposition into function and argument, introduced the quantifiers, binding, and a theory of identity. This created the entire predicate calculus. Grundgesetze presented a theory of classes based on the comprehension principle and defined the natural numbers in terms of them.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... methods.⁴

I refer to Hilbert's formalist program founded on a finitistic analysis of formal systems to prove their consistency and to justify non-constructive reasoning as a (possibly meaningless) detour justified by the consistency of a formal system.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... Hilbert.⁵

Gödel showed that consistency is not sufficient to justify the detour because there are formulas of number theory such that both P and $\neg P$ can be consistently added (P an unprovable formula).

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... incidental.⁶

Principia is not formal in the modern sense. There are semantic elements in the account which [118,117] objected to. Hilbert made a point of formalizing logic, and we follow in that purely formal tradition.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

...[6]).⁷

This capability can be explored at the Nuprl project home page www.cs.cornell.edu/Info/Projects/NuPrl.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... language.⁸

There are, of course, opposing views; [118,117] was concerned with sentences or formulas as is [99], and we access propositions through specific formulas.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

...Prop.⁹

In topos theory Prop and the true propositions form the subobject classifier, $\Omega$, $\top$ see [10,78,72].

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

...[80,28]).¹⁰

In topos theory this leads to the Grothendieck topos which is definable in our predicative type theory of section 3.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... true.¹¹

In Martin-Löf's theorem these judgments are prior to assertion; in Nuprl they can be simultaneous with assertion.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... activity.¹²

But the consequences of finding a proof or a disproof can be very concrete and very significant. For instance, a purported proof might cause someone to test a device in the belief that it is safe to do so. If the proof is flawed, the device might destroy something of great value.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... it.¹³

When we need to present evidence for a typing judgment, we will incorporate that into our proofs as well and speak of proving a typing. One might want to give this a special name, such as a derivation, but in Nuprl we use the term proof. These typing ``proofs'' never have interesting computational content.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... completeness.¹⁴

[73] tries to express this uniformity using permutations.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

....¹⁵

We will deal later with the issue of equality on Prop, which seems necessary to talk about functions.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... ¹⁷

<

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... ¹⁶

Since we do not study any mapping of formulas to pure propositions, I have not worried about relating elements of P_n and P_m, n<m, by coherence conditions.

Then given $f, g \in {\cal{P}}_n$ and given any lifted connective op, we have $(f\: op\: g) \in {\cal{P}}_n$. Nothing else belongs to ${\cal{P}}_n$. When we want to mention the underlying type, we write ${\cal{P}}_n$ as ${\cal P}(Prop^n \rightarrow Prop)$. Let ${\cal P} = {\displaystyle \bigcup_{n=0}^{\infty}} {\cal P}_n$; these are the pure propositionspure proposition. Note that ${\cal P} = {\displaystyle \bigcup^{\infty}_{n=0}} {\cal P}(Prop^n \rightarrow Prop)$ is inductively defined. The validvalid element elements of ${\cal P}$ are those functions $f \in {\cal P}$ such that for $f \in {\cal P}_n$ and $\bar{{\cal P}}$ any element of $Prop^n, f(\bar{{\cal P}})$ is true. Call these $True({\cal P})$.

Using these concepts we can express the idea of a uniform functional proof. The simplest approach is probably to use a Hilbert style axiomatic base. If we take Heyting's or Kleene's axioms for the intuitionistic propositional calculus, then we can define $Provable_H({\cal P})$ inductively. The completeness theorem we want is then $True({\cal P}) = Provable_H({\cal P})$.

We can use the same technique to define the pure typed propositional functions. First we need to define pure type functionspure typed function ${\cal T}$ as a subset of Type $^n \rightarrow$ Type for $n=1, 2, \ldots$. We take $n \geq 1$ since there are as yet no constant types to include. An example is $t(A, B) = A \times B$. Next we define the typed propositional functions $p : t(\bar{T}) \rightarrow Prop$.

In general we need to consider functions whose inputs are n-tuples of the type

$$(t_1(\bar{T}) \rightarrow Prop) \times \ldots \times (t_n(\bar{T}) \rightarrow Prop)$$

and whose output is a Prop. We do not pursue this topic further here, but when we examine the proof system for typed propositions we will see that it offers a simple way to provide abstract proofs for pure typed propositions that use only rules for the connectives and quantifiers -- say a pure proofpure proof. There are various results suggesting that if there is any proof of these pure propositions, then there is a pure proof. These are completeness results for this typed version of the predicate calculus. We will not prove them here.

	$C_{\top}(\bar{P}) = \mathbf{\top}$	$C_{\bot}(\bar{P}) = \mathbf{\bot}$
	$proj^n_i(\bar{P}) = P_i$	where $\bar{P} = \langle P_1, \ldots, P_n\rangle$ and $1 \leq i \leq n$.

¹⁷#552#>Since we do not study any mapping of formulas to pure propositions, I have not worried about relating elements of P_n and P_m, n<m, by coherence conditions.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... display.¹⁸

This is the mechanism used in Nuprl and HOL; PVS uses multiple conclusion sequents.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... argument.¹⁹

Although if functional equality is defined intensionally, then it is also possible to analyze their structure. Of course, function can also be passed as data.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... axioms.²⁰

``AutomathAutomath is a language which we claim to be suitable for expressing very large parts of mathematics, in such a way that the correctness of the mathematical contents is guaranteed as long as the rules of the grammar are obeyed.'' [40].

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... rules.²¹

The associated tactics are attached as well, see [61,62].

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... axioms.²²

The associated tactics can also enforce global constraints on the theory such as ``decidable type checking.''

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

...metatheory.²³

That it had to be so was part of Hilbert's Program for a formal foundation of mathematics. Classical parts of mathematics were to be considered as ideal elements ultimately justified by constructive means.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... proofs.²⁴

``...we extend the language by proclaiming that proofs of one and the same proposition are always definitionally equal. This extra rule was called `proof irrelevance'....''

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... apparatus.²⁵

This is quite different from taking them to be metamathematical objects as is done in proof theory...a theory that could be formalized in Automath.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

...axiom.²⁶

In Martin-Löf type theory and in Nuprl all proofs of atomic formulas are reduced to a token (axiom in Nuprl). Information that might be needed from the proof is kept only at the metalevel.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

...[24]).²⁷

For Brouwer this language is required by an individual only because of the limits and flaws in his or her mental powers. But for our theory, language is essential to the communication among agents (human and artificial or otherwise) needed to establish public knowledge.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... objects.²⁸

The interplay between expressions and objects has seemed confusing to readers of constructive type theory. In my opinion this arises mainly from the fact that computability considerations cause us to say more about the underlying language than is typical, but the same relationship exists in any formal account of mathematics.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... term.²⁹

Martin-Löf would only need the premise $x\!:\!A \vdash b \in B$ since this means that A is a type. But in his system to prove $x\!:\!A \vdash b \in B$ requires proving $A\ is\_a\ type$.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

...$\lambda(x. x)$.³⁰

We could also use $\lambda(x.\ a)$ for any $a \in A$ if there is one since under the assumption that $x \in 0$, x=a for any a, thus $\lambda(x.\ x)=\lambda(x.\ a)$ in $\mathbf{0} \rightarrow A$.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

....³¹

$i_n(0)=inl^{m-1}(inl(\bullet))$ and $i_m(n)=inl^{m-n}(inr(\bullet))$.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... product.³²

Martin-Löf calls this a dependent sum and writes $\Sigma(x \in A)B$. We think of it as a generalization of $A \times B$ and display the constructor in Nuprl as $x:A \times B$.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.