¿Qué "metateoría" utilizaron los primeros investigadores de teoría / lógica de conjuntos para probar resultados semánticos?

Question

Cosas como la de primer orden teorema de completitud y la Löwenheim-Skolem teorema se consideran fundamentales en la lógica matemática.

El enfoque moderno parece ser, por lo general, para interpretar un "modelo" específicamente como un conjunto en algunos otros (normalmente de primer orden) "conjunto de metatheory." Así que cuando hablamos de un modelo de PA, por ejemplo, que por lo general significa que estamos formalizando como una subteoría de algo como de primer orden de ZFC. Modelos de ZFC puede ser formalizado en el conjunto más fuerte de las teorías, tales como los que se obtienen mediante la adición de grandes cardenales, etc.

Pero cuando Gödel demostró que un primer orden de la frase tiene un número finito de prueba, si y sólo si se mantiene en cada "modelo" -- ¿en qué estaba hablando? Del mismo modo, ¿cómo podemos entender la Löwenheim-Skolem teorema de si los modelos no existían en el momento?

Es claro que estos investigadores no estaban hablando sobre el uso de primer orden ZFC como un metatheory, como la teoría ni siquiera ganar popularidad hasta después de Cohen trabajo en forzar en los años 60. Del mismo modo, la teoría de conjuntos NBG todavía no se había formalizado. Y, sin embargo, que, obviamente, estaban hablando acerca de algo. Tenían una idea diferente de la semántica que el moderno conjunto teórico uno?

En el cierre, dos preguntas:

1. En general, ¿cómo hicieron los primeros investigadores (digamos pre-Cohen) formalizar semántica de conceptos como estas?
2. Tiene cualquiera de estas obras originales sido traducido al inglés, sólo para ver directamente en su forma de tratar la semántica?

Answer 1

No sé la historia lo suficientemente bien como para una respuesta completa, pero aquí es una respuesta parcial, en los aspectos matemáticos. Cuando usted escribe:

Es claro que estos investigadores no estaban hablando sobre el uso de primer orden ZFC como un metatheory [...] Y, sin embargo, que, obviamente, estaban hablando acerca de algo. Tenían una idea diferente de la semántica que el moderno conjunto teórico uno?

y

El enfoque moderno parece ser, por lo general, para interpretar un "modelo" específicamente como un conjunto en algunos otros (normalmente de primer orden) "conjunto de metatheory."

usted parece estar siguiendo un poco el concepto erróneo común: que no se puede hacer basado en la semántica sin tener un poco de teoría de conjuntos en la mente como un metatheory.

Pero este no es el caso! La definición fundamental de un (Tarskian) el modelo es sólo como un conjunto con cierta extra estructura, como un grupo, o un anillo, o similar. No "un conjunto de ZFC", o "un conjunto de NBG", pero sólo un conjunto, a la que nos podemos razonar sobre el uso de cualquiera de las técnicas y principios que utilizamos para el razonamiento matemático en general.

Por supuesto, en ese razonamiento, probablemente vamos a seguir algunos de los principios establecidos, como aquellos que son justificados por ZFC o NBG o algunos otros específicos de la teoría. (Históricamente, tales fundacional teorías se desarrollaron exactamente para intentar codificar/justificar los principios generalmente utilizadas y aceptadas.) Y los lógicos son, por una variedad de razones, es más probable que otros matemáticos para ser explícito acerca de lo que los principios que se siguen en una determinada pieza de trabajo. Pero fundamentalmente, no necesita de un conjunto explícito de la teoría de la metatheory a estudio basado en la semántica, más de lo que necesita el estudio de los grupos o de los anillos o las superficies de Riemann.

Como ya he dicho, yo no soy especialmente bien leer históricamente, pero a partir de los papeles que he leído de ese periodo, mi impresión es principalmente que la mayoría de los investigadores en el período fueron el uso de la moderna (Tarskian) noción de la semántica, y que algunos autores escribió explícitamente sobre qué tipo de metatheory que estaban usando, mientras que otros no. Pero la falta de una explícita metatheory no es cualquier falta de rigor o la claridad en su noción de modelos - es normal que la práctica de matemáticas, sin duda, el momento y al menos posiblemente de hoy.

Answer 2

Pedro LeFanu Lumsdaine correctamente comentó que no es necesario especificar un conjunto preciso de la teoría de la metatheory con el fin de demostrar algo como el teorema de completitud. Esta observación se confirma si observamos, por ejemplo, Gödel los documentos originales.

Gödel obras completas han sido publicados por Oxford University Press, y traducciones de inglés están incluidos. En cuanto a la integridad teorema, que fue publicado por primera vez en "Über die Vollständigkeit des Loikkalküls," él hace las siguientes observaciones:

