15 El sistema de Gentzen para la logica proposicional

Definición IV.6 (Sistema de Gentzen).

El sistema de Gentzen o sistema de deduccion natural para la logica proposicional viene dado por:

  • ​

    Sintaxis: la misma que la de la logica proposicional vista en el tema 2, con dos excepciones:

    • •
      ​

      No incluimos ⊤\top ni ⟂\perp en el alfabeto.

    • •
      ​

      No consideramos que ↔\leftrightarrow sea una conectiva binaria. La usaremos como una abreviatura:

      φ↔ψ\varphi\leftrightarrow\psi se considera una abreviatura de (φ→ψ)∧(ψ→φ)(\varphi\rightarrow\psi)\wedge(\psi\rightarrow\varphi)

  • ​

    El conjunto de axiomas es vacio.

  • ​

    Hay 8 reglas de inferencia que describiremos a continuacion. Sus nombres son:

    E¬E\neg I¬I\neg
    E∧E\wedge I∧I\wedge
    E∨E\vee I∨I\vee
    E→E\rightarrow I→I\rightarrow

En lo que sigue denotaremos con A,B,CA,B,C a formulas cualesquiera de la logica proposicional.

Definición IV.7 (Regla de eliminacion de la negacion, E¬E\neg).
¬¬AA\begin{array}[]{c}\neg\neg A\\ \hline\cr A\end{array}
Definición IV.8 (Regla de introduccion de la conjuncion, I∧I\wedge).
ABA∧B\begin{array}[]{c}A\\ B\\ \hline\cr A\wedge B\end{array}
Definición IV.9 (Regla de eliminacion de la conjuncion, E∧E\wedge).

Son, en realidad, dos reglas que llamaremos con el mismo nombre:

A∧BAA∧BB\begin{array}[]{c}A\wedge B\\ \hline\cr A\end{array}\quad\begin{array}[]{c }A\wedge B\\ \hline\cr B\end{array}
Definición IV.10 (Regla de introduccion de la disyuncion, I∨I\vee).

Tambien son dos reglas que llamaremos con el mismo nombre:

AA∨BBA∨B\begin{array}[]{c}A\\ \hline\cr A\vee B\end{array}\quad\begin{array}[]{c }B\\ \hline\cr A\vee B\end{array}
Definición IV.11 (Regla de eliminacion de la implicacion, E→E\rightarrow).

Tambien recibe el nombre de modus ponens.

AA→BB\begin{array}[]{c}A\\ A\rightarrow B\\ \hline\cr B\end{array}
Ejemplo IV.1.

Demostrar la validez de {p,p→q}⊢p∧q\left\{p,p\rightarrow q\right\}\vdash p\wedge q.

  1. 1.
    ​

    pp Premisa

  2. 2.
    ​

    p→qp\rightarrow q Premisa

  3. 3.
    ​

    qq\quad E→,1,2E\rightarrow,1,2

  4. 4.
    ​

    p∧qp\wedge q\quad I∧,1,3I\wedge,1,3

Ejemplo IV.2.

Demostrar la validez de {p∧q→r,q→p,q}⊢r\left\{p\wedge q\rightarrow r,q\rightarrow p,q\right\}\vdash r.

  1. 1.
    ​

    p∧q→rp\wedge q\rightarrow r Premisa

  2. 2.
    ​

    q→pq\rightarrow p Premisa

  3. 3.
    ​

    qq Premisa

  4. 4.
    ​

    pp E→,2,3\quad E\rightarrow,2,3

  5. 5.
    ​

    p∧qp\wedge q I∧,3,4\quad I\wedge,3,4

  6. 6.
    ​

    rr E→,1,5\quad E\rightarrow,1,5

Ejemplo IV.3.

