Inducción en la prueba del teorema de solidez

Question

El enunciado del teorema de solidez tanto en lógica proposicional como en lógica de predicados es el siguiente:

$\Sigma \vdash \alpha \rightarrow \Sigma \vDash \alpha$ para $\Sigma \subseteq W, \alpha \in W$ donde $W$ es el conjunto de fórmulas bien formadas de nuestro lenguaje, y supongamos que nuestro sistema de axiomas es $T$ el conjunto de todas las tautologías. Quiero demostrar el teorema, y parece que la táctica más común (y que me han sugerido) es utilizar la inducción sobre la longitud de $\alpha.$ Desde $\Sigma \vdash \alpha$ Debe haber habido alguna secuencia de deducción $(\alpha_1,\alpha_2,\alpha_3,....\alpha_n=\alpha)$ para $\alpha_i \in \Sigma$ . Entonces, cada $\alpha_i$ ha surgido de uno de los siguientes:

1. $\alpha_i$ era parte de las hipótesis,
2. $\alpha_i$ es una tautología
3. $\alpha_i$ seguido de un anterior $\alpha_j$ por la vía del modus ponens.

Si $\alpha$ entra en una de las dos primeras categorías estamos acabados. Entonces, a través del proceso de eliminación, queremos utilizar la inducción debe $\alpha$ se producen como resultado del modus ponens. ¿Cómo se consigue esto exactamente? Parece que hay muchas formas de $\alpha_i$ como resultado del modus ponens - tal vez sea el resultado de $\alpha_j \rightarrow \alpha_i$ o tal vez $\alpha_j \iff \alpha_i$ o incluso $(\alpha_k \rightarrow \alpha_j) \rightarrow \alpha_i$ . ¿Cuántos casos hay?

Answer 1

Como sugiere Mauro, la inducción funciona sobre la longitud de la derivación de $\alpha$ . En otras palabras, la inducción ocurre sobre el número de pasos de la prueba de la fórmula (bien formada).

Entonces, digamos que la longitud de la derivación es 0. Esto constituye el caso base, donde tenemos un axioma que ya es una tautología conocida.

Ahora, supongamos que la solidez se mantiene para cualquier derivación con n pasos. Mostraremos que una derivación con un paso más también será una tautología. Una derivación con un paso más, para su paso S(n) (el paso sucesor de n) será

1. Instanciar un axioma. En tal caso, el siguiente paso es una tautología. Dado que todos los pasos anteriores eran tautologías, todos los miembros de la prueba son tautologías y el resultado se deduce.
2. Instanciar un teorema previamente probado en la secuencia. En tal caso, el siguiente paso que es una instancia de una tautología es también una tautología. Así que, de nuevo, como todos los pasos anteriores eran tautologías, todos los miembros de la prueba son tautologías y el resultado se deduce.
3. Sigue con el uso del modus ponens de los pasos anteriores de la secuencia. Ahora, los pasos anteriores serían algún condicional y el antecedente de ese condicional. Pero, por la hipótesis de inducción, al ser pasos previos, ambos son tautologías. Y cuando A y (A $\rightarrow$ B) son tautologías, también lo es B. B es el nuevo paso en este caso. Como todos los pasos anteriores eran tautologías, y el nuevo paso también es una tautología, se deduce que todos los miembros de la prueba son tautologías.

Esto cubre todos los casos posibles. Por lo tanto, por inducción sobre la longitud de la derivación de la fórmula $\alpha$ se deduce el metateorema de solidez.