Una construcción algorítmica de la "Prueba Condicional" o "Teorema de la Deducción".
Se presenta la demostración de la llamada "prueba condicional"
en la lógica proposicional (tambien llamada "teorema de la
deducción"); que consiste en que: si en una derivación con
premisas C1, C2,..., Cn, se pone como hipótesis extra la fórmula A y
de ahí se deduce B (usando tal vez las Ci), entonces decimos que por
prueba condicional deducimos la fórmula (A-->B). Y ya no consideramos
la A como hipótesis.
La pregunta es: ¿realmente dedujimos la fórmula (A-->B) de las
premisas C1,...,Cn? La respuesta es NO! Dedujimos B a partir de A (y
las Ci), pero decimos que la regla "prueba condicional" nos permite
decir que se puede tener una prueba de (A-->B). Demostraremos que eso
está bien, demostrándolo y además construyendo dicha prueba de modo
algorítmico es decir, como cuando aplicamos una receta y lo podemos
hacer mecánicamente.
En el resumen extenso anexo en PDF, se explica con detalle esto en un
sistema axiomático particular que también puede verse en [Amor]
pags. 141-143. También en el anexo se usa que para cualquier fórmula A,
es un teorema demostrado la fórmula (A-->A). Eso no está demostrado
ahí, por lo que termino este breve resumen con esa prueba; para
entenderla véanse los axiomas en el resumen extenso o bien en [Amor].
Demostración de que para cualquier fórmula A es teorema formal en el sistema dado, la fórmula (A-->A):
1. (A-->((A-->A)-->A)) Ax.1
2. [(A-->((A-->A)-->A))]-->[(A-->(A-->A))-->(A-->A)] Ax.2
3. (A-->(A-->A))-->(A-->A) MP1,2
4. (A-->(A-->A) Ax. 1
5. (A-->A) MP 4,3
[Amor] Compacidad en la lógica de primer orden y su relación con el teorema de completud, José Alfredo Amor,
Facultad de Ciencias, UNAM, 2006.