¿Qué es un constructiva prueba de $\lnot\lnot(P\vee\lnot P)$?

Question

El teorema de Glivenko dice que $\lnot\lnot P$ es un teorema de intuitionistic lógica siempre $P$ es un teorema de la lógica clásica. Está estrechamente relacionado con el llamado Gödel–Gentzen negativo en conversión de las que se incorpora la lógica clásica en intuitionistic lógica.

Desde $P\vee\lnot P$ es un conocido teorema de la lógica clásica, espero que por el teorema de Glivenko, $\lnot\lnot(P\vee\lnot P)$ es comprobable en intuitionistic lógica. Pero no puedo encontrar una prueba! Me debe estar pasando por alto algo obvio.

Si $\lnot\lnot(P\vee\lnot P)$ es de hecho comprobable en la IL, me gustaría ver una deducción natural o sequent cálculo prueba de ello, o, especialmente, la construcción de un tipo de $\lambda$-cálculo plazo con el tipo de $((P\vee(P\to \bot))\to\bot)\to\bot$.

Si es que no es demostrable en IL, lo he entendido mal?

Anexo: yo verificarse de la proposición con el modelo habitual, dejando $P$ ser un subconjunto de a $\mathbb R$, y la interpretación de $\vee$ como el conjunto de la unión y $\lnot x$ como el interior del complemento de $x$, y la proposición $\lnot\lnot(P\vee\lnot P)$ hizo parecen salir como todos los de $\mathbb R$ para cualquier elección de $P$, así que si he cometido un error aquí también me gustaría saber a qué subconjunto de $\mathbb R$ es el contraejemplo.

Answer 1

Por el BHK interpetation, una prueba de $(P \lor (P \to \bot)) \to \bot$ es una pareja de procedimientos, uno para cada tensión dialéctica en la hipótesis.

• La primera, $s_1$, es un procedimiento que toma una prueba de $P$ como entrada y produce una prueba de $\bot$. En otras palabras, la primera es una prueba de $P \to \bot$.

• La segunda, $s_2$, lleva a ninguna prueba de $P \to \bot$ como entrada y produce una prueba de $\bot$. En otras palabras, se trata de una prueba de $(P \to \bot) \to \bot$.

Mediante la composición de estos para formar $s_2(s_1)$, obtenemos un procedimiento que se lleva a ninguna de entrada y produce una prueba de $\bot$.

El procedimiento que acabamos de describir (composición) toma cualquier prueba de $(P \lor (P \to \bot)) \to \bot$ y se produce una prueba de $\bot$. Esto significa que $((P \lor (P \to \bot))\to \bot) \to \bot$ es demostrable.

Esta descripción muestra cómo escribir un $\lambda$ expresión del tipo apropiado. Todo lo que hace es romper la entrada en sus dos componentes y ejecutar la segunda con la primera entrada. En particular, si consideramos la $(P \lor \lnot P) \to \bot$ como un tipo de $p(n,s)$ tal que $\lambda s.p(1,s)$ es de tipo $P \to \bot$ $\lambda\,s.p(2,s)$ es de tipo $\lnot P \to \bot$ $$\lambda\, p(n,s) . p(2,\lambda\, s.p(1,s))$$ is of type $((P \lor \lnot P) \a \bot) \a \bot$

Answer 2

Aquí está una deducción natural de la prueba:

1. $\lnot (P \lor \lnot P)$ [Asunción]
2. $\lnot P \land \lnot \lnot P$ [De Morgan]
3. $\lnot P$ [$\land$ eliminación]
4. $\lnot \lnot P$ [$\land$ eliminación]
5. $\bot$ [$\bot$ introducción a partir de 3., 4.]
6. $\lnot \lnot (P \lor \lnot P)$ [$\lnot$ introducción]

Answer 3

Aunque ya he aceptado Carl Mummert la respuesta, que era justo lo que yo quería, me voy a anexar las siguientes variaciones para referencia en el futuro.

En primer lugar, una prueba:

1: Suponga $((a\vee(a\to\bot))\to\bot$
2a: Suponga $a$
2b: $a\vee(a\to\bot)$ [2a, derecho $\vee$]
2c: $\bot$ [1, 2b, mp]
3: $a\to\bot$ [2a–2c]
4: $a\vee(a\to\bot)$ [3, a la izquierda $\vee$]
5: $\bot$ [1, 4, mp]
6: $(((a\vee(a\to\bot))\to\bot)\to\bot$ [1-5]

Y un programa con el requisito de tipo:

λf.
  let g = λa. f (Left a)
  let h = λn. f (Right n)
in
  h g

a tipo $a$,
n y g tipo $a\to\bot$,
f tipo $(((a\vee(a\to\bot))\to\bot)$, y
h tipo $((a\to\bot)\to\bot)$.

Por último, el plazo de Haskell

\f -> let   
        g = \a -> f (Left a)
        h = \n -> f (Right n)
        in h g

es aceptado por GHC y el tipo de (Either a (a -> t) -> t) -> t.
Podemos β-reducir este plazo a

\f -> f (Right ( \a -> f (Left a) ))

que tiene el mismo tipo.

Answer 4

Aquí está el argumento intuitivo: Para demostrar $\lnot \lnot (P \lor \lnot P)$, suponga $\lnot (P \lor \lnot P)$ y derivar una contradicción. Ahora suponga $P$. Por lo $P \lor \lnot P$ por regla $\lor$-intro, una contradicción. Por lo tanto,$\lnot P$. Ahora $P \lor \lnot P$ $\lor$- intro, de nuevo una contradicción. Por lo tanto,$\lnot \lnot (P \lor \lnot P)$.

Lo fascinante es que la analógica para la lī ogica de falla:

$$ \lnot \lnot (\forall x)(a(x) \lor \lnot Una(x)) $$ es underivable en intuitionistic lógica!

Answer 5

El demostrador en línea http://tassi.web.cs.unibo.it/logic/ debe ayudar a entender la intuitionistic prueba en el secuente cálculo (G3ip) por $\neg \neg (\neg P \lor P)$. De hecho, esta fórmula es comprobable mínima lógica es decir, un subsistema de intuitionistic lógica. Tenga en cuenta que la prueba a continuación (producido por el armario para G3ip que acabo de mencionar) en realidad no se utiliza el intuitionistic absurdo de la regla de $L\bot$ a pesar de que el uso de esta etiqueta por el armario de: es evidente que el axioma $P , \bot \Rightarrow \bot$ es el axioma de identidad y no la expresión de la famosa Ex Falso Quodlibet en el secuente cálculo. Aquí está la imagen png de la prueba:

Ahora la siguiente prueba en G4ip (es decir, Dyckhoff de la LJT) es más corto:

Aquí están ahora las pruebas en la deducción natural.

En Fitch estilo:

y en Gentzen estilo:

Vemos en este ejemplo que la repetición de la asunción (1) es inevitable. (Es por eso que no está claro, en mi opinión, ¿por qué Gentzen estilo en deducción natural siempre debe ser preferido por los teóricos de la prueba.)

Los mejores deseos,

Jo.