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
 A: 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.
A: 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. 
