# 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.