La notación de Fitch , también conocida como diagramas de Fitch (denominada así en honor a Frederic Fitch ), es un sistema de notación para construir pruebas formales que se utilizan en lógicas oracionales y lógicas de predicados . Las pruebas al estilo de Fitch organizan la secuencia de oraciones que componen la prueba en filas. Una característica única de la notación de Fitch es que el grado de sangría de cada fila transmite qué suposiciones están activas para ese paso.
Ejemplo
Cada fila en una prueba estilo Fitch es:
- una suposición o suposición de prueba secundaria.
- una oración justificada por la cita de (1) una regla de inferencia y (2) la línea o líneas anteriores de la prueba que autoriza esa regla.
La introducción de un nuevo supuesto aumenta el nivel de sangría y comienza una nueva barra de "alcance" vertical que continúa sangrando las líneas subsiguientes hasta que se descarta el supuesto. Este mecanismo transmite inmediatamente qué suposiciones están activas para cualquier línea dada en la demostración, sin que las suposiciones necesiten ser reescritas en cada línea (como con las pruebas de estilo secuencial).
El siguiente ejemplo muestra las características principales de la notación de Fitch:
0 | __ [supuesto, quiero P si no es P]1 | | __ P [supuesto, no quiero no P]2 | | | __ no P [supuesto, para reductio]3 | | | contradicción [introducción de la contradicción: 1, 2]4 | | no no P [introducción de la negación: 2] |5 | | __ no no P [supuesto, quiero P]6 | | P [eliminación de la negación: 5] |7 | P iff not not P [introducción bicondicional: 1 - 4, 5 - 6]
0. La suposición nula, es decir , estamos probando una tautología
1. Nuestra primera subprueba: asumimos que lhs para mostrar que la rhs sigue
2. Una subprueba: somos libres de asumir lo que queramos. Aquí apuntamos a una reductio ad absurdum
3. Ahora tenemos una contradicción
4. Se nos permite anteponer el enunciado que "causó" la contradicción con un no
5. Nuestra segunda subprueba: asumimos que rhs para mostrar que lhs sigue a
6. Invocamos la regla que nos permite eliminar un número par de nots de un prefijo de enunciado
7. De 1 a 4 hemos mostrado si P entonces no P, de 5 a 6 hemos mostrado P si no P; por lo tanto, se nos permite introducir el bicondicional
Ver también
Referencias
- Frederic Brenton Fitch , Lógica simbólica: una introducción , Ronald Press Co., 1952.
- Jon Barwise y John Etchemendy , Language, Proof and Logic 1st edition como PDF , Seven Bridges Press y CSLI, 1999.
enlaces externos
- La paradoja de la capacidad de conocimiento de Fitch
- Una aplicación Java en línea para la creación de pruebas
- Una implementación web del sistema de prueba de Fitch (proposicional y de primer orden) en proofmod.mindconnect.cc
- El asistente de pruebas de uso general de Jape (ver Jape )
- Recursos para la composición tipográfica de pruebas en notación Fitch con LaTeX (ver LaTeX )
- FitchJS: una aplicación web de código abierto para construir pruebas en notación Fitch (y exportar a LaTeX)
- Corrector y corrector de pruebas de deducción natural en notación Fitch