# How to prove this logic?

How to prove

$\exists x (P(x) \lor Q(x)) \equiv \exists x P(x) \lor \exists x Q(x)$

I know it is tautology... but how to solve...?

-
Note to reader. The accepted answer is meaningless and does not prove anything. – RParadox Dec 7 '12 at 13:08

$\def\A{\mathfrak A}$First suppose $\exists x. P(x) \lor Q(x)$ holds true in a structure $\A = (A, P^\A, Q^\A)$. That means that there is an element $a \in A$ such that $a \in P^\A$ or $a \in Q^\A$. If $a \in P^\A$ we have that $\A \models \exists x.P(x)$, if $a \in Q^\A$, we have $\A \models \exists x. Q(x)$. Hence in both case $\A \models \exists x\, P(x) \lor \exists x \, Q(x)$.

Now in the other direction if $\A \models \exists x P(x)\lor \exists x Q(x)$, we have that $\A \models \exists x P(x)$ or $\A \models \exists x Q(x)$. So there is some $a \in A$ such that $a \in P^\A$ or $a \in Q^\A$, that gives $\A \models \exists x. P(x) \lor Q(x)$.

As $\A$ was an arbitrary structure, we have $$\models \bigl(\exists x. P(x) \lor Q(x)\bigr) \equiv \bigl(\exists x\, P(x) \lor \exists x\, Q(x)\bigr)$$

-
What is an arbitrary structure? There is no such thing. – RParadox Dec 6 '12 at 14:24
@RParadox: A full wording would be ‘an arbitrary interpretation of a structure whose signature includes unary relation symbols $P$ and $Q$’ or the like, but the short form is perfectly understandable. – Brian M. Scott Dec 10 '12 at 21:36
The usual understanding is that mathematics is based on predicate logic. What logical system has unary relational symbols and allows for proof of predicate logic? This is not rigorous at all. I have given a proof where the system is well defined and each step is given within the system of predicate logic. Here there is no such system. And if it was there would have to be a mistake, because it is isomorphic to PL. Using concepts of higher algebra to prove concepts in PL is, confusing to say the least. How should relations be defined, if we use them to prove elementary theorems of PL... – RParadox Dec 10 '12 at 22:29

If you can show that whenever the LHS is true, then the right hand side must also be true; and that whenever the left-hand side false, then the right hand side must also be false... then you have proven the equivalence.

Two statements are equivalent if whenever one is true, the other is too, and whenever one is false, the other is also. $$(A \equiv B) \iff [(A\land B) \lor (\lnot A \land \lnot B)] \equiv [(A\land B) \lor \lnot(A \lor B)]$$

Put differently $$(A \equiv B)\; \text{ means}\;\; (A \rightarrow B) \land (B \rightarrow A).$$

