Nivel 3 · Lógica y deducción natural
Verdad: semántica de tablas
Frente al enfoque sintáctico de la página anterior, la semántica se ocupa del significado de las fórmulas, es decir, de sus valores de verdad. La noción básica es la valuación , y sobre ella se definen la consecuencia semántica y la tautología . La presentación sigue a Huth y Ryan (2004) .
El conjunto de valores de verdad es . Una valuación (o modelo) es una función que asigna un valor de verdad a cada átomo. Por ejemplo, para una valuación posible es , .
Las tablas de los conectivos
El valor de una fórmula compleja se determina composicionalmente a partir de sus átomos y del significado de los conectivos, fijado por las tablas de verdad.
La implicación solo es falsa cuando el antecedente es verdadero () y el consecuente falso (); partir de una falsedad nunca invalida la implicación. Esta es la lectura que se traslada literalmente a la evaluación recursiva de fórmulas en la formalización en Lean (nivel 7, próximamente).
Evaluar una fórmula completa
Con estas tablas se evalúa cualquier fórmula. Por ejemplo, :
La columna final da el valor de la fórmula para cada valuación de sus átomos. Esta maquinaria permite definir con precisión la consecuencia lógica.
es consecuencia semántica de , escrito , si ninguna valuación hace verdaderas a todas las premisas y falsa a la conclusión. Intuitivamente: en todo mundo donde las premisas son ciertas, la conclusión también lo es.
- es una tautología, escrito , si es verdadera para toda valuación (por ejemplo ).
- es una contradicción si es falsa para toda valuación (por ejemplo ).
- es satisfacible si alguna valuación la hace verdadera. La fórmula anterior, , es satisfacible pero no tautología.
Compruébalo tú mismo
El constructor de abajo genera una columna por subfórmula, con la semántica composicional a la vista: al pasar el cursor por una columna aparece la cláusula que la justifica, y el veredicto final clasifica la fórmula como tautología, contradicción o contingencia.
Ejercicio: la definibilidad del fragmento mínimo. La
Nota 9.2afirma que , y son definibles a partir de y «como se verifica con tablas de verdad». Esa verificación es exactamente lo que el constructor hace. Compruébese que las dos bicondicionales
son tautologías (en la notación ASCII del constructor: (p | q) <-> (~p -> q) y
(p & q) <-> ~(p -> ~q)), y que (en ASCII: ~(p -> p)) es una
contradicción, es decir, se comporta exactamente como .
Constructor de tablas de verdad
| T | T | T | T | T | F | F | T | T |
| T | F | T | F | F | T | F | F | T |
| F | T | F | T | T | F | T | T | T |
| F | F | F | F | T | T | T | T | T |
Pasa el cursor por una columna para ver la cláusula semántica que la justifica.
Veredicto: tautología — verdadera bajo TODA valuación: por el teorema de completitud, existe una derivación de ella.
Con los dos planos construidos, el sintáctico () y el semántico (), las dos páginas siguientes demuestran que coinciden: primero la solidez, después la completitud.