Ayuda para probar $ \sim \sim (p \to q),\sim \sim p \vdash \sim \sim q $ con axiomas intuicionistas

Question

Regla modus ponens: $ p, p \to q \vdash q $

Axiomas

A1 $ p \to (q \to p) $

A2 $ (p \to (q \to r)) \to ((p \to q) \to (p \to r)) $

A3 $ (p \land q) \to p $

A4 $ (p \land q) \to q $

A5 $ p \to (q \to (p \land q)) $

A6 $ p \to (p \lor q) $

A7 $ q \to (p \lor q) $

A8 $ (p \to r) \to ((q \to r) \to ((p \lor q) \to r)) $

A9 $ (p \to q) \to ((p \to \sim q) \to \sim p) $

A10 $ \sim p \to (p \to q) $

Regla que he derivado: $ p \to q, q \to r \vdash p \to r $

Metarregla derivada (teorema de deducción): $ \Gamma,p \vdash q $ implica $ \Gamma \vdash p \to q $

Teoremas que he demostrado

T1 $ p \to \sim \sim p $

T2 $ (p \to q) \to (\sim q \to \sim p) $

T3 $ p \to (\sim p \to q) $

T4 $ \sim \sim (\sim \sim p \to p) $

T5 $ \sim \sim \sim p \to \sim p $

Supongo que los axiomas 3,4,5,6,7 y 8 no son necesarios para la demostración. Por otro lado creo que A10 y T3 son críticos.

Gracias por cualquier ayuda al respecto.

Answer 1

Como tenemos el teorema de la deducción, el isomorfismo de Curry-Howard viene al rescate.

Negación intuitiva $\neg \phi$ es moralmente equivalente a $\phi\to\bot$ , donde $\bot$ es una contradicción. Y la doble negación corresponde vía Curry-Howard a la programación en estilo de paso de continuación . Así que si tenemos los supuestos $$ F: \neg\neg(p\to q) \qquad X:\neg\neg p $$ y quiere generar $\neg\neg q$ es natural tratar de escribir una transformación CPS de la aplicación $f\;x$ , lo que da $$ \lambda c. F\;(\lambda f. X\;(\lambda x. c(f\; x))) : \neg\neg q$$ El árbol de tipificación de esta expresión se puede desdoblar en una prueba utilizando el teorema de la deducción varias veces:

1. Supongamos que $\neg q$ (esto corresponde a $\lambda c$ ).

2. Supongamos que $p\to q$ (esto corresponde a $\lambda f$ ).

3. Supongamos que $p$ (esto corresponde a $\lambda x$ ).

4. Prueba $q$ (fácilmente por los supuestos 2 y 3 -- esto corresponde a la expresión $f\; x$ ).

5. Descargue el supuesto 3 para obtener $p\to q$ . También tenemos $p\to \neg q$ (a través de A1 y la hipótesis 1). A continuación, aplicamos A9 para concluir $\neg p$ .

   (Esto corresponde a $\lambda x.c(f\; x)$ de tipo $p\to\bot\equiv \neg p$ . Debido a que su sistema de prueba no tiene un explícito $\bot$ era necesario conseguir la contradicción $q$ , $\neg q$ del teorema de la deducción en dos partes, y la aplicación de $c$ a $f\;x$ se eleva para que ocurra "fuera de las lambdas". Una estrategia de prueba más amigable con C-H pero menos mínima habría sido probar $(x\to(y\land \neg y))\to\neg x$ como teorema general primero).

6. Descargue el supuesto 2 para obtener $(p\to q)\to \neg p$ . También tenemos $(p\to q)\to\neg\neg p$ desde $\neg\neg p$ se asume generalmente. Por lo tanto, A9 concluye $\neg(p\to q)$ .

   (Esto corresponde a $\lambda f.x\;(\lambda x.c(f\; x))$ de tipo $(p\to q)\to \bot\equiv \neg(p\to q)$ como en el paso anterior).

7. Por último, descargue la hipótesis 1 para obtener $\neg q\to\neg(p\to q)$ . También tenemos $\neg q\to\neg\neg(p\to q)$ desde $\neg\neg (p\to q)$ se asume generalmente. Por lo tanto, A9 concluye $\neg\neg q$ . Q.E.D.

Después de entretenernos un poco con esta construcción, debería quedar claro cómo podemos levantar sistemáticamente cualquier prueba de $\phi_1,\ldots,\phi_k\vdash \psi$ a una prueba de $\neg\neg\phi_1,\ldots,\neg\neg\phi_k\vdash\neg\neg\psi$ . Habrá $k+1$ invocaciones anidadas del teorema de la deducción, y la prueba original se inserta en lugar del paso (4) en el esquema anterior.

Answer 2

La derivación de unas 40 líneas me parece un poco más larga de lo necesario...

1) $\lnot \lnot (pq)$ --- premisa

2) $\lnot \lnot p$ --- premisa

3) $\vdash \lnot \lnot (pq) [\lnot q \rightarrow \lnot \lnot (pq)]$ --- Axioma 1

4) $\lnot q \rightarrow \lnot \lnot (pq)$ --- de 1) y 3) por modus ponens

5) $\vdash \lnot \lnot p [(p \rightarrow q) \rightarrow \lnot \lnot p]$ --- Axioma 1

6) $(p \rightarrow q) \rightarrow \lnot \lnot p$ --- de 2) y 5) por modus ponens

7) $\lnot q$ ---- asumido [a]

8) $pq$ --- asumido [b]

9) $\lnot q \rightarrow \lnot p$ --- de 8) por T2 y modus ponens

10) $\lnot p$ --- de 7) y 9) por modus ponens

11) $(p \rightarrow q) \rightarrow \lnot p$ --- de 8) y 10) por Deducción Th , descargando [b]

