El principio de la "si $a$ no es una cota superior para $E$, entonces no es un elemento de $E$ que es mayor que $a$" se expresa formalmente como
$$
\lnot [ (\forall x \in E) ( x < a \lor de x = a) ] \(\exists x \in E)(a < x).
$$
Este principio no es demostrable en el estándar de sistema formal llamado "intuitionistic de primer orden de la lī ogica de" que voy a llamar a IFOL. De hecho, incluso los más débiles de la fórmula
$$
(1) \quad \lnot [ ( \forall x) ( x < a \lor de x = a)] \(\exists x)(a < x)
$$
no es demostrable en IFOL de los axiomas de un orden lineal (reflexividad, antisymmetry, y la transitividad de la $<$). Me quiero centrar en el que los más débiles principio (1), porque evita las distracciones innecesarias con conjuntos. Por lo tanto, trabajar en una teoría que tiene sólo un tipo de objeto, y sólo dos relaciones binarias: de la igualdad y de un orden lineal $<$.
Mi reclamo es que (1) no es demostrable en IFOL de los axiomas de un lineal de pedidos. La manera de probar esto, como era de esperar, es para producir un contramodelo. Pero esto no debe ser necesariamente un no clásica contramodelo, porque el principio (1) es demostrable a partir de los axiomas de un orden lineal en la lógica clásica. Antes de describir formal contramodelo, permítanme describir la intuición detrás de él.
La intuición
La intuición de por qué principio (1) no es demostrable en IFOL está relacionado con la diferente relación entre los cuantificadores universal y existencial en la lógica constructiva. También se refiere a una intuición en la lógica constructiva que "más elementos pueden aparecer en cualquier momento". En la lógica clásica, tratamos $\forall$ $\exists$ como doble el uno al otro. En sistemas constructivos, a menudo es mejor para ver los $\forall$ como hacer una promesa y $\exists$ como la producción de un testigo:
$(\forall x)[x < a \lor x = a]$ puede ser visto como una promesa de que, cuando nos encontramos con otro elemento $x$, será igual a $a$ o menos de $a$.
$(\exists x)[a < x]$ afirma que ya tenemos un testimonio específico $x_0$$a < x_0$.
Imagina que yo soy la construcción de un modelo, la adición de elementos de uno en un tiempo, y todavía no he hecho mi mente si quiero $a$ a ser un límite superior. Podemos ver $\lnot (\forall x)[x = a \lor x < a]$ como diciendo que, si bien $a$ podría ser una cota superior para los elementos ya he agregado, no estoy dispuesto a prometer que $a$ será una cota superior para todos los elementos que puede añadir más tarde. Quizás $a$ va a terminar como un límite superior, tal vez no. Pero $(\exists x)[a < x]$ significa que ya he elegido un elemento a ser menos de $a$.
Sin duda, puedo reserva el derecho de añadir un elemento mayor que $a$, sin añadir ese elemento en el momento actual: la formalización de esta situación da un modelo en el principio de que (1) no.
Formal contramodelo
Un tipo de no clásica modelo se llama un marco de Kripke; estos se describen brevemente en la universidad de Stanford artículo de la Enciclopedia sobre intuitionistic lógica. Es importante recordar que "intuitionistic lógica" aquí significa el particular formal deductivo sistema IFOL.
Ahora, suponiendo que alguna familiaridad con marcos de Kripke: el deseado de Kripke marco tiene solo dos nodos, $p$$p'$. En el nodo $p$ tenemos el lineal de pedidos con un solo elemento $a$. En el nodo $p'$ tenemos el lineal del orden de dos elementos $a,b$$a < b$. Nodo $p$ no obliga a que $a$ es un límite superior, en el hecho de $p$ fuerzas de $\lnot [ (\forall x)(x < a \lor x = a)]$. Pero $p$ no obliga a ningún testigo de $(\exists x)[a < x]$. Así nodo $p$ no la fuerza de la fórmula (1). Debido a que una fórmula es comprobable en IFOL si y sólo si es forzado por cada nodo de cada marco de Kripke, el principio (1) no es demostrable en intuitionistic lógica.
Respuestas a las restantes partes de la pregunta
El opuesto de (1) es demostrable en IFOL.
Una manera de debilitar a (1) es el uso de una traducción que se asigna comprobable fórmula clásica de la lógica de primer orden para clásicamente equivalente fórmulas demostrables en IFOL. La doble negación traducciones hacer esto, por ejemplo. Estos complementos adicionales suficientes doble negación a la fórmula para hacer intuitionistically demostrable, mientras que la preservación de la clásica de equivalencia.
