Regla de inferencia

La versión actual de la página aún no ha sido revisada por colaboradores experimentados y puede diferir significativamente de la versión revisada el 9 de noviembre de 2021; la verificación requiere 1 edición .

Una regla de inferencia es un procedimiento eficiente para verificar que una fórmula dada en la teoría bajo consideración es directamente derivable en un paso de otras fórmulas dadas.

En una teoría no contradictoria, los teoremas se obtienen encadenando la aplicación de las reglas de inferencia de esa teoría. Además, si la fórmula se deriva en un cierto número de pasos de las fórmulas , entonces se usa la notación para expresar este hecho . Si en tal caso la teoría bajo consideración es consistente , y cada uno de los enunciados es un axioma o un teorema, entonces también es un teorema.

En el cálculo de predicados en la versión de Hilbert , las reglas de inferencia son el modus ponens y la regla de generalización . Por el teorema de completitud de Gödel, una fórmula es derivable en un cálculo de predicados de primer orden si y solo si es válida , es decir, verdadera en cualquier interpretación de ese cálculo de predicados.

En los cálculos de tipo Gentzen ( cálculo secuencial , sistemas de inferencia natural ), las reglas de inferencia juegan un papel importante: utilizan una pequeña cantidad de axiomas y sistemas desarrollados de reglas de inferencia. En la teoría de la demostración , son precisamente estos cálculos los que se utilizan, ya que debido a la selección de sistemas simétricos de reglas de inferencia, es posible obtener resultados constructivos sobre la consistencia de los sistemas.

Véase también

Literatura