16 Teorema de la deduccion

Ejemplo.

Demostrar la validez de {prs,rq}pqs\displaystyle\{p\rightarrow r\wedge s,r\rightarrow q\}\vdash p\rightarrow q\wedge s.

Ejemplo.

Demostrar la validez de {prs,rq,p}qs\displaystyle\{p\rightarrow r\wedge s,r\rightarrow q,p\}\vdash q\wedge s.

Teorema 16.1 (de la deduccion).

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

{φ1,φ2,,φn}φ\displaystyle\{\varphi_{1},\varphi_{2},\ldots,\varphi_{n}\}\vdash\varphi

si y solo si

{φ1,φ2,,φn1}φnφ\displaystyle\{\varphi_{1},\varphi_{2},\ldots,\varphi_{n-1}\}\vdash\varphi_{n}\rightarrow\varphi
Demostración.

)\displaystyle\Rightarrow) Si tengo una demostracion

φ1φnα1αmφφ1φn1φn Pr auxα1αmφφnφDemostracion del 2\displaystyle\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{ \small Pr aux}\\ \alpha_{1}\\ \vdots\\ \alpha_{m}\\ \varphi\\ \varphi_{n}\rightarrow\varphi\\ \text{Demostracion del 2}\end{array}

)\displaystyle\Leftarrow)

φ1φn1ββmφnφφ1φn1φnβ1βmφnφφEa,b\displaystyle\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.

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

Observación.

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}φ\displaystyle\{\varphi_{1},\varphi_{2}\}\vdash\varphi

es un razonamiento valido, entonces

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

es un teorema.