Is the System Equivalent to the Expressed Conditions?

[mathmari]

Hey!

Suppose we have the system $$\exists y (G(y)=f \land G_1(y)\neq g_1 \land G_2(y)\neq g_2).$$

Is this equivalent to $$\not\exists y \ \left (G(y)=f \land G_1(y)= g_1 \land G_2(y)= g_2) \ \land \ \exists \ x(G(x)=f\right )$$ ?

Or to $$\not\exists y_1, \not\exists y_2 \ \left ((G(y_1)=f \land G_1(y_1)= g_1 ) \land (G(y_2)=f \land G_2(y)= g_2)\right ) \ \land \ \exists x \ \left (G(x)=f\right )$$ ? (Wondering)

 

[mathmari]

When we have one inequation I found in my notes the following:

$$\exists y (G(y)=f \land G_1(y) \neq g) \Leftrightarrow
(\neg (\exists x)(G(x)=f \land G_1(x)=g) \land (\exists y)(G(y)=f)) \lor
(\exists y \exists x (G(x)=f \land G_1(x)=g) \land (G(y)=f \land G_1(y) \neq g))$$ So when we $n$ inequalities do we have the following?

$$\exists y (G(y)=f \land \bigwedge_{j=1}^n G_j(y) \neq g_j) \\ \Leftrightarrow \\
(\neg (\exists x_j)(G(x_j)=f \land G_j(x_j)=g_j) \land (\exists y)(G(y)=f)) \lor
(\exists y \exists x_j (G(x_j)=f \land G_j(x_j)=g_j) \land (G(y)=f \land G_j(y) \neq g))$$ for $j=1, \dots , n$ (Wondering)

 

[Evgeny.Makarov]

Suppose we have the system $$\exists y (G(y)=f \land G_1(y)\neq g_1 \land G_2(y)\neq g_2).$$

The statement $\exists y.\,P(y)\land\neg Q(y)$ is equivalent to a disjunction of two statements. The first is $[\forall x.\,\neg (P(x)\land Q(x))]\land\exists y\,P(y)$. That is, if $P$ and $Q$ are incompatible, then it is enough to find a witness of $P$. The second is $[\exists x.\,P(x)\land Q(x)]\land \exists y.\,P(y)\land\neg Q(y)$. That is, $P$ and $Q$ are compatible, in which case we need to find a witness of the original property, i.e., $P(y)\land\neg Q(y)$.

I don't see how this is useful since the equivalent statement is longer than the original. The point is that if one has to find a witness $y$ of $P(y)\land\neg Q(y)$ and additionally $P$ and $Q$ are incompatible, then it is enough to find a witness of $P$ — this is common sense.

Your situation arises if $P(y)$ is $G(y)=f$ and $Q(y)$ is $Q_1(y)\lor\dots\lor Q_n(y)$ where $Q_i(y)$ is $G_i(y)=g_i$.

 

[mathmari]

When we have $n$ inequalities, is it then as follows?

$$\exists y (G(y)=f \land \bigwedge_{j=1}^n G_j(y) \neq g_j) \\ \iff \\ \neg (\exists x)(G(x)=f \land (\bigvee_{j=1}^n G_j(x)=g_j)) \land (\exists y)(G(y)=f) \lor (\exists y)(\exists x) [(G(x)=f \land (\bigvee_{j=1}^n G_j(x)=g_j) )\land (G(y)=f \land \bigwedge_{j=1}^n G_j(y) \neq g_j)]$$

 

[Evgeny.Makarov]

Yes, this is correct.

 

[mathmari]

And is the formula after the $\iff$ equivalent to $$\neg \left (\exists x \right )\big (\bigvee_{j=1}^n \left (G(x) =f \ \land \ G_j (x) =g_j \right ) \ \land \ \left (\exists y\right )\left (G(y)=f \right ) \big ) \\ \vee \\ \left (\exists y \right ) \left (\exists x \right ) \big [\bigvee_{j=1}^n \left ( G(x) =f \ \land \ G_j (x) =g_j \right ) \ \land \ \left (G(y)=f \ \land \ \bigwedge_{j=1}^n G_j (y) \neq g_j\right ) \big ]$$ ?

 

[Evgeny.Makarov]

In the first member of disjunction, $\exists y\,G(y)=f$ should be outside $\neg\exists x$. Otherwise, yes.

 

[mathmari]

In the first member of disjunction, $\exists y\,G(y)=f$ should be outside $\neg\exists x$. Otherwise, yes.

Ok... In the first member can we change the order of $\neg x$ and $\bigvee$ ?

I mean, is it equivalent to the following?

$$\bigvee_{j=1}^n \big (\neg \left (\exists x \right ) \left (G(x) =f \ \land \ G_j (x) =g_j \right )\big ) \ \land \ \left (\exists y\right )\left (G(y)=f \right ) \\ \vee \\ \left (\exists y \right ) \left (\exists x \right ) \big [\bigvee_{j=1}^n \left ( G(x) =f \ \land \ G_j (x) =g_j \right ) \ \land \ \left (G(y)=f \ \land \ \bigwedge_{j=1}^n G_j (y) \neq g_j\right ) \big ]$$

 

