18 Correccion, completitud y decidibilidad

El sistema formal de Gentzen es un modelo formal de la logica proposicional, vista en el Tema 3 (sin incluir los simbolos $\top$ y $\perp$).

El sistema formado por la sintaxis de la logica proposicional, sin axiomas y con las reglas de inferencia:

• •
  ​

  $I\neg,E\neg,I\wedge,E\wedge,I\vee,I\to,E\to$

• •
  ​

  $E\vee^{\prime}:\left\{A\vee B\right\}\vdash A,\left\{A\vee B\right\}\vdash B$

no es correcto.

El sistema formado por la sintaxis de la logica proposicional, sin axiomas y con las reglas de inferencia:

• •
  ​

  $I\neg,E\neg,I\wedge,E\wedge,I\vee,I\to,E\to$

no es completo.

Asumamos que ya sabemos que el sistema de Gentzen es correcto y completo. Demostrar que el siguiente sistema es completo:

El sistema formado por la sintaxis de la logica proposicional, sin axiomas y con las reglas de inferencia:

• •
  ​

  $I\neg,E\neg,I\wedge,E\wedge,I\vee,I\to,E\to$

• •
  ​

  $TP:\left\{A\vee B,\neg B\right\}\vdash A,\left\{A\vee B,\neg A\right\}\vdash B$.

Obs: el sistema de con las 7 reglas y TP es correcto. Si fuera incorrecto, podria demostrar un teorema que no fuera tautologia usando esas reglas, pero como TP es demostrar en Gentzen, eso implicaria que Gentzen es incorrecto.

Tenemos que ver que el sistema propuesto es completo. Para ello, basta con ver que $E\vee$ se puede demostrar en este sistema y luego usar que Gentzen es completo.

En el sistema nuevo:

1. 1.
   ​

   $A\rightarrow C$ Pr

2. 2.
   ​

   $B\rightarrow C$ Pr

3. 3.
   ​

   $A\vee B$ Pr