Demostrar la validez de {¬¬p,p→q∧¬¬r,¬p∨q→s}⊢s∧r\left\{\neg\neg p,p\rightarrow q\wedge\neg\neg r,\neg p\vee q\rightarrow s% \right\}\vdash s\wedge r

  1. 1.
    ​

    ¬¬p\neg\neg p Premisa

  2. 2.
    ​

    p→q∧¬¬rp\rightarrow q\wedge\neg\neg r Premisa

  3. 3.
    ​

    ¬p∨q→s\neg p\vee q\rightarrow s Premisa

  4. 4.
    ​

    pp E¬,1\quad E\neg,1

  5. 5.
    ​

    q∧¬¬rq\wedge\neg\neg r E→,4,2\quad E\rightarrow,4,2

  6. 6.
    ​

    qE∧,5q\quad E\wedge,5

  7. 7.
    ​

    ¬p∨qI∨,6\neg p\vee q\quad I\vee,6

  8. 8.
    ​

    sE→,7,3s\quad E\rightarrow,7,3

  9. 9.
    ​

    ¬¬rE∧,5\neg\neg r\quad E\wedge,5

  10. 10.
    ​

    rE¬,9r\quad E\neg,9

  11. 11.
    ​

    s∧rI∧,8,10s\wedge r\quad I\wedge,8,10

Definición IV.12 (Regla de introduccion de la implicacion, I→I\rightarrow).

donde la “caja” es una demostracion auxiliar cuya primera linea es AA, que se supone temporalmente valida como premisa auxiliar y cuya ultima linea es BB.

Observación IV.1.

Las lineas dentro de la “caja” solo son validas bajo la suposicion temporal de la validez de AA, en el contexto de la demostracion auxiliar. No son validas en la demostracion principal.

Ejemplo IV.4.

Demostrar la validez de {p→q,p→r}⊢p→q∧r\left\{p\rightarrow q,p\rightarrow r\right\}\vdash p\rightarrow q\wedge r.

  1. 1.
    ​

    p→qp\rightarrow q Premisa

  2. 2.
    ​

    p→rp\rightarrow r Premisa

[resume] 1.​pp Pr aux 2.​qE→,1,3q\quad E\to,1,3 3.​rE→,2,3r\quad E\to,2,3 4.​q∧rI∧,4,5q\wedge r\quad I\wedge,4,5

  1. [resume]

  2. 7.
    ​

    p→q∧rI→(3−6)p\to q\wedge r\quad I\to(3-6)

Definición IV.13 (Regla de introduccion de la negacion, I¬I\neg).
A→B∧¬B¬A\begin{array}[]{c}A\rightarrow B\wedge\neg B\\ \hline\cr\neg A\end{array}
Observación IV.2.

El uso tipico de la regla I¬I\neg es para demostraciones que modelan la reduccion al absurdo. Si quiero demostrar AA, supongo ¬A\neg A como premisa auxiliar de una demostracion auxiliar en la que trato de llegar como conclusion a B∧¬BB\wedge\neg B para una formula cualquiera BB. A partir de ahi, deduzco AA:

¬APremisa auxiliar\neg A\qquad\qquad\text{Premisa auxiliar} ⋮\vdots B∧¬BB\wedge\neg B ¬A→B∧¬BI→¬¬AI¬AE¬\begin{array}[]{lr}\neg A\rightarrow B\wedge\neg B&I\rightarrow\\ \neg\neg A&I\neg\\ A&E\neg\end{array}

Ejemplo IV.5.

Demostrar la validez de {p→q,q→r,¬r}⊢¬p\left\{p\rightarrow q,q\rightarrow r,\neg r\right\}\vdash\neg p.

Definición IV.14 (Regla de eliminacion de la disyuncion, E∨E\vee).
A∨BA→CB→CC\begin{array}[]{c}A\vee B\\ A\rightarrow C\\ B\rightarrow C\\ \hline\cr C\end{array}
Observación IV.3.

El uso tipico de la regla E∨E\vee es para demostraciones que modelan el uso de la tecnica de la demostracion por casos. Si quiero demostrar CC y tengo como hipotesis A∨BA\vee B, primero supongo AA como premisa auxiliar de una demostracion auxiliar en la que trato de llegar como conclusion a CC. A continuacion hago lo mismo suponiendo BB como premisa auxiliar.

Ejemplo IV.6.

Demostrar la validez de {p→q,q→s,p∨q}⊢r∨s\left\{p\rightarrow q,q\rightarrow s,p\vee q\right\}\vdash r\vee s

Ejemplo IV.7.

Demostrar la validez de {p→(q→r)}⊢q→(p→r)\left\{p\rightarrow(q\rightarrow r)\right\}\vdash q\rightarrow(p\rightarrow r).