En conclusión, permítanme hacer una observación sobre el medio de prueba utilizado en lo que sigue. En cuanto a ellos, sin restricción alguna se ha hecho. En particular, el uso fundamental es el hecho de que el principio del medio excluido para las colecciones infinitas (la nondenumerable infinito, sin embargo, no se utiliza en la principal prueba).

Se entra entonces en una bastante extendida defensa de su decisión de utilizar la ley del medio excluido en su prueba. Nota en particular de que él no da una definición cuidadosa de los "metatheory", en el que está trabajando.

En su famoso 1931 papel en el teorema de la incompletitud, Gödel comienza mencionando tanto Principia Mathematica (PM) y de Zermelo–Fraenkel de la teoría de conjuntos, pero pronto se estrecha en su enfoque de la tarde. Él menciona que todos los sintácticas de los conceptos que él utiliza en su prueba se pueden expresar en el sistema de PM, pero no insistir sobre este punto. Después de que el principal argumento, señala que la prueba es intuitionistically válido. Nuevamente, no hay una descripción precisa de la "metatheory", en el que está trabajando.

Answer 3

Para abordar la cuestión principal acerca de Gödel original de la prueba del teorema de completitud, que como Timoteo Chow explica se puede encontrar en Gödel Obras completas, que es el uso de la noción de "Erfüllungssystem", que significa algo así como "satisfactorio del sistema". Es una estructura destinada a satisfacer una fórmula $\phi$ que no es rebatible (es decir, tal que $\neg \phi$ no es demostrable), cuyo conjunto subyacente es que los números naturales. Luego extiende su teorema para contables teorías demostrar el teorema de compacidad.

La estructura está construida como lo que hoy llamaríamos un filtrado colimit de una contables de la cadena de finito de estructuras. Esto se hace mediante el uso de König del lexema, por primera construcción de un finitely de ramificación del árbol finito de estructuras con la propiedad de que las hay las estructuras en cualquier nivel finito y de la satisfacción de una determinada estructura en el nivel $n$ restringe a la satisfacción en el inmediato predecesor. Entonces hay una cofinal rama a través de la cual se construye el modelo de $\phi$ sobre la estructura dada por los números naturales.

Vale la pena mencionar que, como consecuencia inmediata de su prueba se obtiene la tendencia a la baja Löwenheim-Skolem teorema, ya que él construye un modelo sobre la estructura cuyo conjunto subyacente es que los números naturales para cualquier contables conjunto de válido fórmulas. Löwenheim original de la "prueba" de que en realidad había algunos defectos que, más tarde Skolem fijo.

Answer 4

Como Andreas Blass señalado, la meta-teoría puede ser ordinaria de matemáticas, al menos en teoría. En la práctica, sin una explícita meta-teoría, las figuras de autoridad de decidir lo que está permitido y lo que no. Tarski (como Cantor antes de él) aprendió esta lección de la manera difícil, como se puede leer en las cuentas de Tarski del teorema acerca de la elección de 1924:

... cuando trató de publicar el teorema de Comptes Rendus de l'Académie des Sciences de París, Fréchet y Lebesgue se negó a hacerlo. Fréchet escribió que una implicación entre dos conocidos proposiciones no es un nuevo resultado. Lebesgue escribió que una implicación entre dos falsas las proposiciones es de ningún interés.

No es de extrañar que la moderna noción de modelo y meta-teoría son debido a Tarski (y su colega Robert Vaught) a partir de 1956. Pero Tarksi ya presentó un "no moderno" noción de meta-teoría en 1933, ver la SEP entrada en la Verdad de Tarski Definiciones.

La cuestión es un poco más complejo, pero aquí está mi propio resumen de la diferencia entre estas dos nociones para empezar:

Si he entendido correctamente, para la versión de 1933, el modelo (es decir, la estructura algebraica sobre el que hablamos) es parte de la meta-lenguaje y que no se mencionan por separado. La asignación de objetos para las variables en el otro lado es lo que puede satisfacer una determinada fórmula. Una fórmula es (definido) verdadera si es satisfecha por todas las posibles asignaciones de objetos para las variables.

La versión 1956 es tratada de manera menos explícita en los enlaces de SEP de entrada, pero se insinúa que el modelo ya no es una parte implícita de la meta-lenguaje, sino un objeto explícito de la teoría. Un modelo puede satisfacer una fórmula (o frase), de forma similar a una "asignación de objetos para las variables" podría satisfacer una determinada fórmula para la versión de 1933. Pero el texto también sugiere que la de 1956, se basa ahora más fuerte en un conjunto subyacente-la teoría, mientras que la de 1933 explícitamente tratado de minimizar "el conjunto teórico de los requisitos de la definición de la verdad".