Saltar al contenido
Topos Uranos
Español

Sistemas deductivos formales

Resumen

Esta clase convierte el lenguaje de la unidad anterior en un instrumento para demostrar. Define qué es un sistema deductivo formal (un lenguaje, unos esquemas de axiomas y unas reglas de inferencia) y presenta el primero de los dos con que trabaja el curso, el sistema de Łukasiewicz: tres esquemas de axiomas y el modus ponens como regla única. Define con precisión la deducción desde un conjunto de premisas, el teorema y la relación Γ⊢φ\Gamma \vdash \varphi, deduce ⊢(φ→φ)\vdash (\varphi \rightarrow \varphi) en cinco líneas y demuestra las propiedades estructurales de la deducción: presunción, monotonía, modus ponens entre deducciones, corte y carácter finito. Demuestra después, por inducción fuerte sobre el número de líneas, el teorema de deducción y su recíproco, que permiten razonar con deducciones sobre deducciones, y define la equivalencia probada. Por último, establece sin recurrir a los valores de verdad el límite de ese sistema en una lengua cuyo único conector es la negación conjunta: una marca de 00 y 11, calculada por recursión sobre las fórmulas, que los axiomas de Łukasiewicz y el modus ponens conservan, prueba que ciertas fórmulas que deberían deducirse no se deducen, y que ni siquiera se pasa de (v1↓v2)(v_{1} \downarrow v_{2}) a (¬¬v1↓v2)(\neg\neg v_{1} \downarrow v_{2}). De ello se sigue la necesidad de una segunda regla, el reemplazo de la doble negación, con la que la clase siguiente completa el sistema.

Objetivos de aprendizaje

  1. Reconocer las instancias de los esquemas A1, A2 y A3 y decidir si una sucesión de fórmulas es una deducción desde un conjunto de premisas.
  2. Construir deducciones en el sistema de Łukasiewicz, con axiomas, premisas y modus ponens, y deducciones sobre deducciones con presunción, monotonía, corte, el teorema de deducción y su recíproco.
  3. Demostrar las propiedades estructurales de la deducción y el teorema de deducción por inducción fuerte sobre el número de líneas.
  4. Establecer equivalencias probadas y usar que la equivalencia probada es reflexiva, simétrica y transitiva.
  5. Demostrar que una fórmula no es deducible mediante una marca que los axiomas y el modus ponens conservan, y explicar con ella el límite del sistema de Łukasiewicz en la lengua de un solo conector y por qué hace falta una segunda regla.

Qué es un sistema deductivo formal

La unidad anterior construyó un lenguaje: decidió qué cadenas de círculos y discos son fórmulas, y nada más. Ahora bien, un lenguaje por sí solo no afirma ni demuestra nada; para demostrar se necesita, además, un punto de partida y un modo de avanzar. Un sistema deductivo formal consta, por tanto, de tres componentes: un lenguaje formal, que fija las fórmulas; un conjunto de axiomas, fórmulas que se admiten sin demostración; y un conjunto de reglas de inferencia, que dicen qué fórmula puede escribirse a partir de otras ya escritas. Lo decisivo es que las tres cosas son puramente sintácticas: para comprobar que una fórmula es un axioma, o que una regla se aplicó bien, basta mirar las cadenas, sin preguntar qué significan. Si esto es así, una demostración en un sistema formal puede revisarse mecánicamente, signo por signo, y en esa posibilidad reside todo su valor.

Conviene advertir desde el comienzo que un axioma no es aquí una «verdad evidente por sí misma», como en el uso antiguo de la palabra, sino una fórmula elegida como punto de partida. Que la elección sea acertada (que los axiomas sean verdaderos en un sentido que la semántica precisará, y que basten para deducir todo lo que debe deducirse) es una pregunta sobre el sistema, que se responde con teoremas acerca de él y no con la intuición: la unidad sobre la metateoría la responde, y la última sección de esta clase muestra que la pregunta no es ociosa.

Esquemas de axiomas e instancias

Los sistemas de la lógica proposicional no enuncian sus axiomas uno por uno, porque son infinitos, sino mediante esquemas: expresiones del metalenguaje escritas con metavariables, como (φ→(ψ→φ))(\varphi \rightarrow (\psi \rightarrow \varphi)). Un esquema no es una fórmula; es un molde. Una instancia del esquema es la fórmula que resulta de reemplazar cada metavariable por una fórmula, de modo uniforme: todas las apariciones de una misma metavariable se reemplazan por la misma fórmula, aunque metavariables distintas pueden recibir la misma fórmula o fórmulas distintas.

EjemploInstancias de un esquema

Con φ:=v1\varphi := v_{1} y ψ:=¬v2\psi := \neg v_{2}, el esquema (φ→(ψ→φ))(\varphi \rightarrow (\psi \rightarrow \varphi)) da la instancia (v1→(¬v2→v1))(v_{1} \rightarrow (\neg v_{2} \rightarrow v_{1})); con φ:=(v1↓v2)\varphi := (v_{1} \downarrow v_{2}) y ψ:=(v1↓v2)\psi := (v_{1} \downarrow v_{2}), da ((v1↓v2)→((v1↓v2)→(v1↓v2)))((v_{1} \downarrow v_{2}) \rightarrow ((v_{1} \downarrow v_{2}) \rightarrow (v_{1} \downarrow v_{2}))), porque nada impide que dos metavariables reciban la misma fórmula. En cambio, (v1→(v2→v3))(v_{1} \rightarrow (v_{2} \rightarrow v_{3})) no es instancia de ese esquema: la primera y la última aparición de φ\varphi recibirían fórmulas distintas, y el reemplazo no sería uniforme. Cada instancia, una vez desplegadas las abreviaturas, es una cadena de círculos y discos; el esquema, en cambio, vive solo en el metalenguaje.