Validity Theorem

Definition A proof is valid if the goal is true when the premises are.

Theorem: Proofs are valid.

Pf: By induction on level, n, and for each n by induction on the subproof relation.

Let $\Delta = (s, r, \Delta_1, \ldots, \Delta_k)$ be a proof whose premises are true. Let $\bar{\Delta} = (\Delta_1, \ldots, \Delta_k)$.

Consider the cases for rule r.

1.

$r=\bullet, s$ is a premise, hence true.

2.

r is a primitive rule, then s is true by validity of the primitive rules.

3.

r is a tactic with term t. Then t represents a subproof $\Delta'$ which is valid by induction. The premises of $\Delta'$ are roots of $\bar{\Delta}$, they are true, so the goal of $\Delta'$ is, which is s.

4.

r is Refl i, t. So the goal of $\Delta_1$ is true by induction. This means that there is a proof $\Delta'$ of level less than i; thus $\Delta'$ is valid. The premises of $\Delta'$ are the roots of $\Delta_2, \ldots, \Delta_k$, hence true, so s is true as well. QED.