Expressing well-formedness of formulas

The introduction of U₁ combined with the propositions-as-types propositions as types interpretation allows us to express the pure proposition of typed logic more generally, and we can solve the small difficulty of insuring that A+B is a type discussed at the end of section 3.3.

According to the propositions-as-types principle, U₁ represents the type of (small) propositions, and a function $P \in A \rightarrow U_1$ can be interpreted as a propositional function. When we want to stress this logical interpretation, we use the display form Prop₁ for U₁ and generally Prop_i for U_i, and we call Prop_i the proposition of level_i.

We can express general propositions in typed logic by quantifying over Prop_i and U_i. Here are some examples from section 2.

1.

$\forall A, B\!:\!U_1.\: \forall P\!:\!A \rightarrow Prop_1 \forall Q\!:\!B \rightarrow Prop_1.$
$\forall x\!:\!A.\: \forall y\!:\!B.\:(P(x) \& Q(y)) \Leftrightarrow \forall x\!:\!A.\:P(x) \& \forall y\!:\!B.\:Q(y).$

2.

$\forall A, B\!:\!U_1.\: \forall R\!:\!A \times B \rightarrow Prop_1.\:\left(\e... ...A.\: R(x, y) \Rightarrow \forall x\!:\!A.\: \exists y\!:\!B.\: R(x, y)\right).$

At this level of generality, we need to express the well-formedness of typed formulas in the logic rather than as preconditions on the formulas as we did in section 2. This can be accomplished easily using U_i and Prop_i. We incorporate into the rules the conditions necessary for well formedness. For example, in the rule

$\bar{H} \vdash P \Rightarrow Q\ \ \mbox{by}\ \ \Rightarrow\!\!\!R$

$\ \ \ \bar{H}, P \vdash Q$

We need to know that P and Q are propositions. We express this by additional well-formedness subgoals. A complete rule might be

5(160,80)[l] $\bar{H} \vdash P \Rightarrow Q\ \ \mbox{by}\ \ \Rightarrow\!\!R\ \ \mbox{at}\ \ i$
$\ \ \ \bar{H}, P \vdash Q$
$\ \ \ \ \bar{H} \vdash P \in Prop_i$
$\ \ \ \ \bar{H} \vdash Q \in Prop_i$

If we maintain the invariant that whenever we can prove $\bar{H} \vdash a \in A$ then we know A is in a U_i, and whenever we prove $\bar{H} \vdash P$ then we know P is in Prop_i, then we can simplify the rule to this

   $\bar{H} \vdash P \Rightarrow Q\ \ \mbox{by}\ \ \Rightarrow\!\!\!R\ \ \mbox{at}\ \ i$  

$\ \ \ \bar{H}, P \vdash Q$

$\ \ \ \ \bar{H} \vdash P \in Prop_i$

We need to add well-formedness conditions to the following rules, $\vee\!R$, $\Rightarrow\!\!R$, $\forall\!R$, $M\!agic$. We already presented $\Rightarrow\!\!R$; here are the others.

$V\!R$	$\bar{H} \vdash P \vee Q\ \ \mbox{by}\ \ \vee\!\!R_l\ \ \mbox{at}\ \ i$
	$\bar{H} \vdash P$
	$\ \ \ \ \bar{H} \vdash Q \in Prop_i$

The $\vee\!R_r$ case is similar.

$\forall\!R$	$\bar{H} \vdash \forall x\!:\!A.\:P(x)\ \ \mbox{by}\ \ \forall\!R\ \ \mbox{at}\ \ i$
	$\bar{H}, x\!:\!A \vdash P(x)$
	$\ \ \bar{H}\ \ \ \ \ \vdash A \in U_i$
$M\!agic$	$\bar{H} \vdash P \vee \neg P\ \ \mbox{by}\ \ M\!agic\ \ \mbox{at}\ \ i$
	$\ \ \ \ \bar{H} \vdash P \in Prop_i$