Traducción entre la caja de Huth/Ryan y las notaciones de Fitch

Question

Me he encontrado con pruebas que utilizan una notación con casillas ( Lógica en informática de Huth y Ryan), donde cada supuesto está dentro de su propia caja:

Ahora me gustaría escribir estas pruebas utilizando la notación de Fitch, pero no soy capaz de entender cómo hacerlo. Lo he intentado (ver más abajo), pero no estoy seguro de que sea correcto.

He buscado bastante por ahí una "notación Fitch para dummies" pero mis conocimientos dentro del campo de las pruebas lógicas son escasos y aún no he encontrado nada útil.

Agradecería mucho cualquier ayuda en el tema de la traducción de "cajas a Fitch".

Answer 1

Su respuesta es correcta. En realidad, es más fácil utilizar su propio razonamiento lógico para escribir una prueba directamente en la notación de estilo Fitch. El requisito fundamental es que toda estructura sintáctica que implique un $\huge\vdash$ es especificar un subcontexto, donde lo que está arriba especifica el subcontexto, y lo que está abajo es lo que se deriva dentro de ese subcontexto. Así que para la lógica proposicional cada "suposición" corresponde a la creación de un nuevo subcontexto en el que la suposición es verdadera. Y se puede ver fácilmente por qué las reglas de la deducción natural son sólidas, porque por ejemplo el [ $\to$ intro] y [ $\to$ elim] captan el significado de la implicación porque hacen que, dentro de cualquier contexto, tengamos " $A \to B$ " es derivable si " $\begin{array}{|l}A \\\hline B\end{array}$ " es derivable.

Lamentablemente no he podido encontrar ninguna descripción precisa de un sonido Cálculo estilo Fitch que incluye reglas para cuantificadores. El quebradero de cabeza suele estar en especificar qué variables se pueden utilizar y dónde, para evitar conflictos. Así que lo mejor que puedo ofrecerte es mi propio conjunto de reglas (que implementan la lógica libre que es la misma que la lógica de primer orden convencional, excepto que no prohíbe intrínsecamente un dominio vacío).

Answer 2

Aquí hay un ejemplo de notación Fitch que conozco, tal vez es lo que querías decir:

Pero personalmente creo que es irrelevante cuál de estas anotaciones (la de Fitch, la tuya o la de Huth y Ryan) utilices. Todas me parecen buenas y claras (son básicamente las mismas). En particular, la traducción que propones me parece perfectamente bien.

Answer 3

Aquí hay una prueba que muestra cómo se vería su prueba en este verificador de pruebas al estilo de Fitch:

El enlace del comprobador de pruebas y el libro de texto de lógica asociado aparecen a continuación.

---

Editor y comprobador de pruebas de deducción natural al estilo de JavaScript/PHP de Kevin Klement http://proofs.openlogicproject.org/

P. D. Magnus, Tim Button con adiciones de J. Robert Loftis remezclado y revisado por Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: Una introducción a la lógica formal, otoño de 2019. http://forallx.openlogicproject.org/forallxyyc.pdf