Exercise 0.6 in Algebra by Roger Godement Let $R,S$ be two relations and $x$ a letter not contained in $R$. Show that
the relation
$$
(\forall x)(R \lor S) \iff (R \lor (\forall x)S)
$$
is true.
I am just working on the "$\Rightarrow$" case for this question.
I can rearrange the original expression using some rules of logic (provided in
the book) and then I end up using a
truth table to get the answer. I think Godement just wants me to use the rules of logic he has provided
rather than resorting to a truth table. If you answer this question then such
rules of logic will probably be quite obvious to you since you are not a
beginner like me and so I won't quote them from the book here.
(Thanks @DavidDiaz for the table formatting edit)
\begin{array}{|c|c|c|c|c|}
\hline
 R & S &\lnot S & (\exists x)(\lnot S)\quad (*) & R \lor \lnot[(\exists x)(\lnot S)] \lor [(\exists x)(\lnot R) \land (\exists x)(\lnot S)] \\ \hline
F & F & T & T & T \\ \hline
F & T & F & T & T \\ \hline
T & F & T & T & T\\ \hline
T & T & F & T & T \\ \hline
\end{array}
(*) Note that, and I may be abusing truth tables here, I notice that there
exists at least one T value in the $(\lnot S)$ column, so I can say that the $(\exists
x)(\lnot S)$ column is true for all rows [1]. I use a similar approach on the last column. In the interest of keeping the table reasonable in
size I've not included some of the columns I used.


*

*Granting that my use of a truth table is an inelegant way to prove
this, can you tell me if what I did, in [1] above, is logically correct and a valid use of the truth table? Update: This is a fine, though inelegant approach, see my answer below for a useful reference that settles this question.

*More importantly, can you show me how to do this the proper way using only
rules of logic and no explicit truth table (as I am sure Godement intends)? Update: See my, and hopefully others, answer(s) below.
Thanks in advance.
 A: If $\forall x~R\vee S$ then for any arbitary entity (or "mathematical object"), $A$, we have $(A\mid x)(R\vee S)$, and therefore $((A\mid x)R)\vee((A\mid x)S)$. 
In the case for $(A\mid x)R$ then since $x$ does not occur free in $R$, that would be just $R$ and hence $R\vee \forall x~ S$ can be inferred (via the rule of "disjunction introduction", or "weakening"). 
In the case for $(A\mid x)S$, then since $A$ is arbitrary, $\forall x~S$ and hence $R\vee\forall x~S$ can be inferred. 
Therefore $R\vee\forall x~S$ can be inferred from $\forall x~(R\vee S)$ using "proof by cases".

The derivation for the converse is much the same. 
A: First, prove "$\Rightarrow$" case:
At first attempt, we'd like to do the following:
$$
(\forall x)(R \lor S) \Rightarrow [(\forall x)R \lor (\forall x)S]
$$
Unfortunately,
$$
(\forall x)(R \lor S) \iff [(\forall x)R \lor (\forall x)S]
$$
is not true in general. [See Godement, p.33, (TL 10) discussion]. 
Starting again,
$$
(\forall x)(R \lor S) \Rightarrow (R \lor (\forall x)S)
$$
is equivalent to [because $(P \Rightarrow Q) \iff Q \lor \lnot P$ is a true relation - this is easy to miss: that by the foregoing rule the consequent has become the antecedent, no distribution of $(\forall x)$ has occurred across $(R \lor S)$]
$$
(R \lor (\forall x)S) \lor \lnot [(\forall x)(R \lor S)]
$$
which simplifies to
$$
(R \lor (\forall x)S) \lor (\exists x)(\lnot R \land \lnot S)
$$
Because $(\exists x)(P \land Q) \iff [(\exists x)P \land (\exists x)Q]$ is a true relation, we can simplify further to obtain
$$
(R \lor (\forall x)S) \lor [(\exists x)\lnot R \land (\exists x)\lnot S]
$$
Since $x$ is not contained in $R$, we now have (on the RHS)
$$
[R \lor (\forall x)S] \lor [\lnot R \land (\exists x) \lnot S]
$$
Since $[\lnot R \land (\exists x) \lnot S]$ is equivalent to $\lnot [R \lor (\forall x) S]$ we have
$$
[R \lor (\forall x)S] \lor \lnot [ R \lor (\forall x) S]
$$
but then we have a tautology. 
The converse is yet to be proved as I have done all I want to do for today.
Regarding my original question part #1, I was subsequently able to satisfy myself that my use of the truth table, inelegant as it was, was in fact correct with respect to the existential, $\exists$, quantifiers. This was the helpful source that made that clear: Truth Tables for Predicate Logic - G52DOA - Derivation of Algorithms
