Mathematical induction and universal quantification

Mathematical induction and universal quantification

In the following, $x$ and ${x}^{\prime }$ range over the same domain; similarly, $y$ and ${y}^{\prime }$ range over the same domain. Moreover, $<$ is a well-founded relation on the domain of $x$ ,i.e. for any $P$

(0) $\left( {\underline{A}x\because {P}{.}x}\right) \equiv \left( {\underline{A}x\because {P}{.}x \Leftarrow \left( {\underline{A}{x}!\because {x}^{\prime }\prec x : {P}_{.}{x}^{\prime }}\right) }\right)$

Consider now the obligation to prove for some

(1) $\left( {\underline{A} \times ,y : \mathcal{R} \cdot x \cdot y}\right)$

Two approaches are now possible.

(1)

$$ \begin{array}{l} = \frac {{\mathrm {n e s h i n g} }}{(\underline {{A}} y : (\underline {{A}} x : \mathbf {R} . x . y))} \ \begin{array}{r l} & {= {\underline {{(0)}} \mathrm {w i t h} P. x := R. x. y; \mathrm {u n n e s t i n g} }} \ & {\quad (\underline {{A}} x, y: \mathbb {R}. x. y \Leftarrow (\underline {{A}} x ^ {\prime}: x ^ {\prime} < x: \mathbb {R}. x ^ {\prime}. y))} \end{array} \ \end{array} $$

(ii) (i)

$$ \begin{array}{l} = \begin{array}{l} {\mathrm {n e s t i n g} } \ (\underline {{A}} x: (\underline {{A}} y: \mathbb {R}. x. y)) \end{array} \ \begin{array}{r l} & {= {\underline {{(0)}} \mathrm {w i t h} P _ {x} := (\underline {{A}} y: \mathbb {R}. x. y); \mathrm {r e n a m i n g d u m m y} }} \ & {\quad (\underline {{A}} x: (\underline {{A}} y: \mathbb {R}. x. y) \Leftarrow (\underline {{A}} x ^ {\prime}: x ^ {\prime} < x; (\underline {{A}} y ^ {\prime}: \mathbb {R}. x ^ {\prime}. y ^ {\prime})))} \ & {= {\Leftarrow Q \mathrm {d i s t r i b u t e s o v e r} \underline {{A}}; \mathrm {u n n e s t i n g} }} \ & {\quad (\underline {{A}} x, y: \mathbb {R}. x. y \Leftarrow (\underline {{A}} x ^ {\prime}: x ^ {\prime} < x; (\underline {{A}} y ^ {\prime}: \mathbb {R}. x ^ {\prime}. y ^ {\prime})) }} \end{array} \ \end{array} $$

Method (i) gives a shorter formula, but ends with a stronger proof obligation than method (ii),

which, therefore, is more powerful. The message was driven home to me at last week's session of the ETAC, where we considered for R.x.y

$$ i x < y \vee i y < x $$

Approach (i) leads one into a dead end; approach (ii) leads one to observe for any $x,y$

$$ \begin{array}{l} (\underline {{A}} x ^ {\prime}: x ^ {\prime} < x: (\underline {{A}} y ^ {\prime}: \neg x ^ {\prime} < y ^ {\prime} \vee \neg y ^ {\prime} < x ^ {\prime})) \ = {\mathrm {t r a d i n g , u n n e s t i n g} } \ \end{array} $$

$$ (A x ^ {\prime}, y ^ {\prime}: \neg x ^ {\prime} < x \vee \neg x ^ {\prime} < y ^ {\prime} \vee \neg y ^ {\prime} < x ^ {\prime}) $$

$$ \begin{array}{l} \Rightarrow \quad {\mathrm {i n s t a n t i a t e w i t h} x ^ {\prime}, y ^ {\prime} := y, x } \ 7 y < x \vee 7 y < x \vee 7 x < y \ \end{array} $$

$$ \begin{array}{l} = {\mathrm {p r e d . c a l c .} } \ \because x < y \quad \vee \quad \neg y < x. \ \end{array} $$

$$ N u e n e n, 1 0 J u l y 1 9 9 0 $$

$$ \begin{array}{l} p r o f. d r. E d s g e r W. D y k s t r a \ \mathrm {D e p a r t m e n t o f C o m p u t e r S c i e n c e s} \ \mathrm {T h e U n i v e r s i t y o f T e x a s a t A u s t i n} \ A u s t i n, T X 7 8 7 1 2 - 1 1 8 8 \ \end{array} $$

USA