Lo práctico de las pruebas de trabajo en intuitionistic pero no un mínimo de lógica?

Question

Intuitionistic lógica contiene la regla de $\bot \rightarrow \phi$ por cada $\phi$. En las formulaciones que he visto este es un axioma, y la lógica sin este axioma(?) se denomina "un mínimo de lógica".

Es esta regla requiere para la prueba práctica de problemas en intuitionism? Es un buen ejemplo de una práctica de la prueba que va a través intuitionism que no lo atraviesa sin este axioma, o hacer todos/la mayoría de los importantes resultados prácticos también ir a través de un mínimo de lógica? Y por favor puede ilustrar esto con un ejemplo práctico?

Contexto: Estamos ante un problema de la teoría de la decisión en los que podría ser muy útil disponer de un potente razonamiento lógica que puede, no obstante, la notificación y el filtro consecuencias que pasa a través de un principio de explosión. Así que si la prueba usar una regla como $(A \vee B), \neg A \vdash B$ y podemos reemplazar con $(A \vee B), \neg A \vdash \neg \neg B$ a distinguir las pruebas a las que va a través de la 'explosiva' razonamiento, que también sería útil.

AÑADIDO una aclaración: yo no estoy buscando un genérico fórmula proposicional que no puede ser probado, estoy buscando un teorema de la topología o la teoría de la computabilidad o algo que puede ser probada en intuitionism pero no en un mínimo de lógica, junto con un relieve que paso requiere de la explosión. Podría ser una muy simple teorema pero yo todavía quieren ser útiles declaración en algunos dominio concreto.

Answer 1

En un mínimo de lógica no se puede probar una fórmula de la forma $\forall x \;\neg A(x) \rightarrow B(x)$ donde $B(x)$ no ha $\bot$ como subformula, a menos que ya se puede probar $\forall x\;B(x)$. Para ver esto, observe que si podemos probar $\forall x\;(A(x) \rightarrow \bot) \rightarrow B(x)$ en un mínimo de lógica, entonces, podríamos probar la misma fórmula con $\bot$ reemplazado por $\top$ es decir $\forall x\;(A'(x) \rightarrow \top) \rightarrow B(x)$ (donde $A'$ tiene todas las instancias de $\bot$ $A$ reemplazado por $\top$). Desde $\forall x \;A'(x) \rightarrow \top$ es comprobable, podemos deducir que $\forall x\;B(x)$ también es demostrable.

Para dar un ejemplo claro, se puede probar fácilmente que en intuitionisitic la lógica de que si un número natural $n$ no es primo, entonces no se $a, b$ tal que $1 < a, b < n$$n = ab$. Pero esto no funciona en un mínimo de lógica.

Creo que la parte fundamental de la prueba de que funciona para intuitionistic lógica, pero no un mínimo de lógica es la siguiente principio. Sobre la base de este principio no debería ser sorprendente que en el ejemplo anterior se sostiene en intuitionistic lógica. Si $\phi$ es un cuantificador de fórmula libre, entonces podemos probar $$ \neg(\forall x < y \;\neg\phi(x)) \rightarrow \exists x < y\; \phi(x) $$ (Esta es una versión limitada del clásico principio de $\neg \forall x \neg \phi \rightarrow \exists x \phi$).

Podemos demostrar esto por inducción en $y$. Tenga en cuenta que si tenemos ex falso, entonces el caso $y = 0$ es fácil. Supongamos ahora que hemos demostrado que esto de $y$ y quieres mostrarlo para $y + 1$. Supongamos, además,$\neg(\forall x < y + 1\; \neg \phi(x))$. Desde $\phi(x)$ es cuantificador libre, sabemos que cualquiera de las $\phi(y)$ o $\neg \phi(y)$ sostiene (por otro argumento inductivo). Supongamos que $\phi(y)$ mantiene. Entonces podemos trivialmente espectáculo $\exists x < y + 1\;\phi(x)$. Ahora supongamos que $\neg \phi(y)$ mantiene. Tenga en cuenta que nosotros no podemos tener $\forall x < y\; \neg \phi(x)$ porque esto implicaría $\forall x < y + 1 \; \neg \phi(x)$ (debido a que para cada $x < y + 1$ $x = y$ o $x < y$ por otro inductivo argumento!). Por lo tanto $\neg (\forall x < y \; \neg\phi(x))$ mantiene y, entonces, por la hipótesis inductiva podemos mostrar a $\exists x < y\; \phi(x)$, y deducir $\exists x < y + 1\;\phi(x)$.

Así que ex falso se utiliza explícitamente para el caso de $y = 0$. Sospecho que también es importante para el argumento inductivo que por cada $x < y + 1$ $x = y$ o $x < y$ que no se ha presentado.

Answer 2

la disyuntiva Silogismo $( (A \vee B), \neg A \vdash B )$ es sobre la más importante de la deducción que es válido en (Heytings) intuitionistic lógica pero no en (Johanssons) un mínimo de lógica. Johanssons artículo (ver el enlace en http://en.wikipedia.org/wiki/Minimal_logic ) también menciona la siguiente fórmula de la que son teoremas en intuitionistic lógica, pero NO son teoremas en un mínimo de lógica.

$ ( A \land \lnot A) \to B $

$ ( ( A \land \lnot A) \lor B ) \to B $

$ ( B \lor B) \to( \lnot \lnot B \to B ) $

$ ( \lnot A \lor B) \to ( A \to B) $

$ ( A \lor B) \to ( \lnot A \to B ) $

$ ( A \to ( B \lor\lnot C) \to ((A \land C) \to B)) $

$ \lnot \lnot ( \lnot \lnot A \to A) $

Pero tal vez Johansson sólo menciona a estos porque son los que se mencionan en Heyting del artículo.

Estoy doubtfull si $ ( A \lor B) , \lnot A \vdash \lnot \lnot B $ es un teorema de un mínimo de lógica , han demostrado que o acaba de asumir?
[CORRECCIÓN de $ ( A \lor B) , \lnot A \vdash \lnot \lnot B $ es un teorema de un mínimo de lógica, porque $ ( A \land \lnot A) \to \lnot \lnot B $ $ B \to \lnot \lnot B $ son ambos teoremas de un mínimo de lógica]

En la década de 1920 hubo discusiones sobre lo que los axiomas de la lógica constructiva se, es solo que el fundador de intuitionism (Brouwer) le gustaba Heyting y sólo le dio el honor de ser el nombre de su sistema EL sistema de intuitionistic lógica, Brouwer encontrar la lógica sin derramamiento de sangre, y realmente no es importante)

Lo que yo creo que es un problema más serio es que $ ( A \land \lnot A) \to \lnot B $ es un teorema de un mínimo de lógica. así se podría concluir que mnimal lógica todavía permite una gran explosión. Creo que sería mejor mediante el uso de un paraconstistent o relevantes de la lógica. ver:

http://en.wikipedia.org/wiki/Paraconsistent_logic
y
http://en.wikipedia.org/wiki/Relevance_logic

Buena suerte