next up previous contents
Next: Proof semantics Up: Natural Deduction Language Previous: Formulas   Contents


Proof syntax

The following grammar describes the syntax of NDL proofs:

\begin{eqnarray*}
D & ::= & \mbox{\em RuleApp} \; \vert \; \; \mbox{\tt assume ...
...\mbox{\tt ,} ...\mbox{\tt ,} s_n \;\mbox{\tt\mbox{\tt =}}\; t_n
\end{eqnarray*}



where the syntax of inference rule applications is as follows:

\begin{eqnarray*}
\mbox{\em RuleApp\/} & ::= & \mbox{\tt modus-ponens } F \; \m...
...\tt =}}\; t_2\mbox{\tt ,} t_2\;\mbox{\tt\mbox{\tt =}}\; t_3 \\
\end{eqnarray*}



Proofs of the form $D_1$;$D_2$ are called composite. Proofs of the form assume $F$ $D$ are called conditional (or hypothetical) proofs. The formula $F$ is called the hypothesis and the subproof $D$ is called the body of the conditional proof. We say that the body $D$ represents the scope of the hypothesis $F$. Proofs of the form suppose-absurd $F$ $D$ are called proofs by contradiction. As with conditional proofs, $F$ is called the hypothesis and $D$--the scope of $F$--is called the body. Proofs of the form

\begin{displaymath}\mbox{\tt pick-any } x \;\: D\end{displaymath}

are called universal generalizations. We refer to the variable $x$ as an eigenvariable. Proofs of the form

\begin{displaymath}\mbox{\tt pick-witness } w \;\; \mbox{\tt for} \;\, \mbox{\tt (exists } x \;\: F\mbox{\tt )} \;\: D \\ \end{displaymath}

are called existential specializations. We refer to the variable $w$ as the witness variable; we also say that $w$ is an eigenvariable. Proofs of the form

\begin{displaymath}\mbox{\tt specialize (forall $x$ $F$) with $t$}\end{displaymath}

are called universal specializations, while proofs of the form

\begin{displaymath}\mbox{\tt ex-generalize (exists $x$ $F$) from $t$}\end{displaymath}

are called existential generalizations. Proofs of the form $F \mbox{\tt BY } D$ are called conclusion-annotated proofs. assume, suppose-absurd, pick-any, pick-witness, and BY all bind tighter than the composition operator ;. For example,

\begin{displaymath}\mbox{\tt assume A claim A; claim true}\end{displaymath}

is parsed as the composition of assume A claim A and claim true, not as the hypothetical proof with A as the hypothesis and the composition claim A; claim true as the body. The composition operator ; associates to the right, meaning that

\begin{displaymath}D_1\mbox{\tt ;} D_2 \mbox{\tt ;} D_3\end{displaymath}

is parsed as
\begin{displaymath}
D_1\mbox{\tt ;}(D_2 \mbox{\tt ;} D_3)
\end{displaymath} (+1.1)

and not as
\begin{displaymath}
(D_1\mbox{\tt ;}D_2 )\mbox{\tt ;} D_3
\end{displaymath} (+1.2)

This is an important convention, because proof composition in NDL is not associative--proofs (1.1) and (1.2) do not have the same semantics. This will become more clear in the sequel. These conventions can be overriden by using begin-end pairs. Finally, we note that pick-any and pick-witness are variable-binding constructs; they introduce variable scope. In particular, in a deduction of the form

\begin{displaymath}\mbox{\tt pick-any } x \;\: D\end{displaymath}

we say that the scope of the eigenvariable $x$ is the deduction $D$. And in a deduction of the form

\begin{displaymath}\mbox{\tt pick-witness } w \;\; \mbox{\tt for} \;\, \mbox{\tt (exists } x \;\: F\mbox{\tt )} \;\: D \\ \end{displaymath}

we say that the scope of the witness variable $w$ is $D$. Two deductions that only differ in the names of their bound eigenvariables are condidered identical. For instance, the two deductions
pick-any x
 pick-any y
   assume x = y
     swap x = y
and
pick-any foo1
 pick-any foo2
   assume foo1 = foo2
     swap foo1 = foo2
are considered identical. We can define a notion of substitution (free variable occurrence replacement) for deductions much as we do for formulas. Specifically, for any deduction $D$, variable $x$ and term $t$, we define $\{x \mapsto t\}D$ as the deduction obtained from $D$ by replacing every free occurrence of $x$ inside $D$ by $t$, possibly renaming bound eigenvariables to avoid variable capture. A rigorous definition can be found in the appendix.
next up previous contents
Next: Proof semantics Up: Natural Deduction Language Previous: Formulas   Contents
2004-08-04