Lógica

Sistema Formal

La presentación anterior sugiere que la lógica proposicional puede verse como un sistema formal (o cálculo), con tres componentes:

Definición 1 — Sistema formal proposicional

Un sistema formal proposicional consiste en:

  1. Lenguaje: las expresiones booleanas definidas anteriormente
  2. Axiomas: un conjunto de expresiones booleanas que se aceptan como verdaderas sin demostración (las propiedades marcadas como "Axioma" arriba)
  3. Reglas de inferencia: mecanismos para derivar nuevas verdades a partir de verdades conocidas

Reglas de inferencia

Las reglas de inferencia permiten derivar nuevas expresiones válidas a partir de expresiones ya establecidas. Las dos reglas fundamentales son:

Definición 2 — Regla de sustitución

Si EE es un teorema (expresión válida) y vv es una variable, entonces E[v:=F]E[v := F] (el resultado de reemplazar toda ocurrencia de vv en EE por la expresión FF) también es un teorema.

EE[v:=F]\frac{E}{E[v := F]}

Definición 3 — Regla de Leibniz

Si X=YX = Y es un teorema, entonces para cualquier expresión EE y variable zz:

X=YE[z:=X]=E[z:=Y]\frac{X = Y}{E[z := X] = E[z := Y]}

Es decir: si dos expresiones son iguales, se puede sustituir una por la otra en cualquier contexto.

Definición 4 — Regla de transitividad

X=Y,Y=ZX=Z\frac{X = Y, \quad Y = Z}{X = Z}

Qué es un teorema

Definición 5 — Teorema del sistema formal

Un teorema del cálculo proposicional es una expresión booleana que:

  • Es un axioma, o
  • Se obtiene a partir de axiomas y teoremas ya demostrados mediante las reglas de inferencia

Todo teorema es una tautología: es verdadero en todos los estados posibles.

El poder de este enfoque es que permite razonar sintácticamente: podemos manipular fórmulas aplicando reglas mecánicas, sin necesidad de evaluar tablas de verdad. Esto es especialmente útil cuando las expresiones tienen muchas variables, donde las tablas de verdad crecen exponencialmente.

Ejemplo de prueba formal

Para ilustrar el estilo de prueba ecuacional, demostremos que p∧⊤≡pp \land \top \equiv p:

Teorema 1 — Identidad de la conjunción

p∧⊤≡pp \land \top \equiv p

▶Demostración

Usamos la regla dorada: p∧q≡p⇔q⇔p∨qp \land q \equiv p \Leftrightarrow q \Leftrightarrow p \lor q. Sustituyendo q:=⊤q := \top:

p∧⊤≡p⇔⊤⇔p∨⊤p \land \top \equiv p \Leftrightarrow \top \Leftrightarrow p \lor \top

Sabemos que p∨⊤≡⊤p \lor \top \equiv \top (dominación) y p⇔⊤≡pp \Leftrightarrow \top \equiv p (identidad de ⇔\Leftrightarrow). Entonces:

p∧⊤≡p⇔⊤⇔⊤p \land \top \equiv p \Leftrightarrow \top \Leftrightarrow \top ≡p⇔⊤\equiv p \Leftrightarrow \top ≡p\equiv p

QED

Este estilo ecuacional, donde cada paso transforma una expresión en otra equivalente con una justificación explícita, es el corazón del razonamiento formal en lógica proposicional.