Why is this proposition provable and its converse not?

I found this proposition and don’t see exactly as to why it is true and even more so, why the converse is false:

Proposition 1. The equivalence between the proposition $z \in D$ and the proposition $(\exists x \in D)x = z$ is provable from the definitory equations of the existential quantifier and of the equality relation. If $D = \{t_{1},t_{2},…t_{n}\}$, the sequent
$z = t_{1} \vee z = t_{2} \vee z \vee … z = t_{n} \vdash z \in D$ is provable from the definition of the additive disjunction $\vee$.

The converse sequent $z \in D \vdash z = t_{1} \vee z = t_{2} \vee … z = t_{n}$ is not provable.

The author goes on to say: “We adopt the intuitionistic interpretation of disjunction. With respect to it, one can characterize a particular class of finite sets”

On the first part of the proposition, well I am not sure what the point is as if we take an element z in D, then we could just call this element x and hence this x = z. Is there something more to this? On the second part of Proposition 1 since $z = \text{ some } t \in D$ since t is in the set of axioms and $t = z$, then $t \vdash z$ as z is derivable from t.

For the converse if $z \in D$ then why wouldn’t z = some $t \in D$? Is this because of the Incompleteness theorem? That perhaps there D as a set of axioms has some consequence which can not be proven by the set of axioms in D? Or perhaps I am way off here.

Any ideas?

Thanks,

Brian

Solutions Collecting From Web of "Why is this proposition provable and its converse not?"

This is most of an answer, with an omission at the end:

Intuitionistically, to prove $s \vee t$ you must exhibit either a proof of $s$ or a proof of $t$. Hence, you can’t prove $z = t_1 \vee z = t_2 \vee \dots$ unless you have some method of discovering which $t_i$ was equal to $z$.

Now, if you had decidable equality, of the form $(\forall x)(\forall y)(x = y \vee x \not= y)$, then you could use that to “check” each $t_i$ for equality with $z$. I don’t know how you would use the fact that $D = \{t_1 \dots t_n\}$ to show that this process must eventually succeed, since I don’t know how that set equality would be interpreted as a logical statement.

The deeper question here is what the author means by
$$
D = \{ t_1, \ldots, t_n\}.
$$
The normal definition of this is:
$$
D = \{t_1,\ldots,t_n\} \qquad \text{means}\qquad (\forall z)[ z \in D \leftrightarrow z = t_1 \lor \cdots \lor z = t_n].
$$
But, according to that definition, one does have an intuitionistic proof that
$$
x \in D \leftrightarrow x = t_1 \lor \cdots \lor x = t_n
$$
because this follows immediately from the definition of $D$.

Therefore, until it is clarified what the author means by “$D = \{ t_1, \ldots, t_n\}$”, very little can be said.