[Evgeny.Makarov]

No. The existential quantifier commutes with disjunction, i.e., $\exists x\,(A\lor B)\iff(\exists x\,A)\lor(\exists x\,B)$, so you can take $\exists$ inside the disjunction. However, the external $\neg$ will turn the disjunction into a conjunction.

 

[mathmari]

Do you mean $$\neg \left (\exists x \right )\big (\bigvee_{j=1}^n \left (G(x) =f \ \land \ G_j (x) =g_j \right )\big ) \ \land \ \left (\exists y\right )\left (G(y)=f \right ) \\ \iff \\ \bigwedge_{j=1}^n \neg \left (\exists x \right )\left (G(x) =f \ \land \ G_j (x) =g_j \right ) \ \land \ \left (\exists y\right )\left (G(y)=f \right ) $$ ?

 

[Evgeny.Makarov]

Yes.

 

[mathmari]

The second member $$ \left (\exists y \right ) \left (\exists x \right ) \big [\bigvee_{j=1}^n \left ( G(x) =f \ \land \ G_j (x) =g_j \right ) \ \land \ \left (G(y)=f \ \land \ \bigwedge_{j=1}^n G_j (y) \neq g_j\right ) \big ]$$ is equivalent to $$ \left (\exists x \right ) \big [\bigvee_{j=1}^n \left ( G(x) =f \ \land \ G_j (x) =g_j \right ) \ \land \ \left (\exists y \right ) \left (G(y)=f \ \land \ \bigwedge_{j=1}^n G_j (y) \neq g_j\right ) \big ]$$ right? At the beginning of the formula we cannot change the order of $\exists x$ and $\bigvee$, can we?

 

[Evgeny.Makarov]

The following equivalences are true.

\[
\begin{align}
\exists x\,\exists y\,A&\iff\exists y\,\exists x\,A\\
\exists x\,(A\land B)&\iff(\exists x\,A)\land B&&\text{if }x\text{ is not free in }B\\
\exists x\,(A\lor B)&\iff(\exists x\,A)\lor(\exists x\,B)\\
\exists x\,A&\iff A&&\text{if }x\text{ is not free in }A
\end{align}
\]

So ideally $\exists x$ and $\exists y$ should be in different members of conjunction. There is no reason for nesting one $\exists$ inside the other. Then the $\exists$ that is in front of the disjunction can be swapped with it.

 

[mathmari]

We have $$ \left (\exists x \right ) \big [\bigvee_{j=1}^n \left ( G(x) =f \ \land \ G_j (x) =g_j \right ) \ \land \ \left (\exists y \right ) \left (G(y)=f \ \land \ \bigwedge_{j=1}^n G_j (y) \neq g_j\right ) \big ]$$

The $\left (\exists x \right )$ isn't for the whole expression, is it? So we don't need the "$\big [$" ... "$\big ]$", right?

The above formula is equivalent to $$ \bigvee_{j=1}^n \left (\exists x \right )\left ( G(x) =f \ \land \ G_j (x) =g_j \right ) \ \land \ \left (\exists y \right ) \left (G(y)=f \ \land \ \bigwedge_{j=1}^n G_j (y) \neq g_j\right ) $$

Is this correct?

 

[Evgeny.Makarov]

We have $$ \left (\exists x \right ) \big [\bigvee_{j=1}^n \left ( G(x) =f \ \land \ G_j (x) =g_j \right ) \ \land \ \left (\exists y \right ) \left (G(y)=f \ \land \ \bigwedge_{j=1}^n G_j (y) \neq g_j\right ) \big ]$$

The $\left (\exists x \right )$ isn't for the whole expression, is it?

As it is written, yes, it is for the whole expression, but using the equivalences I wrote the formula can be converted to where $\exists x$ is only in front of the first member of conjunction.

The above formula is equivalent to $$ \bigvee_{j=1}^n \left (\exists x \right )\left ( G(x) =f \ \land \ G_j (x) =g_j \right ) \ \land \ \left (\exists y \right ) \left (G(y)=f \ \land \ \bigwedge_{j=1}^n G_j (y) \neq g_j\right ) $$

Yes.

 

[mathmari]

So does for each $j=1, \dots , n$ stand that

$$ \left (\exists x \right )\left ( G(x) =f \ \land \ G_j (x) =g_j \right ) \ \land \ \left (\exists y \right ) \left (G(y)=f \ \land \ \bigwedge_{j=1}^n G_j (y) \neq g_j\right ) \\ \iff \\ \left (\exists x \right )\left ( G(x) =f \ \land \ G_j (x) =g_j \right ) \ \land \ \left (\exists y \right ) \left (G(y)=G(x) \ \land \ \bigwedge_{j=1}^n G_j (y) \neq G_j (x)\right )$$

?

 

[Evgeny.Makarov]

For this the scope of $\exists x$ should be extended to the end of the formula.

 

[mathmari]

Ok... Thanks a lot!