Ya no tienes que indagar más en otros sitios ya que llegaste al lugar adecuado, poseemos la solución que buscas pero sin problemas.
Solución:
Estos problemas pueden ser bastante difíciles. Me enorgullezco de ser razonablemente bueno con ellos, pero no puedo darte más que pautas muy vagas y de alto nivel sobre cómo atacarlos.
En algunos casos, puede tener la suerte de tener un método infalible al que recurrir. En particular, si tiene una prueba constructiva de que el sistema formal que está utilizando es completo, entonces esto le brinda un enfoque garantizado si-todo-lo-demás-falla: Primero verifique que la fórmula que tiene es una tautología, usando tablas de verdad, luego rastree los pasos en la prueba de integridad aplicada a su fórmula.
La desventaja es que este método puede conducir a algunos enormemente pruebas formales largas y engorrosas, incluso para conclusiones de aspecto bastante inocente. Tratando de ser inteligente primero casi siempre vale la pena el esfuerzo.
Entonces, ¿cuál es un plan general para tratar de ser inteligente? Eventualmente todo se reduce a la práctica y la experiencia. Pienso, tenativamente, que la experiencia requerida se puede dividir en dos categorías amplias.
(1) Una buena comprensión intuitiva de fórmulas lógicas.
O preferiblemente varias vistas intuitivas de fórmulas con las que tenga suficiente práctica para alternar sin esfuerzo, para ver el problema desde varios lados.
La semántica oficial de las fórmulas proposicionales dice que especifican cómo combinar valores de verdad para las letras proposicionales en un valor de verdad para toda la fórmula, utilizando tablas de verdad para cada uno de los conectivos. Eso no es incorrecto, pero tampoco es muy estimulante para la imaginación.
Creo que es importante conocer al menos una “interpretación de recursos” para la lógica proposicional, en la línea de:
- Cada letra proposicional es una especie de recurso primitivo.
- $ varphi to psi $ es una máquina que le dará $ psi $ si le pone $ varphi $.
- $ varphi land psi $ es un conjunto en caja que contiene $ varphi $ y $ psi $.
- $ varphi lor psi $ es una caja misteriosa que contiene un $ varphi $ o un $ psi $. Se le permite mirar en él para ver qué es. Cuando necesite hacer un $ varphi lor psi $ usted mismo, podrá decidir si colocar un $ varphi $ o un $ psi $ en una caja.
- $ neg varphi $ es un genio que siempre quiso un $ varphi $ y te concederá deseos ilimitados si le das uno. O tal vez sea un genio presumido y condescendiente que está convencido de que $ varphi $ s no existen y está dispuesto a apostarle cualquier cosa a que usted no puede mostrarle una.
Entonces, una prueba de $ varphi $ es lo mismo que una receta para hacer un $ varphi $.
Por ejemplo, aquí se le pide que demuestre $ ( neg alpha to beta) to ( neg beta to alpha) $. Mi primer paso sería obtener un modelo mental de lo que eso significa en la imagen de recursos.
Hmm, necesito construir una máquina que obtenga un $ neg alpha to beta $ y produzca otra máquina … así que eso es lo mismo que hacer una máquina que obtenga un $ neg alpha to beta $ y un $ neg beta $ y debe producir un $ alpha $. Tengo que averiguar cómo combinaría esos dos componentes para obtener el resultado requerido.
Esto no ayuda de inmediato, porque parece que no hay por dónde empezar. El genio $ neg beta $ me daría el $ alpha $ deseado si le proporcionara un $ beta $, que podría obtener el $ beta $ de $ neg alpha a beta $, pero luego Necesito un $ neg alpha $. Mmm.
Aquí es donde ayuda tener varias perspectivas disponibles, porque, volviendo a la imagen del valor de verdad, $ alpha $ es true o false. Si es true, luego termino de inmediato; si es false entonces tengo $ neg alpha $ y puedo cambiar eso por $ beta $ y finalmente por $ alpha $, y habré terminado.
Entonces, si el sistema prueba el ley del medio excluido, significa que en la imagen de recursos puedo obtener, gratis, un cuadro que contendrá $ alpha $ o $ neg alpha $. Abre la caja; si es una salida interna $ alpha $ que; pero si $ neg alpha $ póngalo en la máquina $ neg alpha to beta $, y dé el $ beta $ que sale al genio $ neg beta $. Luego, desea un $ alpha $ que pueda generar.
Desafortunadamente, eso realmente no nos ayuda porque los axiomas que está usando aquí no parecen hacer que sea particularmente fácil probar la ley del medio excluido (en realidad, como se cita, ni siquiera sabe qué es $ lor $). Y eso nos lleva al segundo tipo de experiencia que necesitamos:
(2) Experiencia en el trabajo con el sistema formal en cuestión.
Aquí es donde archivaríamos (2a) “si entiendo cómo hacer algo en la imagen del recurso, entonces, ¿cómo expreso esa receta en forma de prueba en este sistema en particular?”. También es donde debemos responder (2b) “si necesito hacer algo que no es posible solo en la imagen de los recursos constructivos, ¿qué medios tengo para escapar?” – como apelar al medio excluido, la eliminación de la doble negación o la ley de Peirce.
De estos (2a) es principalmente una cuestión de práctica con la construcción de pruebas para el sistema. En su sistema, MP y las leyes (L1), (L2) y (L4) están ahí esencialmente para poder expresar manipulaciones de cosas dentro y fuera de máquinas, construcción de máquinas que implementan una receta dada, etc. HS también parece estar en esta categoría (no sé qué significa eso, pero en su ejemplo parece ser una regla abreviada para conectar la salida de una máquina a la entrada de otra).
También se cubre en (2a) cómo lidiar con la negación en el sistema, que desafortunadamente varía mucho más entre sistemas que lo que hace con la implicación.
Con todo (2a) se puede ganar razonablemente haciendo muchos ejercicios en el sistema. Desafortunadamente, la habilidad en la que resultará esta práctica es prácticamente inútil para cualquier cosa. pero resolviendo este tipo de ejercicios, que solo ocurre en las aulas de lógica formal. Por el contrario, la experiencia que recopilé en (1) es, en mi experiencia, bastante útil incluso fuera del aula.
Para (2b) hay algunos conocimientos generalmente útiles sobre los tipos de formas de escapar de la imagen de los recursos en las pruebas. En términos más técnicos, se trata de conocer una variedad de leyes que se pueden agregar a la lógica intuicionista para producir la lógica clásica. Aquí es donde me equivoqué anteriormente, porque mi primera idea fue usar el medio excluido, pero el medio excluido no es una ley primitiva en el sistema particular con el que estamos trabajando.
(He mantenido ese desvío en la respuesta como una ilustración del tipo de false comienza uno debe estar preparado para hacer mucho antes de encontrar algo que funcione).
Una trampilla de escape diferente es la eliminación de la doble negación, su regla (L5). Pero no parece haber una forma sencilla de hacer que eso afecte a $ ( neg alpha to beta) to ( neg beta to alpha) $.
Por otro lado, (L3) es claramente una forma de contraposición, y $ ( neg alpha to beta) to ( neg beta to alpha) $ también es como una contraposición: es solo una diferencia de donde van las negaciones. También sé, por una larga experiencia, que (L3) es una forma de contraposición que no es intuicionistamente válida, lo que hace que (L3) comience a parecer realmente prometedor.
Si quiero concluir $ neg beta to alpha $ de (L3), tendré que proporcionarle $ neg alpha to neg neg beta $. Pero todo lo que tengo es $ neg alpha to beta $. Pero, volviendo a los valores de verdad por un segundo aquí, sabemos que $ neg neg beta $ es lo mismo que $ beta $, por lo que $ neg alpha to neg neg beta $ es el igual que $ neg alpha to beta $.
Esto lo podemos hacer en la imagen de recursos. Queremos construir una máquina para $ neg alpha to neg neg beta $. Lo que hace esta máquina es obtener un $ neg alpha $, ejecutarlo a través del $ neg alpha to beta $ que ya tenemos y convertir el $ beta $ resultante en $ neg neg beta $ usando (L6), que convenientemente hace precisamente eso.
Y esto resulta que funciona. Conseguir que estas ideas “cinemáticas” intuitivas sobre cómo mover cosas dentro y fuera de las máquinas se transformen en la prueba particular que cita ahora es solo una aplicación de las habilidades de la categoría (2a). Las líneas anotadas (L1), (L2), MP, HS son parte de modismos estándar para unir cosas; el contenido creativo está en el uso (L3) y (L6).
En cuanto a cómo aprender esos modismos estándar para este sistema en particular, no tengo mejor consejo que buscar la prueba de la Teorema de deducción para el sistema (es de esperar que tenga uno) y analice exactamente lo que hace en un buen número de ejemplos.
Lo siento si esta respuesta es un poco divagante. Estoy haciendo todo lo posible para dar algún tipo de visión interna de cómo un problema como este sería atacado desde un punto de vista “bastante experimentado”. Esto puede ser útil o no para usted; creo que el punto más general para llevar a casa es que es importante tener muchas formas de pensar acerca de las fórmulas lógicas disponibles y ser competente en el uso de todas ellas.
¿Por dónde empiezas? ¡Empiezas por el final! Luego trabajas al revés.
Deseamos usar $$ begin array ll (MP) & p, p to q vdash q \ (HS) & p to q, q to r vdash p to r \ (L1) & p to (q ap) \ (L2) & (p to (q to r)) to ((p to q) to (p to r)) \ (L3) & ( neg p to neg q) to (q to p) \ (L4) & p to p \ (L5) & neg neg p to p \ (L6) & p to neg neg p finarray $$
Para demostrar $ ( neg a to b) to ( neg b to a) $
Ahora, trabajando al revés, vemos que casi lo tenemos en L3, excepto que al sustituir $ neg b $ por $ q $ se introduce una doble negación donde necesitamos el literal.
$$ ( neg p to neg q) to (q to p) \ ( neg a to neg ( neg b)) to (( neg b) to a) $$
Esto sería trivial si pudiéramos sustituir la doble negación directamente, pero todo lo que tenemos son L5 y L6. Así que de alguna manera tenemos que pasar de uno de ellos a L3.
Ahora, si podemos demostrar que $ ( neg a ab) to ( neg a to neg neg b) $ podemos usar un silogismo hipotético para llegar a lo que queremos a través de L3.
$$ begin array lll P_ n-2 & ( neg a to b) to ( neg a to neg neg b) & \ hline P_ n-1 & ( neg a a neg ( neg b)) a (( neg b) a a) & L3 \ hline P_n & ( neg a a b) a ( neg b a a) & HS, P_ n-1, P_ n-2 end array $$
Sin embargo, eso no se parece a ninguno de los axiomas. Entonces tendríamos que llegar a él usando MP o HS. Ya usamos HS, así que mirando MP, necesitaríamos algo para que algo implique $ P_ n-2 $.
$$ X to (( neg a to b) to ( neg a to neg neg b)) $$
Una forma de construir tal implicación es L1 $$ p to (q to p) \ color red ( neg a to neg neg b) to (( neg a to b) to ( neg a to neg neg b)) $$
Otro es L2. $$ (p to (q to r)) to ((p to q) to (p to r)) \ color blue ( neg a to (b to neg neg b)) to (( neg a to b) to ( neg a to neg neg b)) $$
Eso parece ser más fructífero de los dos.
$$ begin array lll P_ n-4 & ( neg a to (b to neg neg b)) \ hline P_ n-3 & ( neg a to (b to neg neg b)) to (( neg a to b) to ( neg a to neg neg b)) & L2 \ hline P_ n-2 & ( neg a a b) a ( neg a a neg neg b) & MP, P_ n-3, P_ n-4 \ hline P_ n-1 & ( neg a a neg ( neg b)) to (( neg b) to a) & L3 \ hline P_n & ( neg a to b) to ( neg b to a) & HS, P_ n-1, P_ n-2 end array $$
Ahora probemos MP y L1, $ X to ( neg a to (b to neg neg b)) $
$$ p to (q to p) \ color blue (b to neg neg b) to ( neg a to (b to neg neg b)) $ PS
Y hemos retrocedido a L6, por lo que al volver a numerar tenemos:
$$ begin array lll P_1 & b to neg neg b & L6 \ hline P_2 & (b to neg neg b) to ( neg a to (b to neg neg b) ) & L1 \ hline P_3 & ( neg a to (b to neg neg b)) & MP, P_1, P_2 \ hline P_4 & ( neg a to (b to neg neg b)) to (( neg a to b) to ( neg a to neg neg b)) & L2 \ hline P_5 & ( neg a to b) to ( neg a to neg neg b) & MP, P_3, P_4 \ hline P_6 & ( neg a to neg ( neg b)) to (( neg b) to a) & L3 \ hline P_7 & ( neg a to b) to ( neg b to a) & HS, P_5, P_6 end array $$
Este es un tema profundo y difícil. Es posible que desee ver aquí: Trucos para construir pruebas al estilo de Hilbert También existen algunos buenos consejos en un volumen antiguo de LH Hackstaff titulado “Sistemas de lógica formal”.
Utilizo la notación polaca / Lukasiewicz.
Para su sistema particular, tiene el metateorema de deducción. Siempre que pueda probar las reglas de inferencia p $ vdash $ Cqp y CpCqr, Cpq $ vdash $ Cpr, puede probar el teorema de la deducción. Espero que pueda hacerlo, sea evidente al tener CpCqp y CCpCqrCCpqCpr como axiomas en su sistema.
Por lo tanto, para su problema particular, podemos asumir cosas como las siguientes:
assumption 1 | CNpq
assumption 2 |@ Nq
Y queremos derivar “p” de eso. ¿Cómo podemos obtener “p”? Bien, si p es el consecuente de alguna fórmula, y podemos probar el antecedente de esa misma fórmula, entonces podemos derivar p en un paso. Tenga en cuenta que solo tenemos “p” en el primer supuesto. Entonces, necesitaremos usar eso en algún lugar del camino. ¿Cómo introducimos “p” en el consecuente aquí? Bueno, el axioma C CNpNq Cqp nos dice que si podemos poner un símbolo de negación antes de “q”, entonces podemos hacer que esa fórmula sea el antecedente que coincida con C CNpNq Cqp o con una instancia de sustitución de C CNpNq Cqp. CpNNp nos permite agregar dos negaciones a cualquier fórmula. Por lo tanto, a partir de CNpq y CqNNq, al tener la regla HS podemos derivar CNpNNq. Entonces, dado que tenemos C CNpNq Cqp, podemos derivar CNqp. Y el siguiente paso debería ser sencillo. Continuando en esa línea:
instance of CpNNp 3 |@ CqNNq
this is a theorem 4 |@ C Cpq C Crp Crq
4, 3 MP (and some substitution) 5 |@ C Crq CrNNq
5, 1 MP (and some substitution) 6 |@ C Np NNq
axiom 7 |@ C CNpNq Cqp
7, 6 MP (and some substitution) 8 |@ C Nq p
8, 2 MP 9 |@ p
Y a partir de ahí podríamos aplicar el metateorema de deducción para obtener nuestro resultado.
Al final de la artículo puedes encontrar las explicaciones de otros programadores, tú asimismo tienes la libertad de dejar el tuyo si lo crees conveniente.