I'm having trouble with a proof in first order logic. I'm supposed to prove that if x occurs free in either φ or ψ, then x occurs free in (φ◦ψ) for ◦ = ∧,∨,→,↔. I do understand what they mean and I can see how this is true. However I'm stuck at figuring out how to actually prove it correctly.
The concept of bound and free variables was explained with parsing trees. They also gave this formal definition of a bound variable:
Let (n,x) be an occurrence of a variable x in a formula φ and (m, Qy) an occurrence of a quantifier Q = ∀, ∃ in φ.
Then, (n, x) is bound by (m, Qy) iff
(i) x=y, (ii) there is an downwards path from m to n, (iii) this path from m to n does not go through a node k such that (k, Q′x) is an occurrence of a quantifier Q′ = ∀, ∃ in φ.
When a variable occurrence in a formula is not bound by some quantifier occurrence in the same formula, we also call the variable occurrence free.
I have tried a couple different proof strategies but I just can't seem to figure this one out. Would someone like to point me in the right direction? I would really appreciate it.
Intuitively, we have the concept of scope of a quantifier $Qx$; in both formulas $\forall x \varphi$ $\exists x (\varphi) \lor \psi$ we have that the sub-formula $\varphi(x)$ is in the scope of the quantifier, while sub-formula $\psi$ is not.
Having said that, we have that every occurrence of a variable $x$ in a formula that is in the scope of a quantifier is bound.
In terms of the formation tree of formula $\varphi$, the definition above says : we have that there are two nodes labelled with $(m,Qy)$ and $(n,y)$ respectively, and the node of $Qy$ is at an "upper" level (starting from root) with respect to the node of $y$ and there is no quantifier $Q'y$ that precedes $Qy$ in the path that leads from $n$ to $m$.
Example : $Px, Ry, Px \land Ry, \forall y (Px \land Qy)$.
The proof strategy is quite simple : you have two trees, one for $\varphi$ and one for $\psi$ and you have to "join" them with a new node for $\varphi \circ \psi$.
Because the new node does not add any new quantifier, if there is a free occurrence of $x$ in at least one of the two trees, that occurrence will be free also in the new tree.
A formal treatment of parsing trees can be found into : Ian Chiswell & Wilfrid Hodges, Mathematical Logic, (Oxford, 2007), page 38-on and similar for predicate logic.