He estado tratando de probar $\vdash\phi \land \diamond\psi \to \diamond(\psi\land\diamond \phi)$ en la deducción natural donde se permite usar $\phi\to \square \diamond \phi$ y/o $\diamond\square\phi\to\phi$ (es decir, en $KB)$ pero he fallado. ¿Cómo se puede demostrar esto? No incluyo mi trabajo porque consta de decenas de páginas y no lleva a ninguna parte...
Respuesta
¿Demasiados anuncios?
He aquí un esbozo de la idea, que te dejo para que la traduzcas en una prueba formal en tu sistema, si te interesa.
Supongamos que $\phi$ y $\lozenge \psi$ . A partir de B y del modus ponens, obtenemos $\square\lozenge \phi$ , por lo que obtenemos $(\square\lozenge\phi \land \lozenge \psi)$
Ahora como una instancia del axioma de distribución K, tenemos: $$\square (\lozenge \phi \rightarrow \lnot \psi) \rightarrow (\square \lozenge \phi \rightarrow \square \lnot \psi)$$
El contrapositivo de esta implicación es: $$\lnot (\square\lozenge \phi \rightarrow \square \lnot \psi) \rightarrow \lozenge \lnot (\lozenge \phi \rightarrow \lnot \psi)$$
Girando $\lnot (p\rightarrow q)$ en $p\land \lnot q$ en dos lugares, obtenemos: $$(\square\lozenge \phi \land \lozenge \psi) \rightarrow \lozenge (\psi \land \lozenge \phi)$$
Finalmente, por modus ponens, obtenemos $$\lozenge (\psi \land \lozenge \phi)$$
