## 23 September 2007

### Existential logic got ya down?

Having just started a graduate applied mathematics program without a heavy math background, they're putting me through boot camp. Lots of the proofs require combining ands and ors with the existence quantifiers, and I invariably screw these up. Quick, does $\exist{}x_1:p(x_1)\wedge{}\exist{}x_2:q(x_2) \Rightarrow \exist{}x:p(x)\wedge{}q(x)$ ? How about $
\exist{}x:p(x)\wedge{}q(x) \Rightarrow \exist{}x_1:p(x_1)\wedge{}\exist{}x_2:q(x_2)
$
?

One nice tool I've just found is Molle:

Molle is a cross-platform prover for modal logic, that exploits the modal semantic tableaux method. It features a very usable graphical interface, with interactive representation of generated models.
Particularly sweet is the Java Web Start version mollecino. You feed Molle first order logic statements and it will prove whether or not they are correct. It's a great tool, especially to convince yourself that things you think may be true actually are true.

To play with second order quantifiers, recast them as collections of statements. For example, to pretend that you've got $\exist{}x:p(x)$ say that $p(x)$ is really a set of three separate conditions $p_1$, $p_2$, and $p_3$. Then convert $\exist{}x:p(x)$ into $p_1\vee{}p_2\vee{}p_3$ and feed that into Molle. Similarly, change $\forall{}x:p(x)$ into $p_1\wedge{}p_2\wedge{}p_3$.

To check $\exist{}x_1:p(x_1)\wedge{}\exist{}x_2:q(x_2) \Rightarrow \exist{}x:p(x)\wedge{}q(x)$ feed Molle the input (A|B|C|D)&(Z|X|Y|W)=>(A&Z)|(B&X)|(C&Y)|(D&W). To check $
\exist{}x:p(x)\wedge{}q(x) \Rightarrow \exist{}x_1:p(x_1)\wedge{}\exist{}x_2:q(x_2)
$
feed Molle the input (A&Z)|(B&X)|(C&Y)|(D&W)=>(A|B|C|D)&(Z|X|Y|W). The first statement isn't valid but the second one is.