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 \vDash y la tautología . La presentación sigue a Huth y Ryan (2004) .

Definición 9.8 (Verdad y valuación)

El conjunto de valores de verdad es {T,F}\{T, F\}. Una valuación (o modelo) es una función vv que asigna un valor de verdad a cada átomo. Por ejemplo, para p¬qp \land \neg q una valuación posible es v(p)=Tv(p) = T, v(q)=Fv(q) = F.

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.

ϕ¬ϕTFFTϕψϕψTTTTFFFTFFFFϕψϕψTTTTFTFTTFFF\begin{array}{c|c} \phi & \neg\phi \\ \hline T & F \\ F & T \end{array} \qquad \begin{array}{cc|c} \phi & \psi & \phi \land \psi \\ \hline T & T & T \\ T & F & F \\ F & T & F \\ F & F & F \end{array} \qquad \begin{array}{cc|c} \phi & \psi & \phi \lor \psi \\ \hline T & T & T \\ T & F & T \\ F & T & T \\ F & F & F \end{array} ϕψϕψTTTTFFFTTFFT\begin{array}{cc|c} \phi & \psi & \phi \rightarrow \psi \\ \hline T & T & T \\ T & F & F \\ F & T & T \\ F & F & T \end{array}

La implicación solo es falsa cuando el antecedente es verdadero (v(ϕ)=Tv(\phi)=T) y el consecuente falso (v(ψ)=Fv(\psi)=F); 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, (p¬q)(q¬p)(p \rightarrow \neg q) \rightarrow (q \lor \neg p):

pq¬p¬qp¬qq¬p(p¬q)(q¬p)TTFFFTTTFFTTFFFTTFTTTFFTTTTT\begin{array}{c|c||c|c|c|c||c} p & q & \neg p & \neg q & p \rightarrow \neg q & q \lor \neg p & (p \rightarrow \neg q) \rightarrow (q \lor \neg p) \\ \hline T & T & F & F & F & T & T \\ T & F & F & T & T & F & F \\ F & T & T & F & T & T & T \\ F & F & T & T & T & T & T \end{array}

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.

Definición 9.9 (Consecuencia semántica)

ψ\psi es consecuencia semántica de {ϕ1,,ϕn}\{\phi_1, \ldots, \phi_n\}, escrito ϕ1,,ϕnψ\phi_1, \ldots, \phi_n \vDash \psi, 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.

Definición 9.10 (Tautología, contradicción y satisfacibilidad)
  • ϕ\phi es una tautología, escrito ϕ\vDash \phi, si es verdadera para toda valuación (por ejemplo p¬pp \lor \neg p).
  • ϕ\phi es una contradicción si es falsa para toda valuación (por ejemplo p¬pp \land \neg p).
  • ϕ\phi es satisfacible si alguna valuación la hace verdadera. La fórmula anterior, (p¬q)(q¬p)(p \rightarrow \neg q) \rightarrow (q \lor \neg p), 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.2

afirma que \vee, \wedge y \bot son definibles a partir de ¬\neg y \rightarrow «como se verifica con tablas de verdad». Esa verificación es exactamente lo que el constructor hace. Compruébese que las dos bicondicionales

(pq)(¬pq),(pq)¬(p¬q)(p \vee q) \leftrightarrow (\neg p \rightarrow q), \qquad (p \wedge q) \leftrightarrow \neg(p \rightarrow \neg q)

son tautologías (en la notación ASCII del constructor: (p | q) <-> (~p -> q) y (p & q) <-> ~(p -> ~q)), y que ¬(pp)\neg(p \rightarrow p) (en ASCII: ~(p -> p)) es una contradicción, es decir, se comporta exactamente como \bot.

Constructor de tablas de verdad

(o en ASCII: ~ & | -> <->)
ppqqppqqpqp \rightarrow q¬q\neg q¬p\neg p¬q¬p\neg q \rightarrow \neg ppq¬q¬pp \rightarrow q \leftrightarrow \neg q \rightarrow \neg p
TTTTTFFTT
TFTFFTFFT
FTFTTFTTT
FFFFTTTTT

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 (\vdash) y el semántico (\vDash), las dos páginas siguientes demuestran que coinciden: primero la solidez, después la completitud.