18 Correccion, completitud y decidibilidad

Definición 18.1.

Todo sistema de demostracino formal se puede ver como un modelo formal de cierto ambito (usualmente formado por objetos matematicos).

Decimos que un sistema formal es

  •  
    ​

    Correcto si todo teorema del sistema formal es una afirmacion verdadera en el ambito que se esta modelando.

  •  
    ​

    Completo si toda afirmacion verdadera en el ambito que se esta modelando es un teorema del sistema formal.

  •  
    ​

    Decidible si existe un procedimiento algoritmico finito para determinar si una formula es un teorema del sistema formal.

Ejemplo.

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

Teorema 18.1.

El sistema de Gentzen es correcto: todo teorema del sistema de Gentzen es una tautologia de la logica proposicional.

Demostración.

No la hacemos con detalle. Es facil: se debe, basicamente, a que todas las 8 reglas de inferencia son razonamientos validos en logica proposicional. ∎

Teorema 18.2.

El sistema de Gentzen es completo: toda tautologia de la logica proposicional es un teorema del sistema de Gentzen.

Demostración.

No la hacemos. ∎

Teorema 18.3.

El sistema de Gentzen es decidible.

Ejemplo.

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

  •  
    ​

    I¬,E¬,I∧,E∧,I∨,I→,E→\displaystyle I\neg,E\neg,I\wedge,E\wedge,I\vee,I\to,E\to

  •  
    ​

    E∨′:{A∨B}⊢A,{A∨B}⊢B\displaystyle E\vee^{\prime}:\{A\vee B\}\vdash A,\{A\vee B\}\vdash B

no es correcto.

Ejemplo.

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

  •  
    ​

    I¬,E¬,I∧,E∧,I∨,I→,E→\displaystyle I\neg,E\neg,I\wedge,E\wedge,I\vee,I\to,E\to

no es completo.

Ejemplo.

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¬,E¬,I∧,E∧,I∨,I→,E→\displaystyle I\neg,E\neg,I\wedge,E\wedge,I\vee,I\to,E\to

  •  
    ​

    T⁢P:{A∨B,¬⁢B}⊢A,{A∨B,¬⁢A}⊢B\displaystyle TP:\{A\vee B,\neg B\}\vdash A,\{A\vee B,\neg A\}\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∨\displaystyle E\vee se puede demostrar en este sistema y luego usar que Gentzen es completo.

En el sistema nuevo:

  1. 1.
    ​

    A→C\displaystyle A\rightarrow C Pr

  2. 2.
    ​

    B→C\displaystyle B\rightarrow C Pr

  3. 3.
    ​

    A∨B\displaystyle A\vee B Pr

4.​¬⁢C\displaystyle\neg C Pr aux 5.​¬⁢AM⁢T⁢4,1\displaystyle\neg A\quad MT4,1 (MT es valido en el sistema nuevo) 6.​BT⁢P⁢,3,5\displaystyle B\quad TP,3,5 7.​CE→,6,2\displaystyle C\quad E\rightarrow,6,2 8.​C∧¬⁢CI∧,4,7\displaystyle C\wedge\neg C\quad I\wedge,4,7

  1. 9.
    ​

    ¬⁢C→C∧¬⁢CI→(4−8)\displaystyle\neg C\rightarrow C\wedge\neg C\quad I\rightarrow(4-8)

  2. 10.
    ​

    ¬⁢¬⁢CI⁢¬⁢,9\displaystyle\neg\neg C\quad I\neg,9

  3. 11.
    ​

    CE⁢¬⁢,10\displaystyle C\quad E\neg,10