¿Lowenheim-Skolem intuicionista?

Question

¿Existe una versión del teorema de Löwenheim-Skolem en lógica intuicionista? Estoy especialmente interesado en la forma "descendente". La prueba estándar que conozco utiliza la prueba de Tarski-Vaught para las subestructuras elementales, que a su vez se basa en el hecho de que "forall" es equivalente a "not exists not", y eso falla intuitivamente.

Answer 1

Tengo una referencia que dice que el teorema de Löwenheim-Skolem hacia abajo no se da en la lógica intuicionista. En palabras del resumen "incluso una versión muy potente versión de la teoría de conjuntos intuicionista no da ninguna de las formas habituales de un teorema de Löwenheim-Skolem hacia abajo".

La paradoja de Skolem y el constructivismo Revista de Lógica Filosófica Springer Países Bajos Edición Volumen 16, Número 2 / Mayo, 1987

http://www.springerlink.com/content/t28583t748301t04/

También página 341 de A Companion to Metaphysics Por Jaegwon Kim

"...no hay un análogo intuitivamente aceptable del clásico teorema descendente de Löwenheim-Skolem"

Answer 2

¿La pregunta es sobre el teorema de Löwenheim-Skolem para modelos clásicos en la metateoría intuicionista, o sobre el teorema de Löwenheim-Skolem para modelos intuicionistas (Kripke) en la metateoría clásica? Este último ciertamente es válido. Se puede demostrar fácilmente si se comprueba que un modelo de Kripke puede representarse mediante un modelo clásico adecuado de dos órdenes, de manera que la satisfacción de cualquier fórmula intuicionista en el modelo original sea definible de primer orden en la representación, y aplicando luego el teorema clásico de Löwenheim-Skolem.

Answer 3

Hace tiempo, pero creo que Ebbinghaus, Flum y Thomas, en el libro Mathematical Logic, obtienen los teoremas de Löwenheim-Skolem como un subproducto del teorema de completitud, que demuestran utilizando la construcción de Henkin. Y creo que eso es plenamente constructivista.