formula for defining terms in a finite set

Question

Suppose there's a finite set, $S$ of terms in $\mathbb{R}$ which have the property $P(x)$. Suppose we know how to define the maximum value of the set by the relation, $max(x)$. We also have the relation $<$. Now we want to define every other term in the set. We can have an order of the terms. i.e. $a_1,\ldots, a_n$.

Obviously $a_n(x) = max(x)$.

Nevertheless, I don't understand the following definition (for the other terms):

$$a_i(x) = P(x) \land \forall y\left(x<y \land P(y) \to \bigvee_{j=i+1}^n a_j(y)\right)$$

More specifically, I don't understand the recursion part and be glad for an explanation.

Thanks.

Answer 1

The definition you gave is wrong. Firstly it is syntactically meaningless; what is "$a(j)$" supposed to mean at all? Secondly, even if we replace it by "$a_j(y)$", including all the defining axioms still does not uniquely define what you want, since $a_i(a_n)$ is trivially satisfied for every $i \in \{1..n\}$.

A much easier way is via the following defining axioms:

$a_n(x) = max(x)$.

$a_i(x) = P(x) \land \forall y\ ( a_{i+1}(y) \to x<y \land \neg \exists z\ ( P(z) \land x < z < y ) )$.   [for each $i \in \{1..n-1\}$]

If you really want to stick with the original kind of defining axiom:

$a_i(x) = P(x) \land \forall y\ ( P(y) \to ( x < y \leftrightarrow \bigvee_{j=i+1}^n a_j(y) ) )$.   [for each $i \in \{1..n\}$]

In other words, everything that satisfies $P$ is more than $x$ if and only if it satisfies one of $a_{i+1..n}$.