comprensión lógica intuicionista

Question

Acaba de empezar un capítulo sobre Intuitionism, y ya estoy un poco confundido en cómo la estructura de una prueba en favor de intuitionistic lógica.

Y entonces hice un intento en los dos siguientes ejercicios de práctica:

1. $\neg X \lor ¬Y \implies \neg(X \land Y)$

Intento 1: Si tenemos una prueba de la premisa, entonces tenemos una prueba de $\neg X$ o una prueba de $\neg Y$. Supongamos ahora que se nos ha dado una prueba de $X$. De ello se desprende que nuestra primera prueba no podría haber sido una prueba de $\neg X$: por que sería una prueba de que $X$ no puede ser probado, y estamos suponiendo que nos han dado una prueba de $X$. Así que nuestra primera prueba deberá sido, en realidad, una prueba de $\neg X$ y el otro una prueba de las $\neg Y$.

2. $\cfrac{\neg\exists x\neg F x \quad \forall x(Fx \lor \neg F x)}{\forall x Fx}$

Intento 2: Supongamos que se nos ha dado una prueba de su premisa, entonces tenemos una prueba de que para algunos $n$, $\neg F n$ y para cada $n$, tenemos una prueba de $Fx$ o $\neg Fx$. Usando (9)(vi), se tiene una prueba de una sustitución, decir $\neg Fk$. La pregunta es si hay una operación que transforma cada prueba de para todos $x$, $F(x)$ en una prueba de $0 = 1$. No es: dada una prueba de la cuantificación universal, se aplican para generar una prueba de $Fk$; esto, junto con la prueba de $\neg Fk$, los rendimientos de una prueba de $0 = 1$.

Toda la ayuda es muy apreciada!

Answer 1

El BHK (Brouwer-Heyting-Kolmogorov) interpretación (describir) ve a declaraciones como las pruebas de esta afirmación. Así que la forma en que usted necesita a la razón es la siguiente: Si quiero mostrar que la de una declaración en la $X$ puedo concluir declaración de $Y$, entonces la necesidad de demostrar que si tengo una prueba de declaración de $X$ puedo describir de una prueba para la declaración de $Y$.

Vamos a empezar con un ejemplo sencillo. Quiero mostrar a $P\to P\lor Q$. Así que quiero demostrar que puedo encontrar una prueba de $P\to P\lor Q$. Por definición, tengo que venir para arriba con una operación que toma una prueba de $P$, y la transforma en una prueba de $P\lor Q$. Una prueba de $P\lor Q$ es una prueba de $P$ o una prueba de $Q$. Así que ¿qué sería de esa operación? En este caso es bastante simple, la operación no hace nada. Se necesita una prueba de $P$ y me da la espalda de la misma prueba. Ahora esta la prueba de $P$ es también una prueba de $P\lor Q$ (por la definición de la prueba de $P\lor Q$).

Ahora echemos un vistazo a las derivaciones que tiene usted en su pregunta. Asumiendo $\lnot X\lor\lnot Y$ quiero concluir $\lnot(X\land Y)$ (es decir, suponiendo que tengo una prueba de $\lnot X\lor\lnot Y$) para encontrar una prueba de $\lnot(X\land Y)$).

Así, en primer lugar pensar en qué es lo que usted necesita para llegar a: Una prueba para $\lnot(X\land Y)$ es, por definición, de la prueba de $X\land Y\to 0=1$ o (de nuevo, con la definición) una operación que toma una prueba de $X\land Y$ y da una prueba de $0=1$.

Ahora echemos un vistazo a lo que tenemos. Tenemos una prueba de $\lnot X\lor\lnot Y$, que es una prueba de $\lnot X$ o una prueba de $\lnot Y$.

Supongamos que tenemos una prueba de $\lnot X$. Esto significa que tenemos una operación $O_x$ que toma una prueba de $X$ y nos da una prueba de $0=1$. Podemos utilizar esta operación para producir una operación que toma una prueba de $X\land Y$ y se produce una prueba de $0=1$? Claro, una prueba de $X\land Y$ es una prueba de $X$ y una prueba de $Y$. Así que si tengo una prueba de $X$ y una prueba de $Y$ I puede utilizar la operación $O_x$ en la prueba de $X$ para encontrar una prueba de $0=1$. Lo que acabo de describir es una operación que toma una prueba de $X\land Y$ y da una prueba de $0=1$.

Así que ahora vamos a suponer que tenemos una prueba de $\lnot Y$. Usted puede venir para arriba con una operación que toma una prueba de $X\land Y$ y le da una prueba de $0=1$?

El segundo ejemplo debe ser similar:

Supongamos que tenemos una prueba de $\lnot\exists x\lnot Fx$ (¿qué significa eso? tratar de romper esta abajo) y una prueba de $\forall x(Fx\lor\lnot Fx)$ y necesitamos encontrar una prueba de $\forall x Fx$ (que es una operación que toma cada elemento $n$ y da una prueba de $Fn$.

Espero que esto le ayudará a entender un poco mejor el BHK interpretación. Si las cosas no están claras, hágamelo saber y voy a tratar de dar más detalles.