Un aparato formal que consiste en un lenguaje formal junto con un conjunto de axiomas (o esquemas axiomáticos) y reglas de inferencia que determinan qué secuencias de fórmulas cuentan como derivaciones válidas de premisas a conclusiones.

Principio

Especificar verdades primitivas y pasos de transformación permitidos de modo que la derivabilidad sea comprobable mecánicamente y preserve propiedades semánticas deseadas como corrección y completitud respecto a una semántica.

Demostración

Un sistema deductivo al estilo Hilbert para lógica proposicional puede tener esquemas de axiomas y modus ponens como única regla; dadas instancias de axiomas, el uso repetido de modus ponens deriva teoremas.

Aplicación incorrecta

Combinar reglas de inferencia sin atender a la captura de variables o condiciones laterales —por ejemplo aplicar la instanciación universal en una fórmula donde la variable está ligada en otro contexto— produce derivaciones inválidas y pruebas no correctas.

Consecuencia

Un sistema deductivo bien especificado precisa la demostrabilidad, permite la búsqueda y mecanización de pruebas y respalda resultados metateóricos (por ejemplo consistencia, decidibilidad, completitud) al compararlo con la semántica.

Inversión

La visión inversa enfatiza la consecuencia semántica por sí sola (modelos y consecuencia) y considera las reglas y axiomas como artefactos secundarios en lugar de la definición principal de consecuencia.

Límite

Se refiere a sistemas formales con reglas sintácticas explícitas; no incluye la argumentación informal, la inferencia empírica ni nociones puramente modelo-teóricas de consecuencia que omiten derivaciones sintácticas.

Tensión semántica

Existe tensión entre definiciones prueba-teóricas de consecuencia (derivabilidad dentro de un sistema) y definiciones semánticas (entailment en todos los modelos); se requieren teoremas de corrección y completitud para reconciliarlas.

Síntesis

Un sistema deductivo es el motor sintáctico para generar pruebas formales: los axiomas proporcionan fórmulas iniciales y las reglas de inferencia pasos lícitos, definiendo en conjunto la relación de derivabilidad en una lógica.