next up previous contents
Next: Universal quantifier elimination Up: Quantifier reasoning Previous: Quantifier reasoning   Contents

Universal quantifier introduction

When they need to prove a universally quantified formula, say \bgroup\color{red}$\forall \; x \, . \, \mbox{\em Even}(x) \vee \mbox{\em Odd}(x)$\egroup, mathematicians often reason as follows:

\begin{displaymath}\bgroup\color{red}\mbox{Consider an arbitrary $x$. Then $\cdots$}\egroup\end{displaymath}

where \bgroup\color{red}$\cdots$\egroup is a proof that establishes the claim for \bgroup\color{red}$x$\egroup--in this case a proof of the disjunction \bgroup\color{red}$\mbox{\em Even}(x) \vee \mbox{\em Odd}(x)$\egroup. The adjective ``arbitrary'' can be metaphysically misleading (leading one to believe in fictitious ``arbitrary'' objects), but nevertheless serves an important purpose: to emphasize that no special assumptions about \bgroup\color{red}$x$\egroup can be made. If we analyze this reasoning in terms of programming language theory, we see that what is inside the dots \bgroup\color{red}$\cdots$\egroup is essentially a method for proving that something is even or odd, parameterized over \bgroup\color{red}$x$\egroup. That is, a method that takes any given term \bgroup\color{red}$x$\egroup and produces the conclusion \bgroup\color{red}$\mbox{\em Even}(x) \vee \mbox{\em Odd}(x)$\egroup. To make sure that no special assumptions are made about \bgroup\color{red}$x$\egroup, we need to apply this method to a fresh variable \bgroup\color{red}$v$\egroup: a newly generated term that has not been seen or used before. If that succeeds in deriving \bgroup\color{red}$\mbox{\em Even}(v) \vee \mbox{\em Odd}(v)$\egroup then we are entitled to conclude that everything has this property (of being even or odd). This idea can be succinctly captured by the following semantics:
\bgroup\color{red}$\;\;$\egroup \bgroup\color{red}$\mbox{$\beta$}\mbox{$\:\vdash\:$}\{x \mapsto v\}D \mbox{$\:\longrightarrow\;$}F$\egroup \bgroup\color{red}$\;$\egroup
\bgroup\color{red}$\;\:$\egroup
\bgroup\color{red}$\;\;$\egroup
\bgroup\color{red}$\mbox{$\beta$}\mbox{$\:\vdash\:$}\mbox{\tt pick-any } x\,\; D \mbox{$\:\longrightarrow\;$}(\forall v) F$\egroup
provided \bgroup\color{red}$v$\egroup does not occur in \bgroup\color{red}$\beta$\egroup or in \bgroup\color{red}$D$\egroup.
\bgroup\color{red}$\;$\egroup
The proviso that \bgroup\color{red}$v$\egroup must not occur in \bgroup\color{red}$\beta$\egroup or in \bgroup\color{red}$D$\egroup ensures that \bgroup\color{red}$v$\egroup is fresh. For example, consider the proof
pick-any x
 ref x
To evaluate this proof in a given assumption base, we generate a fresh variable, say v85, and evaluate the body ref x with every free occurrence of x replaced by v85. Hence, in this case we will evaluate ref v85. According to the semantics of ref, the rule application ref v85 will yield the conclusion v85 = v85. Having finished evaluating the (renamed) body, the semantics of pick-any tell us that we can now produce the universal quantification (forall v85 (v85 = v85)) as the final conclusion of the entire pick-any. To make the result more readable, NDL will display this conclusion as (forall x (x = x)) instead of (forall v85 (v85 = v85)). That is, it will alphabetically rename the result, replacing the fresh variable with the actual eigenvariable that was used (in this case x). This is sound because recall that NDL treats alphabetically equivalent formulas as identical, so that

\begin{displaymath}\bgroup\color{red}\mbox{\tt (forall v85 (v85 = v85))}\egroup\end{displaymath}

and

\begin{displaymath}\bgroup\color{red}\mbox{\tt (forall x (x = x))}\egroup\end{displaymath}

mean the exact same thing. In summary, if you evaluate this proof, NDL will reply with

\begin{displaymath}\bgroup\color{red}\mbox{\tt Theorem:}\;\mbox{\tt (forall x (x = x))}.\egroup\end{displaymath}


next up previous contents
Next: Universal quantifier elimination Up: Quantifier reasoning Previous: Quantifier reasoning   Contents
2004-08-06