Well-founded sets revisited

Well-founded sets revisited

In the following

$\left( {C, < }\right)$ is a nonempty partially ordered set.

$x,y\;$ are elements of $C$ ,

$\mathfrak{S}$ is a subset of $c$

$P,Q$ are predicates on $C$ ,

where $S$ and $P$ are coupled by

(0) ${P}_{X} \equiv \neg x \in S$ ,or $S = { x|{\neg Px}}$ .

As a result we have

(1) $S = \phi \equiv \left( {\underline{A} \times :{P}_{X}}\right)$

" $x$ is a minimal element of ${S}^{\prime \prime }$ means

$x \in S \land \left( {\underline{A}y : y < x : y \in S}\right)$

"C is well-founded" means "any nonempty sub-

Theorem 0 " $C$ is well-founded" $\equiv$ "mathematical induction over $C$ is valid".

Proof

" $C$ is well-founded

$= {$ definitiois of well-foundedness and minimal element $}$

$\left( {A,S}\right) : S \neq \phi = 1$

$$ (E \times :: x \in S \land (A y: y < x: \neg y \in S))) $$

$= {$ predicate calculus, ${de}\;{Morgan}$ in particular $}$

$$ (\underline {{A}} S:: S = \varnothing \equiv $$

$$ (\underline {{A}} x: \neg x \in S \vee (\underline {{E}} y: y < x: y \in S))) $$

$= {$ renaming the dummy with (0) and (1) $}$

$$ (A P: (A X: P X) \equiv $$

$$ (\underline {{A}} x: P x \vee (E y: y < x: \neg P y)) $$

$= {$ definition of mathematical induction $}$

"mathematical induction over $C$ is valid".

(End of Proof.)

Theorem 1 "C is well-founded" $\equiv \left( {\underline{A}x : ?Qx}\right)$ , where Q is defined as the strongest solution

of

(3) $Q : \left( {\underline{A}x\therefore Qx}\right) \vee \left( {{E}_{y} : y < x : {7Qy}}\right)$

Note. The above Q is usually interpreted as:

[\text{Q} \equiv \text{each}\text{descending chain starting with}x]

is of finite length.

The following proof does not appeal to this interpretation. (End of Note.)

Proof Rewriting (3) as

$$ Q: (\underline {{A}} x:: (\underline {{A}} y: y < x: Q y) \Rightarrow Q x) $$

and recognizing that the antecedent is a mono-

Tarski- that (3) has a strongest solution.

" $C$ is well-founded

$$ \Rightarrow {\mathrm {T h e o r e m} 0 } $$

$$ \begin{array}{l} (\underline {{A}} x: Q x) \equiv (\underline {{A}} x: Q x \vee (E y: y < x: \neg Q y)) \ = {Q i s a s o l u t i o n o f (3) } \ (\underline {{A}} x: \underline {{Q}} x) \ \end{array} $$

$$ " C i s n o t w e l l - f o u n d e d " $$

$$ \Rightarrow {\mathrm {d e f i n i t i o n o f w e l l - f o u n d e d n e s s}, (2); \mathrm {f o r s o m e} S } $$

$$ S \neq \varnothing \land (\underline {{A}} x: \neg x \in S \lor (\underline {{E}} y: y < x: y \in S)) $$

$$ = {\mathrm {f o r} P, \mathrm {a s d e f i n e d b y (0) , a n d (1)} } $$

$$ \lnot (\underline {{A}} x: \underline {{P}} x) \land (\underline {{A}} x: \underline {{P}} x \lor (\underline {{E}} y: y < x: \neg P y)) $$

$$ \begin{array}{l} = {(3) } \ i (\underline {{A}} x: P _ {x}) \wedge “ P s o l v e s (3) ” \ \Rightarrow {Q i s t h e s t r o n g e s t s o l u t i o n o f (3) } \ \lnot (\underline {{A}} x:: Q x) \ \end{array} $$

(End of Proof.)

The above proof was designed in the presence of W.M. Turshi and here recorded under super- vision of A.J.M. van Gasteren.

London, 13 June 1984

Plataanstraat 5

5671 AL NUENEN

The Netherlands

p r o p. d r. Eds g e r W. D y j ksha

Burroughs Research Fellow