La notación de Fitch , también conocida como diagramas de Fitch (llamado así en honor a Frederic Fitch ), es un sistema de notación para construir pruebas formales utilizado en lógica oracional y lógica de predicados . Las pruebas de estilo 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é supuestos están activos para ese paso.
Cada fila en una prueba estilo Fitch es:
La introducción de una nueva suposición aumenta el nivel de sangría y comienza una nueva barra vertical de "alcance" que continúa sangrando las líneas siguientes hasta que se descarta la suposición. Este mecanismo transmite inmediatamente qué supuestos están activos para cualquier línea determinada en la prueba, sin que sea necesario reescribir los supuestos en cada línea (como ocurre 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 P]1 | |__ P [suposición, no quiero P]2 | | |__ no P [supuesto, para reducción]3 | | | contradicción [introducción de 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 no no P [introducción bicondicional: 1 - 4, 5 - 6]
0. El supuesto nulo, es decir , estamos demostrando una tautología
. 1. Nuestra primera subprueba: asumimos los lhs para mostrar los derechos.
2. Una subsubprueba: somos libres de asumir lo que queramos. Aquí apuntamos a una reducción al absurdo
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 el derecho para mostrar que el izquierdo sigue
a 6. Invocamos la regla que nos permite eliminar un número par de no de un enunciado con prefijo
7. Del 1 al 4 hemos mostrado si P entonces no no P, del 5 al 6 hemos mostrado P si no no P; por lo tanto, se nos permite introducir el bicondicional en 7, donde iff representa si y sólo si