16 Teorema de la deduccion

Example 16.1.

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.

Example 16.2.

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.

Theorem 16.3 (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
Proof 16.4.

⇒)\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}
Remark 16.5.

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

Remark 16.6.

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.