0
$\begingroup$

In an attempt to transform following equivalent definitions of the cartesian product from the first into the second, trying to be rather formal about it:

$$ \forall A : A \in X \times Y \leftrightarrow \exists x \exists y[A = (x, y) \wedge x \in X \wedge y \in Y] \\ \forall x \forall y : (x, y) \in X \times Y \leftrightarrow x \in X \wedge y \in Y $$

My attempts led to the following steps: $$ \begin{align} &\text{0. Suppose} &\Longrightarrow &\forall A : A \in X \times Y \leftrightarrow \exists x \exists y[A = (x, y) \wedge x \in X \wedge y \in Y] \\ &\text{1. Universal elimination} &\Longrightarrow &A_0 \in X \times Y \leftrightarrow \exists x \exists y[A_0 = (x, y) \wedge x \in X \wedge y \in Y] \\ &\text{2. Existential elimination} &\Longrightarrow &A_0 \in X \times Y \leftrightarrow A_0 = (x_0, y_0) \wedge x_0 \in X \wedge y_0 \in Y \\ &\text{3. Substitution} &\Longrightarrow &(x_0, y_0) \in X \times Y \leftrightarrow A_0 = (x_0, y_0) \wedge x_0 \in X \wedge y_0 \in Y \\ &\text{4. Conjunction elimination} &\Longrightarrow &(x_0, y_0) \in X \times Y \leftrightarrow x_0 \in X \wedge y_0 \in Y \\ &\text{5. Universal generalization} &\Longrightarrow &\forall x \forall y: (x, y) \in X \times Y \leftrightarrow x \in X \wedge y \in Y \\ \end{align} \\ \blacksquare . $$

To me these look and feel like valid steps, however, I failed to find or understand why exactly the universal generalization is indeed allowed in this particular case, considering one of the steps involves existential elimination, which does not guarentee the arbitrariness of $x_0, y_0$.

To justify that intuitively, each arbitrary choice of $A_1 \neq A_2 \rightarrow x_1 \neq x_2$ and $y_1 \neq y_2$ by the definition of an ordered pair, so for each arbitrary choice of $A$ there is a unique pair $(x, y)$ for which the definition holds. This ties the choice of the pair entirely to the choice of the arbitrary element, making it just as arbitrary.

What I wish to know, if at all possible, are three things:

  1. Is this proof even logically correct, or are some of the steps invalid within natural deduction / first order logic?
  2. What is the formal way to define the dependence of the pair on the arbitrary element $A$ and how do we show it's uniquness?
  3. What is the formal way to define the applicability of the universal generalization in this particular case?

I would greatly appreciate it if the answers detailed both the general definitions and the special application for this particular case. Thanks in advance!

If any notation makes the intent of some sentence unclear, or if there are any language-related errors, please comment the specific issue so it can be fixed.

$\endgroup$

1 Answer 1

Reset to default
1
$\begingroup$

To me these look and feel like valid steps, however, I failed to find or understand why exactly the universal generalization is indeed allowed in this particular case, considering one of the steps involves existential elimination, which does not guarentee the arbitrariness of $x_0,y_0$.

Indeed. Instead, you should establish the pair of $(x_0,y_0)$ as arbitrary variables during the universal elimination step, take another pair $(x_1,y_1)$ as a witness for existential instantiation, ... then use conjunction elimination and substitution to dis-include these non-arbitrary variables, so that universal generalization may be applied.

You also need to do this inside a sub-proof --one of two-- to properly handle the biconditional.

  1. Suppose $\hspace16ex∀A:A∈X×Y↔∃x∃y[A=(x,y)∧x∈X∧y∈Y]$
  2. Universal elimination $\hspace4ex(x_0,y_0)∈X×Y↔∃x∃y~[(x_0,y_0)=(x,y)∧x∈X∧y∈Y]$
  3. Suppose $\hspace24ex(x_0,y_0)∈X×Y$
  4. Biconditional elimination $\hspace8ex ∃x∃y~[(x_0,y_0)=(x,y)∧x∈X∧y∈Y]$
  5. Existential instantiation $\hspace9ex(x_0,y_0)=(x_1,y_1)∧x_1∈X∧y_1∈Y$
  6. Conjunction elimination $\hspace9ex(x_0,y_0)=(x_1,y_1)$
  7. Conjunction elimination $\hspace9ex x_1∈X∧y_1∈Y$
  8. Substitution $\hspace20ex x_0∈X∧y_0∈Y$
  9. Conditional introduction $\hspace2ex(x_0,y_0)∈X×Y\to[x_0∈X∧y_0∈Y]$
  10. Suppose $\hspace24ex[x_0∈X∧y_0∈Y]$
  11. Identity $\hspace24ex(x_0,y_0)=(x_0,y_0)$
  12. Conjunction introduction $\hspace8ex(x_0,y_0)=(x_0,y_0)\wedge x_0∈X∧y_0∈Y$
  13. Existential generalization $\hspace8ex\exists x\exists y~[(x_0,y_0)=(x,y)\wedge x∈X∧y∈Y]$
  14. Biconditional elimination $\hspace8ex(x_0,y_0)∈X×Y$
  15. Conditional introduction $\hspace2ex [x_0∈X∧y_0∈Y]\to(x_0,y_0)∈X×Y$
  16. Biconditional introduction $\hspace1ex x_0∈X∧y_0∈Y\leftrightarrow(x_0,y_0)∈X×Y$
  17. Universal generalisation $\hspace3ex \forall x\forall y:[x∈X∧y∈Y\leftrightarrow(x,y)∈X×Y]$

Now, to establish equivalence, suppose $~\forall x\forall y:[x∈X∧y∈Y\leftrightarrow(x,y)∈X×Y]~$ with the intention to derive $~∀A:A∈X×Y↔∃x∃y[A=(x,y)∧x∈X∧y∈Y]~$.

$\endgroup$
1
  • $\begingroup$ Of course, this glosses over some formal details, such as $(x_0,y_0)=(x_1,y_1)$ entailing $x_0=x_1\wedge y_0=y_1$ to justify that substitution step $\endgroup$ Commented Oct 16 at 4:48

You must log in to answer this question.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.