Is this the correct way to prove $\exists y \forall x (P(x) \vee Q(y)) \equiv \forall xP(x) \vee \exists x Q(x)$?

$\exists y \forall x (P(x) \vee Q(y)) \equiv \forall xP(x) \vee \exists x Q(x)$

If the LHS is true, then there are two cases: P(x) is true, in which case $\forall$ P(x) is true and the RHS is true, and Q(y) is true, in which case $\exists$ x Q(x) is true and the RHS is true.

If the RHS is true, then there are two cases $\forall$ P(x) is true, in which case P(x) is true and the LHS is true, and $\exists$ x Q(x) is true, in which case Q(y) is true and the LHS is true.

-

– MJD Oct 31 '12 at 3:49

1 Answer

I think the easiest way to prove this is to use the rules for manipulating quantifiers. Starting with the LHS, we have

$$\begin{align*} \exists y[\forall x(P(x)\vee Q(y))] &\equiv \exists y [\forall x P(x) \vee \forall x Q(y)]\\ &\equiv \exists y [\forall x P(x) \vee Q(y)] \\ &\equiv \exists y\forall x P(x) \vee \exists y Q(y) \\ &\equiv \forall xP(x) \vee \exists yQ(y) \\ &\equiv \forall xP(x) \vee \exists xQ(x). \end{align*}$$

This is because $\mathbf{Q}\mathbf{v}(\mathbf{P}(\mathbf{v})\ \mathbf{B}\ \phi)\equiv (\mathbf{Q}\mathbf{v}\mathbf{P}(\mathbf{v}))\ \mathbf{B}\ \phi$ is valid where $\mathbf{Q}$ is a quantifier, $\mathbf{v}$ is a variable, $\mathbf{P}$ is a predicate, $\mathbf{B}$ is either the conjunction or disjunction operator, and $\phi$ is a formula where $\mathbf{v}$ isn't free.

For your proof, when assuming the LHS, splitting directly into cases isn't possible because the disjunction is "trapped" by the quantifiers. We must say: let $c$ be an object such that $\forall x(P(x)\vee Q(c))$ is true (we know such a $c$ exists because of the assumption). Now let $a$ be an arbitrary object. We know $P(a)\vee Q(c)$ is true. Suppose now that $Q(c)$ is true. Then certainly $\exists xQ(x)$. Now suppose $P(a)$ is true. Since $a$ was arbitrary, $\forall xP(x)$ is true.

-

shouldn't it be $P(c) \vee Q(c)$? – Gladstone Asder Oct 31 '12 at 17:29
{"extraction_info": {"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 24, "mathjax_display_tex": 1, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0}, "config": {"markdown_headings": false, "markdown_code": true, "boilerplate_config": {"ratio_threshold": 0.18, "absolute_threshold": 10, "end_threshold": 15, "enable": true}, "remove_buttons": true, "remove_image_figures": true, "remove_link_clusters": true, "table_config": {"min_rows": 2, "min_cols": 3, "format": "github"}, "remove_chinese": true, "remove_edit_buttons": true, "extract_latex": true}, "english_confidence": 0.9503745436668396, "perplexity_flag": "head"}