12) $\lnot (p \rightarrow q)$ --- de 11) y 6) y del axioma 9 por modus ponens dos veces

13) $\lnot q \rightarrow \lnot (p \rightarrow q)$ --- de 7) y 12) y Deducción Th , descargando [a]

14) $\lnot \lnot q$ --- de 4) y 13) y del axioma 9 por modus ponens dos veces.

Por lo tanto, forma 1), 2) y 14) :

$\lnot \lnot (pq), \lnot \lnot p \vdash \lnot \lnot q$ .

Answer 3

Intenta demostrar el muy útil metateorema: $\Gamma, p \vdash \sim q$ si $\Gamma, \sim\sim p \vdash \sim q$ .

Puede utilizarlo para convertir el fácilmente comprobado $ p \to q, p \vdash q $ en algo que pueda ser compuesto con su teorema T1 para conseguir su objetivo.

Answer 4

Usando T2 dos veces tenemos $ (p\to q) \to (\sim\sim p \to \sim\sim q)$ . Utiliza esto para "sí mismo" ( $p':=p\to q$ y $q':=(\sim\sim p\to \sim\sim q)$ obtenemos $$ \sim\sim(p\to q)\to\sim\sim(\sim\sim p\to \sim\sim q) $$ entonces usa algo como T4 para conseguir: $\sim\sim(p\to q) \to (\sim\sim p\to\sim\sim q)$ .

Answer 5

Gracias por todas las respuestas.

Me he centrado en el útil trabajo del Sr. Makholm. Aunque es cierto que no tengo acceso a $ \bot $ Me parece que sus pasos 3-5 no son necesarios:

Derive la regla A: $ \sim q \vdash (p \to q) \to \sim p $

1 $ \sim q $ hipótesis

2 $ p \to q $ hipótesis

3 $ \sim q \to (p \to \sim q) $ A1

4 $ p \to \sim q $ 1,3 modus ponens

5 $ (p \to q) \to ((p \to \sim q) \to \sim p) $ A9

6 $ (p \to q) \to ~p $ 2,5 modus ponens

7 $ \sim p $ 4,6 modus ponens

8 $ \sim q, p \to q \vdash \sim p $ 1-7

9 $ \sim q \vdash (p \to q) \to \sim p $ 8 teorema de la deducción

Derivar $ \sim \sim (p \to q),\sim \sim p \vdash \sim \sim q $

1 $ \sim \sim (p \to q) $ hipótesis

2 $ \sim \sim p $ hipótesis

3 $ \sim q $ hipótesis

4 $ \sim q \vdash \sim \sim (p \to q) $ 1

5 $ p \to q \vdash \sim \sim p $ 2

6 $ \sim q \to \sim \sim (p \to q) $ 4 teorema de la deducción

7 $ (p \to q) \to \sim \sim p $ 5 teorema de la deducción

8 $ (p \to q) \to \sim p $ 3 regla A

9 $ ((p \to q) \to \sim p) \to ((p \to q) \to \sim \sim p) \to \sim (p \to q)) $ A9

10 $ (p \to q) \to \sim \sim p) \to \sim (p \to q) $ 8,9 modus ponens

11 $ \sim (p \to q) $ 7,10 modus ponens

12 $ \sim q \vdash \sim (p \to q) $ 3-11

13 $ \sim q \to \sim (p \to q) $ 12 teorema de la deducción

14 $ ( \sim q \to \sim (p \to q)) \to (( \sim q \to \sim \sim (p \to q)) \to \sim \sim q) $ A9

15 $ ( \sim q \to \sim \sim (p \to q)) \to \sim \sim q $ 13,14 modus ponens

16 $ \sim \sim q $ 6,15 modus ponens

17 $ \sim \sim (p \to q),\sim \sim p \vdash \sim \sim q $ 1-16

Mis únicos puntos de incomodidad son los pasos 4 y 5 de mi segunda derivación (las "suposiciones generales" del Sr. Makholm en sus pasos 6 y 7). Suponen la metarregla $ \varnothing \vdash p $ implica $ \Gamma \vdash p $ . Sin embargo, supongo que esto debería ser bastante fácil de probar.

Creo que he encontrado una manera de evitar el uso de la meta regla $ \varnothing \vdash p $ implica $ \Gamma \vdash p $

Para obtener el paso 6 de mi segunda derivación sin utilizar el paso 4:

Prueba $ \sim q \to \sim \sim (p \to q) $

1 $ \sim \sim (p \to q) $ hipótesis

2 $ \sim \sim (p \to q) \to ( \sim (p \to q) \to q) $ A10

3 $ \sim (p \to q) \to q $ 1,2 modus ponens

4 $ (\sim (p \to q) \to q) \to ( \sim q \to \sim \sim (p \to q)) $ T2

5 $ \sim q \to \sim \sim (p \to q) $ 3,4 modus ponens

Para obtener el paso 7 de mi segunda derivación sin utilizar el paso 5:

Prueba $ (p \to q) \to \sim \sim p $

1 $ \sim \sim (p \to q) $ hipótesis

2 $ \sim \sim p $ hipótesis

3 $ p \to q $ hipótesis

4 $ \sim \sim p \to ( \sim p \to \sim (p \to q)) $ A10

5 $ \sim p \to \sim (p \to q) $ 2,4 modus ponens

6 $ (\sim p \to \sim (p \to q)) \to ( \sim \sim (p \to q) \to \sim \sim p) $ T2

7 $ \sim \sim (p \to q) \to \sim \sim p $ 5,6 modus ponens

8 $ \sim \sim p $ 1,7 modus ponens

9 $ p \to q \vdash \sim \sim p $ 3-8

10 $ (p \to q) \to \sim \sim p $ 9 teorema de la deducción