Modelo simple de lógica intuicionista (proposicional) para reconocer fórmulas válidas

Question

Me di cuenta de que cuando quiero saber (o más bien de ver/entender) si algunos de los clásicos de la tautología es válido intuitionistically, la primera vez que intente reemplazar cada variable proposicional por una unión finita de abiertos intervalos en la recta real $\mathbb R$, y a ver si puedo construir un contraejemplo de esta manera. Empecé a creer que este método siempre funciona, y se encontró lo siguiente en la wikipedia:

Se puede demostrar que reconocer fórmulas válidas, es suficiente para considerar una sola álgebra de Heyting cuyos elementos son los subconjuntos abiertos de la línea real $\mathbb R$.

La referencia de esta declaración es "Conferencias sobre el Curry-Howard Isomorfismo" por M. P. Sørensen y Urzyczyn, que contiene el siguiente teorema:

1. Una fórmula $\varphi$ de la longitud de la $n$ es válido iff es válido en todas las álgebras de Heyting de cardinalidad en la mayoría de las $2^{2^n}$;
2. Deje $\mathcal H$ ser el álgebra de todos los subconjuntos de un denso en sí mismo espacio métrico $V$ (por ejemplo, el álgebra de todos los subconjuntos de a $\mathbb R^2$). A continuación, $\mathcal H \vDash \varphi$ fib $\varphi$ es válido.

Este teorema no es suficiente para demostrar que mi enfoque siempre va a funcionar, porque podría ser necesario considerar también la posibilidad de abrir conjuntos como el complemento del conjunto de Cantor, o al menos de los complementos de contable de conjuntos cerrados con interesantes límite de puntos.

Pero si mi enfoque siempre funciona, entonces ya el álgebra $\mathcal H'$ de todas las uniones de intervalos abiertos con el entero de los puntos finales de $\mathbb R$ debe satisfacer "$\mathcal H' \vDash \varphi$ fib $\varphi$ es válido". ¿Es esto cierto? Si no, ¿qué es un simple contraejemplo?

Answer 1

Por desgracia, su enfoque no siempre funciona. La fórmula $$\lnot\lnot p \lor (\lnot\lnot p\rightarrow p)$$ is true whenever $p$ is a finite union of open intervals in $\mathbb{R}$, pero no es intuitionistically válido.

Deje $T$ ser finito, de la unión de intervalos abiertos. Vamos a llamar a $T$ la de la tierra y $\lnot T$ (el interior del complemento de $T$) el mar. Cualquier punto de $\mathbb{R}$ que no está en la tierra o en el mar es un punto límite de $T$. Digamos que un límite de punto de $x$ es un lago si $x$ es aislado en el complemento de $T$, e $x$ es una playa si no. Por ejemplo, si $T = (a,b)\cup (b,c)$, $a$ $c$ son las playas y $b$ es un lago. Deje $L$ el conjunto de los lagos. Desde $T$ es una unión finita de intervalos, $L$ es finita conjunto discreto.

A continuación, $\lnot\lnot T$ es el interior del complemento de la mar. Este contiene la tierra y los lagos, pero no las playas, por lo $\lnot\lnot T = T\cup L$.

Ahora $(\lnot\lnot T \rightarrow T)$ es el mayor conjunto abierto con la propiedad de que su intersección con la a $T\cup L$ está contenido en $T$. En otras palabras, todos los puntos que tienen un barrio que no contengan ninguno de los lagos. Desde los lagos forman un conjunto discreto, $(\lnot\lnot T \rightarrow T) = \mathbb{R}\setminus L$.

Por lo tanto $\lnot\lnot T \lor (\lnot\lnot T\rightarrow T) = (T\cup L)\cup (\mathbb{R}\setminus L) = \mathbb{R}$.

He encontrado este ejemplo buscando el primer lugar donde la libre álgebra de Heyting en un generador se contrae cuando el generador está asignado a un genérico finito de la unión de intervalos.

El argumento anterior también pasa a través de al $L$ no tiene límite de puntos fuera de $L$ (que no la uso que es finito). Así que esta fórmula también es válida en el álgebra $\mathcal{H}'$ (no necesariamente finita) uniones de intervalos abiertos con el entero de los puntos finales.

Para llegar a un subconjunto abierto de $\mathbb{R}$ que no cumpla con esta fórmula, sólo necesitamos los lagos para tener un punto límite que es una playa (un límite de lagos no pueden estar en la tierra o en el mar). Así que vamos a $U = \bigcup_{n\in\mathbb{N}_+} (\frac{1}{n+1},\frac{1}{n})$. Tenemos $\lnot\lnot U = (0,1)$$(\lnot\lnot U \rightarrow U) = \mathbb{R}\setminus (\{0\}\cup \{\frac{1}{n}\mid n\in\mathbb{N}_+\})$, lo $0\notin \lnot\lnot U \lor (\lnot\lnot U \rightarrow U)$.