15 El sistema de Gentzen para la logica proposicional

Definition 15.1 (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.

Definition 15.2 (Regla de eliminacion de la negacion, E⁢¬E\neg).
¬¬AA\begin{array}[]{c}\neg\neg A\\ \hline\cr A\end{array}
Definition 15.3 (Regla de introduccion de la conjuncion, I∧I\wedge).
ABA∧B\begin{array}[]{c}A\\ B\\ \hline\cr A\wedge B\end{array}
Definition 15.4 (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}
Definition 15.5 (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}
Definition 15.6 (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}
Example 15.7.

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

Example 15.8.

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

Example 15.9.

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

Definition 15.10 (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.

Remark 15.11.

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.

Example 15.12.

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)

Definition 15.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}
Remark 15.14.

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}

Example 15.15.

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

Definition 15.16 (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}
Remark 15.17.

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.

Example 15.18.

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

Example 15.19.

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