¿Si $A$ es un teorema de lógica clásica, es el caso que $\neg \neg A$ es un teorema de la lógica intuicionista? Y en segundo lugar, si el $A \to B$ es un teorema de lógica clásica, $\neg B \to \neg A$ es un teorema de lógica intuicionista. ¿En tercer lugar, es $\neg A \vee \neg \neg A$ un esquema del teorema de la lógica intuicionista?
Respuestas
¿Demasiados anuncios?
JoshL
Puntos
290
La respuesta a la primera pregunta,
Si $A$ es un teorema de la lógica clásica, es el caso de que $\lnot \lnot A$ es un teorema de intuitionistic lógica?
es "sí" cuando estamos hablando de lógica proposicional. Esta es una muy clásica resultado de Glivenko.
Para la lógica de primer orden, no es suficiente simplemente prefacio la fórmula con dos negaciones. Sin embargo, hay un número de los llamados negativos traducciones que lograr algo similar en una más complicado: para cada uno de primer orden de la fórmula $\phi$ se asocia otra fórmula $\phi^*$ que si $\phi$ es comprobable en el clásico de la lógica de primer orden, a continuación, $\phi^*$ es comprobable en intuitionistic la lógica de primer orden.
Este uso de la negativa de las traducciones es muy estudiado en la prueba de la teoría, y es un método estándar que se ha convertido comúnmente utilizados. Sin embargo, no es realmente accesible la literatura en la prueba de la teoría. El artículo de la Wikipedia vinculado anteriormente tiene algunas de posgrado a nivel de referencias.
Para un intuitionistically comprobante válido de $A \to B \vdash \lnot B \to \lnot A$, con Deducción Natural :
1) $A \to B$ --- premisa
2) $\lnot B$ --- asumido [a]
3) $A$ --- asumido [b]
4) $B$ --- a partir de 1) y 3) por $\to$-eliminación
5) $\bot$ --- de 2) y 4) por $\to$-eliminación : $\lnot B$ es una abreviatura para : $B \to \bot$
6) $\lnot A$ --- a partir de 3) y 5) por $\to$-introducción, la descarga de [b]
7) $\lnot B \to \lnot A$ --- de 2) y 6) por $\to$-introducción, la descarga de [una].
Ningún lugar en la derivación hemos utilizado Exluded Medio, ni la Doble Negación; por lo tanto, la prueba es intuitionistically válido.
Ahora la cuestión es :
si $\vdash_K A \to B$, $\vdash_J ¬B \to ¬A$ o no ?
Whe puede aplicar el Gödel–Gentzen traducción a $⊢_K A \to B$ y tenemos que : $⊢_J ¬¬A \to ¬¬B$.
Pero esto es simplemente un "doble contraposición"; por lo tanto, parece que el $⊢_J ¬B \to ¬A$.
Con respecto a $\lnot A \lor \lnot \lnot A$, no es intuitionistically demostrable.
El contra-ejemplo con la semántica de Kripke es una estructura con tres nodos : $0,1,2$ tal que $0 \le 1$ $0 \le 2$ donde $A$ mantiene sólo en $1$ ($1 \Vdash A$).
Tenemos que $2 \Vdash \lnot A$, y desde allí, por la semántica de la cláusula : $k \Vdash \lnot A$ fib para todos los $k' \ge k : (k' \nVdash A)$ :
$0 \nVdash \lnot \lnot A$.
Pero desde $1 \Vdash A$, también se $0 \nVdash \lnot A$, y por lo tanto :
$0 \nVdash \lnot A \lor \lnot \lnot A$.
