La notación Fitch , también conocida como diagramas Fitch (denominada así por Frederic Fitch ), es un sistema de notación para construir pruebas formales que se utiliza en lógicas oracionales y lógicas 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 Fitch es que el grado de sangría de cada fila transmite qué suposiciones están activas para ese paso.
Cada fila en una prueba de estilo Fitch es:
Al introducir una nueva suposición, se aumenta el nivel de sangría y se inicia una nueva barra de "alcance" vertical que continúa sangrando las líneas subsiguientes hasta que se cancela la suposición. Este mecanismo transmite inmediatamente qué suposiciones están activas para cualquier línea dada en la prueba, sin que sea necesario reescribirlas en cada línea (como en las pruebas de estilo secuencial).
El siguiente ejemplo muestra las principales características de la notación Fitch:
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 de la contradicción: 1, 2]4 | | no no P [introducción de negación: 2] |5 | |__ no no P [suposición, quiero P]6 | | P [eliminación de negación: 5] |7 | P si no es P [introducción bicondicional: 1 - 4, 5 - 6]
0. La suposición nula, es decir , estamos demostrando una tautología
1. Nuestra primera subprueba: suponemos que el lado izquierdo muestra que el lado derecho se sigue
2. Una subsubprueba: somos libres de suponer lo que queramos. Aquí buscamos un reductio ad absurdum
3. Ahora tenemos una contradicción
4. Se nos permite anteponer un no al enunciado que "causó" la contradicción
5. Nuestra segunda subprueba: suponemos que el lado derecho muestra que el lado izquierdo se sigue
6. Invocamos la regla que nos permite eliminar un número par de no de un prefijo de enunciado
7. De 1 a 4 hemos demostrado que si P entonces no no P, de 5 a 6 hemos demostrado que P si no no P; por lo tanto, se nos permite introducir el bicondicional en 7, donde iff representa si y solo si