Notación de Fitch

La notación de Fitch , también conocida como diagramas de Fitch (en honor a Frederic Fitch ), es un método para presentar demostraciones de deducción natural en cálculo proposicional y lógica de primer orden mediante un formato estructurado, línea por línea, que muestra explícitamente supuestos, inferencias y su alcance. Fue inventada por Frederic Brenton Fitch en la década de 1930 y posteriormente popularizada a través de su libro de texto Lógica simbólica (1952). ^{[ 1 ]} La notación de Fitch se distingue por el uso de sangría o recuadros para indicar el alcance de los supuestos subordinados, lo que la convierte en uno de los sistemas más accesibles pedagógicamente para la enseñanza de la lógica formal.

Fitch desarrolló su sistema de deducción natural como parte de su tesis doctoral en la Universidad de Princeton en 1934, bajo la supervisión de Alonzo Church . Su enfoque introdujo la idea clave de las pruebas subordinadas , donde las suposiciones podían plantearse dentro de una subderivación y descartarse posteriormente, como al probar implicaciones o negaciones. Si bien su sistema circuló inicialmente de forma no publicada, se popularizó gracias a su libro Lógica simbólica ^{[ 1 ]} , que se utilizó ampliamente en la enseñanza universitaria.

Lógicos y educadores posteriores, como Patrick Suppes ^{[ 2 ]} y E.J. Lemmon ^{[ 3 ],} reformularon el sistema de Fitch. Si bien introdujeron cambios gráficos —como reemplazar la sangría con barras verticales—, la estructura subyacente de la deducción natural al estilo Fitch se mantuvo intacta. Estas variaciones suelen denominarse formato Suppes-Lemmon , aunque se basan fundamentalmente en la notación original de Fitch.

La notación de Fitch presenta las demostraciones como una secuencia de líneas numeradas, donde cada línea incluye:

• Una fórmula lógica
• Una justificación (nombre de la regla y referencias de línea)
• Opcionalmente, se puede usar sangría o corchetes para mostrar el alcance de las suposiciones.

0 |__ [suposición, se quiere P si no P] 1 | |__ P [suposición, no quiero P] 2 | | |__ no P [suposición, para reducción] 3 | | | contradicción [introducción a la contradicción: 1, 2] 4 | | no no P [introducción a la negación: 2] | 5 | |__ no no P [suposición, quiero P] 6 | | P [eliminación de negación: 5] | 7 | P si y solo si no no P [introducción bicondicional: 1 - 4, 5 - 6] 

• La deducción natural al estilo Gentzen presenta las demostraciones como árboles, con las suposiciones en las hojas y las conclusiones en la raíz. A diferencia de la notación Fitch, no utiliza recuadros subordinados ni sangría para gestionar las suposiciones temporales. En cambio, todas las suposiciones se presentan explícitamente en los nodos hoja del árbol de demostración. Este tratamiento uniforme de las suposiciones hace que los sistemas Gentzen sean especialmente adecuados para las transformaciones estructurales de las demostraciones y facilita la modularización y el análisis metateórico, como la eliminación de cortes.
• Las demostraciones mediante sistemas de Hilbert se basan en axiomas y en solo unas pocas reglas de inferencia, lo que las hace concisas pero abstractas y menos intuitivas.
• La notación de Suppes-Lemmon sigue la lógica de Fitch y modifica su disposición visual para facilitar la composición tipográfica y la claridad didáctica.

La notación de Fitch se utiliza ampliamente en libros de texto y en la enseñanza de la lógica . Además, sirve de base para diversas herramientas de asistencia a la demostración . Su estilo estructurado se ha convertido en un estándar para la enseñanza de la lógica formal en la educación universitaria.

• Deducción natural
• Frederic Fitch
• Cálculo de secuencias
• Teoría de la demostración
• Sistema de Hilbert
• Notación de Suppes-Lemmon

• Fitch, Frederic Brenton (1952). Lógica simbólica: Una introducción . Nueva York: The Ronald Press Company. LCCN 52006196 . 

• Barker-Plummer, Dave; Barwise, Jon ; Etchemendy, John (2011) [1999]. Lenguaje, demostración y lógica (2.ª  ed.). CSLI Publications. pág.  606. ISBN 9781575866321.
• Lemmon, EJ (1965). Lógica básica . Nelson.
• Suppes, Patrick (1957). Introducción a la lógica . Van Nostrand.

• Brogaard, Berit ; Salerno, Joe (otoño de 2019). "La paradoja de la cognoscibilidad de Fitch" . En Zalta, Edward N. (ed.). Enciclopedia de filosofía de Stanford . ISSN 1095-5054 . OCLC 429049174 .  
• "Una aplicación Java en línea para la construcción de pruebas" . Archivado del original el 2 de octubre de 2006. Consultado el 6 de mayo de 2025 .
• "Implementación web del sistema de pruebas de Fitch (proposicional y de primer orden)" . proofmod.mindconnect.cc . Consultado el 6 de mayo de 2025 .
• "El asistente de pruebas de propósito general Jape" . GitHub . Consultado el 6 de mayo de 2025 .(ver Japón )
• "Recursos para la composición tipográfica de pruebas en notación Fitch con LaTeX" . Logic Matters . Consultado el 6 de mayo de 2025 .(ver LaTeX )
• "FitchJS: Una aplicación web de código abierto para construir demostraciones en notación Fitch (y exportarlas a LaTeX)" . Consultado el 6 de mayo de 2025 .
• "Editor y verificador de pruebas de deducción natural en notación Fitch" . Consultado el 6 de mayo de 2025 .