Is this predicate logic sequent valid? This is perhaps a silly set of related questions and the following is the problem that sparked it.
I am asked to prove this predicate logic sequent:
$\exists x[R(x) \vee S(x)] \;\;\;\;\; |-  \;\;\;\;\exists x R(x) \vee \exists x S(x) $
I am ashamed to say I cannot prove it. I tried the direct approach as well as a proof by contradiction approach, with no luck. And then it dawned on me that perhaps the question is wrong. Perhaps there is no proof. Ofcourse, not being able to prove a sequent does not imply it is invalid and therefore I do not even know if the question is phrased incorrectly. If this was a propositional logic question, and the ammount of propositional atoms were sufficiently small, I could construct a truth table and check for semantic entailment. A propositional sequent is valid iff it is semantically entailed, and therefore a truth table could invalidate it. However, with predicate Logic and its set of quantifiers, I dont have any experience checking truth tables in this instance and I therefore cannot even know if the sequent invalid.
Using an English argument, I can invalidate it by letting $R(x)$ mean $x$ is a rough object and $S(x)$ meaning $x$ is a smooth object:
"Premise: There exists a rough object like a grit. Conclusion: There exists a smooth object like a ball bearing".
Propositionally, the sentence is valid because the premise and conclusion is true. But logically, it is invalid. The existance of a rough object doesn't imply the existance of a smooth object. (Side note: What is extra confusing is now Ive left the core propositional logic domain and entered what feels like a more "subjective" domain and its frustrating)
But there is no "rigor" in the logical argument articulated in English.
Questions:

*

*Is the above sequent valid?

*If you know its valid because you proved it using deduction rules, stop here

*If there is no proof, how can you prove it is invalid? Do you use truth tables?

 A: The inference is valid and derivable.
In general, a counter example to an invalid inference consists of a structure in which all the premises are true but the conclusion is false.
Your argument is incorrect because it does not precisely show (by the means of providing a concrete counter model) that this interpretation of the predicates invalidates the sequent, and your English example is not an appropriate deformalization of the statement: You can't just drop one of the disjuncts in each of the sentences. If $R(x)$ is to stand for a rough object and $S(x)$ smooth, then the argument is "If exists an object which is rough or smooth, then either there exists a rough object or there exists a smooth one".
Normally it is advisable to start a natural deduction proof from the bottom to the top, performing backwards introduction rules on the main operator until you can get no futher, then switching to the top and working your way down from the premises by successive applications of elimination rules until you hopefully meet in the middle.
In this case, the conclusion is a disjunction, but attempting disjunction introduction as the last step won't lead to success, because this would require a proof of one of the disjunctions, which is obviously not possible, because you can not infer either of the two sides for sure, only the disjunction of them. So go to the top immediately and start disassembling the premises.
The only premise you are given is an existential statement, so the first thing to do is an existential elimination. Existential elimination means that you assume the quantified statement for some arbitrary object (say $a$), derive some conclusion from this assumption, then, since you know that at least one such object exists, you can infer the conclusion for sure. The conclusion you want to arrive at is $\exists x R(x) \lor \exists x S(x)$, so try to derive that under the assumption $R(a) \lor S(a)$:
| exists x(R(x) v S(x))
| | R(a) v S(a)
| | -----------
| | ...
| | exists x R(x) v exists x S(x)
| exists x R(x) v exists x S(x)

The next thing from the top is the disjnction $R(a) \lor S(a)$. So you do disjunction elimination, which means that you assume each of the disjuncts, derive the same conclusion from both, then conclude that since at least one of the two sides holds, the conclusion follows for sure. The conclusion to infer at the end, and in the two subproofs, is again $\exists x R(x) \lor \exists x S(x)$:
| exists x(R(x) v S(x))
| | R(a) v S(a)
| | -----------
| | | R(a)
| | |-----
| | | ...
| | | exists x R(x) v exists x S(x)
| | | S(a)
| | | ----
| | | ...
| | | exists x R(x) v exists x S(x)
| | exists x R(x) v exists x S(x)
| exists x R(x) v exists x S(x)

That's the scaffold of the proof. Can you fill in the ...'s on your own?
