Help with using universal instantiation/generalization when variable ocurrence is unknown.

46 Views Asked by At

For example:

$\forall x(\varphi \land \psi)\rightarrow (\forall x\varphi \land \forall x\psi)$

Now I would try to drop the forall, and deduce $\varphi$, $\psi$ from $(\varphi \land \psi)$ and then use universal generalization to get to the right side, but I don't know whether the formulas contain $x$ or not. Looking at examples which do contain $x$, it doesn't seem to make a difference, but how do I go about writing that down correctly?

1

There are 1 best solutions below

0
On

In general it is a theorem that $\forall x (\varphi \wedge \psi) \implies (\varphi \wedge \psi)$