15 El sistema de Gentzen para la logica proposicional ‣ Parte IV Teoria de la demostracion para logica proposicional ‣ Lógica‣ Parte IV Teoria de la demostracion para logica proposicional ‣ Lógica

Definición 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 $\displaystyle\top$ ni $\displaystyle\perp$ en el alfabeto.
- •
  
  No consideramos que $\displaystyle\leftrightarrow$ sea una conectiva binaria. La usaremos como una abreviatura:
  
  $\displaystyle\varphi\leftrightarrow\psi$ se considera una abreviatura de $\displaystyle(\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:

$\displaystyle E\neg$	$\displaystyle I\neg$
$\displaystyle E\wedge$	$\displaystyle I\wedge$
$\displaystyle E\vee$	$\displaystyle I\vee$
$\displaystyle E\rightarrow$	$\displaystyle I\rightarrow$

Definición 15.2 (Regla de eliminacion de la negacion, $\displaystyle E\neg$ ).

\displaystyle\begin{array}[]{c}\neg\neg A\\ \hline\cr A\end{array}

Definición 15.3 (Regla de introduccion de la conjuncion, $\displaystyle I\wedge$ ).

\displaystyle\begin{array}[]{c}A\\ B\\ \hline\cr A\wedge B\end{array}

Definición 15.4 (Regla de eliminacion de la conjuncion, $\displaystyle E\wedge$ ).

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

\displaystyle\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 15.5 (Regla de introduccion de la disyuncion, $\displaystyle I\vee$ ).

Tambien son dos reglas que llamaremos con el mismo nombre:

\displaystyle\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 15.6 (Regla de eliminacion de la implicacion, $\displaystyle E\rightarrow$ ).

Tambien recibe el nombre de modus ponens.

\displaystyle\begin{array}[]{c}A\\ A\rightarrow B\\ \hline\cr B\end{array}

Ejemplo.

Demostrar la validez de $\displaystyle\{p,p\rightarrow q\}\vdash p\wedge q$ .

1.

$\displaystyle p$ Premisa
2.

$\displaystyle p\rightarrow q$ Premisa
3.

$\displaystyle q\quad$ $\displaystyle E\rightarrow,1,2$
4.

$\displaystyle p\wedge q\quad$ $\displaystyle I\wedge,1,3$

Ejemplo.

Demostrar la validez de $\displaystyle\{p\wedge q\rightarrow r,q\rightarrow p,q\}\vdash r$ .

1.

$\displaystyle p\wedge q\rightarrow r$ Premisa
2.

$\displaystyle q\rightarrow p$ Premisa
3.

$\displaystyle q$ Premisa
4.

$\displaystyle p$ $\displaystyle\quad E\rightarrow,2,3$
5.

$\displaystyle p\wedge q$ $\displaystyle\quad I\wedge,3,4$
6.

$\displaystyle r$ $\displaystyle\quad E\rightarrow,1,5$

Ejemplo.

Demostrar la validez de $\displaystyle\{\neg\neg p,p\rightarrow q\wedge\neg\neg r,\neg p\vee q% \rightarrow s\}\vdash s\wedge r$

1.

$\displaystyle\neg\neg p$ Premisa
2.

$\displaystyle p\rightarrow q\wedge\neg\neg r$ Premisa
3.

$\displaystyle\neg p\vee q\rightarrow s$ Premisa
4.

$\displaystyle p$ $\displaystyle\quad E\neg,1$
5.

$\displaystyle q\wedge\neg\neg r$ $\displaystyle\quad E\rightarrow,4,2$
6.

$\displaystyle q\quad E\wedge,5$
7.

$\displaystyle\neg p\vee q\quad I\vee,6$
8.

$\displaystyle s\quad E\rightarrow,7,3$
9.

$\displaystyle\neg\neg r\quad E\wedge,5$
10.

$\displaystyle r\quad E\neg,9$
11.

$\displaystyle s\wedge r\quad I\wedge,8,10$

Definición 15.7 (Regla de introduccion de la implicacion, $\displaystyle I\rightarrow$ ).

donde la “caja” es una demostracion auxiliar cuya primera linea es $\displaystyle A$ , que se supone temporalmente valida como premisa auxiliar y cuya ultima linea es $\displaystyle B$ .

Observación.

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

Ejemplo.

Demostrar la validez de $\displaystyle\{p\rightarrow q,p\rightarrow r\}\vdash p\rightarrow q\wedge r$ .

1.

$\displaystyle p\rightarrow q$ Premisa
2.

$\displaystyle p\rightarrow r$ Premisa

3. $\displaystyle p$ Pr aux 4. $\displaystyle q\quad E\to,1,3$ 5. $\displaystyle r\quad E\to,2,3$ 6. $\displaystyle q\wedge r\quad I\wedge,4,5$

7.

$\displaystyle p\to q\wedge r\quad I\to(3-6)$

Definición 15.8 (Regla de introduccion de la negacion, $\displaystyle I\neg$ ).

\displaystyle\begin{array}[]{c}A\rightarrow B\wedge\neg B\\ \hline\cr\neg A\end{array}

Observación.

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

$\displaystyle\neg A\qquad\qquad\text{Premisa auxiliar}$ $\displaystyle\vdots$ $\displaystyle B\wedge\neg B$ $\displaystyle\begin{array}[]{lr}\neg A\rightarrow B\wedge\neg B&I\rightarrow\\ \neg\neg A&I\neg\\ A&E\neg\end{array}$

Ejemplo.

Demostrar la validez de $\displaystyle\{p\rightarrow q,q\rightarrow r,\neg r\}\vdash\neg p$ .

Definición 15.9 (Regla de eliminacion de la disyuncion, $\displaystyle E\vee$ ).

\displaystyle\begin{array}[]{c}A\vee B\\ A\rightarrow C\\ B\rightarrow C\\ \hline\cr C\end{array}

Observación.

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

Ejemplo.

Demostrar la validez de $\displaystyle\{p\rightarrow q,q\rightarrow s,p\vee q\}\vdash r\vee s$

Ejemplo.

Demostrar la validez de $\displaystyle\{p\rightarrow(q\rightarrow r)\}\vdash q\rightarrow(p\rightarrow r)$ .

15 El sistema de Gentzen para la logica proposicional

Definición 15.1 (Sistema de Gentzen).

Definición 15.2 (Regla de eliminacion de la negacion, E⁢¬\displaystyle E\neg).

Definición 15.3 (Regla de introduccion de la conjuncion, I∧\displaystyle I\wedge).

Definición 15.4 (Regla de eliminacion de la conjuncion, E∧\displaystyle E\wedge).

Definición 15.5 (Regla de introduccion de la disyuncion, I∨\displaystyle I\vee).

Definición 15.6 (Regla de eliminacion de la implicacion, E→\displaystyle E\rightarrow).

Ejemplo.

Ejemplo.

Ejemplo.

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

Observación.

Ejemplo.

Definición 15.8 (Regla de introduccion de la negacion, I⁢¬\displaystyle I\neg).

Observación.

Ejemplo.

Definición 15.9 (Regla de eliminacion de la disyuncion, E∨\displaystyle E\vee).

Observación.

Ejemplo.

Ejemplo.

Definición 15.2 (Regla de eliminacion de la negacion, $\displaystyle E\neg$ ).

Definición 15.3 (Regla de introduccion de la conjuncion, $\displaystyle I\wedge$ ).

Definición 15.4 (Regla de eliminacion de la conjuncion, $\displaystyle E\wedge$ ).

Definición 15.5 (Regla de introduccion de la disyuncion, $\displaystyle I\vee$ ).

Definición 15.6 (Regla de eliminacion de la implicacion, $\displaystyle E\rightarrow$ ).

Definición 15.7 (Regla de introduccion de la implicacion, $\displaystyle I\rightarrow$ ).

Definición 15.8 (Regla de introduccion de la negacion, $\displaystyle I\neg$ ).

Definición 15.9 (Regla de eliminacion de la disyuncion, $\displaystyle E\vee$ ).