Se necesita ayuda con el ejercicio * 148 en SC Kleene Introducción a las metamatemáticas.
Dejar $x$ ser una variable, $A(x)$ una fórmula y $y$ una variable distinta de $x$ que es gratis para $x$ en $A(x)$ y no ocurre gratis en $A(x)$.
Dejar $Q(x)$ ser: $\forall y [y<x \Rightarrow \lnot A(y)]$.
Necesito ayuda para demostrar que $Q(x), \lnot A(x) \vdash Q(x')$ usando el sistema de Kleene (aquí 'es el sucesor).
Esta es la última parte del ejercicio * 148 (principio de número mínimo para un segmento inicial de los números naturales) página 190 en Introducción a las metamatemáticas de Kleene. Según Kleene, esto debería usarse:$\vdash a\le b \sim a \lt b'$
Gracias
Respuestas
Vamos a utilizar el siguiente lema: $y < x' \rightarrow y = x \vee y < x$. Esto se puede derivar de varias formas: por ejemplo, a través de un argumento de inducción, o simplemente apelando a 139 y 141 establecidos anteriormente.
Daré una prueba de deducción natural de $Q(x), \neg A(x) \vdash Q(x')$. Es posible que el sistema que utilizo no se corresponda exactamente con el de Kleene, pero debería parecerse lo suficiente para que pueda traducir entre ellos. Avísame si eso te da algún problema.
Dado que su conclusión deseada es $\forall y. y < x' \rightarrow \neg A(y)$, puede comenzar su demostración con cuatro suposiciones y trabajar hacia una contradicción.
- Asumir $\forall y. y < x \rightarrow \neg A(y)$ - es decir $Q(x)$
- Asumir $\neg A(x)$.
- Asumir $y < x'$.
- Asumir $A(y)$.
- Tener $y < x' \rightarrow y = x \vee y < x$ (por el lema discutido anteriormente).
- Tener $y = x \vee y < x$ (de 5 y 1 usando eliminación de implicaciones).
- Asumir $y=x$.
- Tener $A(x)$ (de 7 y 4 con sustitución).
- Tiene una contradicción (de 8 y 2).
- Tener $y = x \rightarrow \neg A(y)$ (de 7-9 por contradicción, descartando el supuesto 7).
- Tener $y<x \rightarrow \neg A(y)$ (de 1 por eliminación universal).
- Tener $\neg A(y)$ (de 6, 10, 11 usando eliminación de disyunción).
- Tiene una contradicción (de 12 y 4).
- Tener $\neg A(y)$ (de 4-13 por introducción de negación, descargando el supuesto 4).
- Tener $y < x' \rightarrow \neg A(y)$ (de 3-14 por introducción implícita, descargando el supuesto 3).
- Tener $\forall y. y<x' \rightarrow \neg A(y)$(de 15 por introducción universal), QED .