If you can only show one direction, then it is not an equivalence! (Or if one side can be true, while the other false, then it is not an equivalence!

$\exists x (P(x) \lor Q(x)) \equiv \exists x P(x) \lor \exists x Q(x)$

Equivalently:

$\exists x (P(x) \lor Q(x)) \equiv \exists x P(x) \lor \exists y Q(y)$

• Suppose $\exists x, (P(x) \lor Q(x))$. Then there is some x such that (either $P(x)$ or $Q(x)$).
Hence, it must certainly be true that $\exists x P(x)$ or $\exists yQ(y).$

• Can you argue the other reverse implication is also true?
If $\exists x P(x)$ or $\exists yQ(y)$, ($x$ not necessarily $y$), then in either case, we can correctly infer that $\exists x(P(x) \lor Q(x))$.

-
A and P(x) are very different things. The standard notation is that A, B, C are propositions and P(X) are properties. The first we sometimes refer to as propositional calculus and the second as predicate calculus. – RParadox Dec 6 '12 at 14:06
But here $\exists x. P(x)$ is a proposition. – martini Dec 6 '12 at 14:07
P(x) is the proposition that X has the property P. But we are very close to the axioms, so this is not so easy. I believe the formal statement is P(X) $\iff$ $\exists x P(X)$. That is, I think, a combination of the axiom of generalization and axiom of existence. – RParadox Dec 6 '12 at 14:15
@RParadox: You missed my point...I took A to be the LHS, B to be the right hand side! - i.e., I did not equate A with P(x)! I was simplifying the task by shedding light on what needs to be established (establishing biconditionality of the expressions) : if the lhs implies the rhs, and rhs implies lhs, then we have equivalence... – amWhy Dec 6 '12 at 14:20
Sorry, to be so frank, but I believe this doesn't explain anything. If you want to give a formal proof for such an elementary prop, please cite the axioms you are using. – RParadox Dec 6 '12 at 14:26

This is not a formal proof, but it should get you started.

Suppose $\exists x (P(x) \vee Q(x))$ (1)

From (1), $P(a)\vee Q(a)$ (for some $a$)

This gives us two cases to consider.

Case 1: Suppose $P(a)$ (2)

From (2), $\exists x P(x)$ (3)

From (3), $\exists x P(x)\vee \exists x Q(x)$ (4)

From (2) and (4), $P(a)\rightarrow \exists x P(x)\vee \exists x Q(x)$

Case 2: Suppose $Q(a)$...

-

Formal proof

We are in the system of predicate calculus PC axioms

(Note (Set $\varphi$ as $P(X)$ and $\psi$ as $Q(X)$))

Hyp: $\exists x ( \varphi x \vee \psi x)$

Step 1 (Hyp) $\vdash \exists x ( \varphi x \vee \psi x)$

Step 2 mpg $\vdash \exists x ( \varphi x \vee \psi x) \Rightarrow \exists x (\exists x (\varphi x) \vee \exists x (\psi x))$

Step 3 19.9 $\vdash \exists x (\exists x (\varphi x) \vee \exists x (\psi x)) \Rightarrow (\exists \varphi x \vee \exists \psi x)$

($\Leftarrow$ is left to the reader)

This proof can be written as a program within a program such as metamath, where as the other proofs given don't use a system and are therefore not proofs. A proof is a way of deriving true statements from axioms. In this case its necessary to cite the system you are proving the results in.

The following still holds:

There exists an x, such that x has the property P or x has the property Q. According to Russell, when we denote any x we speak about the existence of x or non-existence of x. To speak about a man, we can analyze this further to mean: there is an x and x is a man. The equation is an expression of this idea, although it's not very simple. With $P(X)$ we mean $\exists x: P(X)$. The equation can be read as: there is an x with the Property P or Q. This is true if and only if there is an x with the Property P or there is an x with the property Q.

I'm not sure it's really possible to prove the equation besides an argument along the lines given above, i.e. a proof within the the system of predicate calculus (see axioms of PC). The proof is very elementary given these axioms, I think it's two steps. Historically these systems of PC were identical to Russell's principia mathematica (PM). So, it's important to understand the principle of proof within ZFC or proof within PM. Any standard modern textbook on logic should introduce these notions (otherwise get a better book). To me, most standard textbooks are however, not really clear in this regards. Usually proof within S is mostly defined in a late chapter.

(Solve is, I believe, the wrong word here. To understand it, it is probably best to start with the essay on denoting. One could say that logic (proper) tries to answer questions about the calculations which we do. To distinguish between "this kind of logic" and logic as calculation, people use the term mathematical logic.)

-
I think you need to speak in the language of the asker. And you don't address the question at all. – amWhy Dec 6 '12 at 14:28
I highly doubt you have understood what I have said. The point of predicate calculus is that there is a common language. The actual calculations are trivial. – RParadox Dec 6 '12 at 14:33
Oh I finally got it, you don't know what axioms of predicate calculus are. – RParadox Dec 6 '12 at 14:38
There have been some flags saying that the last comment is rude or offensive. However, since a link was added to the axioms of predicate calculus at about the same time, I don't think that this was meant to be rude. – robjohn Dec 6 '12 at 17:48
I was wondering for quite some time and then I understood. I added the proof now. It should be correct (but obvious from my statements before that). In PC the proof takes a few steps. So, I'll discount the downvotes for the typical cognitive dissonance which must occur to mathematicians when seriously arguing on logic. – RParadox Dec 6 '12 at 18:18