Derivations of membership judgments

We need some method of systematically showing that $a\in A$. Since the definition is inductive, we can resort to some standard presentation method for membership in inductively defined types as discussed in section 2 on Naive Type Theory. The result is a calculus or logic for making what Martin-Löf calls membership judgments. The form of this judgment is

$$\vdash a\in A$$

which is read: we know that a belongs to type A.

The definition of

$\vdash \lambda(x.b) \in A\rightarrow B$

suggest that we also want hypothetical judgments, such as

$x:A \vdash b\in B$.

In general, a sequent

$x_1:A_1, x_2:A_2, \ldots, x_n:A_n \vdash g\in G$

means: if A₁ is a type, x₁ an element, A₂ a type for x₁ in $A_1, \ldots$, then G is a type with element g.

Rules

We present the inductive definition in terms of rules for sequents. We organize them top-down, e. g.

Nuprl supports a problem-solving style that is top-down or goal-driven (like Prolog and $\lambda$Prolog [38]). In this style, the goals is

$\vdash G$ thought of as $\vdash ?\in G$

starting with G we try to synthesize g.

Rules in this style look like

$$\vdash A\rightarrow B D0 \, [new x] x:A\vdash B$$

The rule name Di means decompose hypothesis i or if i=0 decompose the conclusion.

Sample Proof

$$\vdash A\rightarrow\mbox{\bf 1} \mbox{by} D0 [new y]$$

Extract $\lambda(y.\bullet)$ as element.

Proof Trees

In Nuprl, derivations are organized into proof trees. Here is a diagram.

$$\vdash G by r_0$$

$$H_1 \vdash G_1 by r_1 \hspace*{1in} H_2\vdash G_2 by r_2$$

$$H_{11}\vdash G_{11} \hspace*{.4in} H_{12}\vdash G_{12} \hspace*{1in} H_{21}\vdash G_{21} by r_{21}$$

We can define these trees inductively in Naive Type Theory as follows:

sequent = (term list) $\times$ term justification = {rule names} + ... proof = sequent $\times$ justification $\times$ proof list