16 Teorema de la deduccion

Ejemplo IV.8.

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

Ejemplo IV.9.

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

Teorema IV.1 (de la deduccion).

Sean n≥1n\geq 1 y φ1,φ2,…,φn,φ\varphi_{1},\varphi_{2},\ldots,\varphi_{n},\varphi una coleccion de formulas. Entonces

{φ1,φ2,…,φn}⊢φ\left\{\varphi_{1},\varphi_{2},\ldots,\varphi_{n}\right\}\vdash\varphi

si y solo si

{φ1,φ2,…,φn−1}⊢φn→φ\left\{\varphi_{1},\varphi_{2},\ldots,\varphi_{n-1}\right\}\vdash\varphi_{n}\rightarrow\varphi
Demostración.

⇒)\Rightarrow) Si tengo una demostracion

φ1⋮φnα1⋮αmφ⇒φ1⋮φn−1φn Pr auxα1⋮αmφφn→φDemostracion del 2\begin{array}[]{c}\varphi_{1}\\ \vdots\\ \varphi_{n}\\ \alpha_{1}\\ \vdots\\ \alpha_{m}\\ \varphi\end{array}\Rightarrow\begin{array}[]{c}\varphi_{1}\\ \vdots\\ \varphi_{n-1}\\ \varphi_{n}\text{ Pr aux}\\ \alpha_{1}\\ \vdots\\ \alpha_{m}\\ \varphi\\ \varphi_{n}\rightarrow\varphi\\ \text{Demostracion del 2}\end{array}

⇐)\Leftarrow)

φ1⋮φn−1β⋮βmφn→φ⇒φ1⋮φn−1φnβ1⋮βmφn→φφE→a,b\begin{array}[]{c}\varphi_{1}\\ \vdots\\ \varphi_{n-1}\\ \beta\\ \vdots\\ \beta_{m}\\ \varphi_{n}\rightarrow\varphi\end{array}\Rightarrow\begin{array}[]{c}\varphi_{% 1}\\ \vdots\\ \varphi_{n-1}\\ \varphi_{n}\\ \beta_{1}\\ \vdots\\ \beta_{m}\\ \varphi_{n}\rightarrow\varphi\\ \varphi E\rightarrow a,b\end{array}

∎

Observación IV.4.

No se puede demostrar que un razonamiento es incorrecto con Gentzen.

Observación IV.5.

El teorema de la deduccion permite transformar cualquier razonamiento valido del sistema de Gentzen en un teorema de ese sistema. Por ejemplo, si

{φ1,φ2}⊢φ\left\{\varphi_{1},\varphi_{2}\right\}\vdash\varphi

es un razonamiento valido, entonces

⊢φ1→(φ2→φ)\vdash\varphi_{1}\rightarrow(\varphi_{2}\rightarrow\varphi)

es un teorema.