2

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

Relative0
  • 1,419
  • 2
    I suspect it's "We adopt the intuitionistic interpretation of disjunction". Intuitionist logic is, despite its name, rather counterintuitive. – Daniel Fischer Jul 29 '13 at 23:19
  • 1
    From the context, I have to presume that the sequent $ z \in D \vdash z=t_1 \vee=t_2\vee...z=t_n$ is not provable in this intuitionistic logic because such a proof would require enumerating all the elements of $D$ and comparing each of them to $z$. $\exists x$ does not merely mean that there is an $x$. It means, "there is an $x$ and we have found it." – nomen Jul 29 '13 at 23:23
  • Could you name the book and author you are referring to? That will help others explain what is going on by looking at the context of the statement. – Carl Mummert Jul 30 '13 at 12:13
  • I apologize for the delay in responding. @Carl, it is a paper: http://www.math.unipd.it/~giulia/pdf/battilottiQI13july.pdf
    Definition 1     – Relative0 Aug 08 '13 at 21:37
  • @nomen. I think I see what your saying. Helps a lot thanks! I can see that $z = t_{1} \vee z = t_{2} \vee z \vee ... z = t_{n} \vdash z \in D$ as for some $t_i¦ t_i \in D$ there would be some element $z \in D$ such that $t_i = z$. That is that we can eventually (in finite time) find a $t_i$ since D is finite. I am wondering though, since the papers author has a finite D, wouldn't we eventually find a $t_i$ such that $z \in D \vdash z = t_{i}$ where $t_{i} = z \vdash z $ which is true? This is of course restricting to the finite case. – Relative0 Aug 09 '13 at 11:16

2 Answers2

1

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.

Ben Millwood
  • 14,211
1

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.

Carl Mummert
  • 81,604