Cómo gran parte de la actual lógica es acerca de la sintaxis?

Question

La lógica básica del curso en la escuela da la impresión de que la lógica de la sintaxis y la semántica de los aspectos. Recientemente, me pregunto si la sintaxis parte todavía juega un papel esencial en los estudios actuales. A continuación están algunas de mis observaciones, espero que la idea de la comunidad pueden hacerlas más completas.

Modelo de la teoría: a pesar de que el modelo de la teoría se expresa en el lenguaje de la lógica, se puede ver como el estudio de local isomorfismo (ver Poizat del "curso de formación en el Modelo de la Teoría"). La sintaxis parte es por lo tanto natural (aunque puede ser incómodo para algunos) manera de ver la teoría, más que una necesidad.

La teoría de la recursividad: El objeto de estudio es la noción de computabilidad en un contexto diferente. Si creemos en la Tesis de Church-Turing, entonces estos concepto son independientes de la formalismo elegido.

Teoría de conjuntos: La íntima relación entre el gran cardenal y determinación tal vez puede sugerir que este es un fenómeno universal. Será este fenómeno desaparecer si queremos cambiar el idioma de las matemáticas, por ejemplo, la categoría de la teoría?

Prueba de teoría: yo sé muy poco para decir nada.

Si la observación es cierto, es que se justifica la demanda que Turing grados, y los grandes cardenales reciben la misma matemática de estado como, por ejemplo, los números primos?

Answer 1

No sabemos cómo abstracto, lejos de la sintaxis en la prueba de la teoría. Si decimos que hay tres ramas principales en la prueba de la teoría:

1. Axiomatics parecen ser necesariamente sintáctica: las fórmulas de qué se trata;
2. Consistencia relativa & ordinal análisis, que son en última instancia acerca de la caracterización de provability fuerza de varias maneras: estos son tal vez como sintáctica como la teoría de la recursividad;
3. Estructurales de la prueba de la teoría, donde nos preocupamos por la analítica de las pruebas: hay programas para intentar abstracto, lejos de la sintaxis, tales como pruebas categóricas de la teoría, pero demasiado de la prueba de la teoría de no ceder a este tipo de análisis, por lo que no podemos decir que estos son exitosas hasta el momento.

Answer 2

Me gustaría plantear que la prueba de la teoría es exactamente el sintáctica parte de la lógica, y las otras tres ramas (teoría de conjuntos, el modelo de la teoría, y la teoría de la recursividad) son lo que queda cuando te deshaces de la sintaxis. La que es probablemente la razón por la que esas tres ramas, para obtener más atención hoy en día.

Answer 3

Elaborar ligeramente en Neel del post: el hecho de que no todas las pruebas en intuitionist y substructural lógicas identificadas es una fortaleza y no una debilidad cuando se ve a través de la lente de la de Curry-Howard isomorfismo que muestra que la lógica computacional contenido.

Básicamente, el Curry-Howard isomorfismo de los estados que las proposiciones en intuitionist la lógica puede ser identificado con los tipos en un lenguaje de programación y las pruebas pueden ser identificados con los programas. En la lógica clásica todas las pruebas de una determinada proposición se identifican de modo que la lógica clásica es demasiado empobrecido para servir como un modelo para el cálculo. En otras palabras, el hecho de que hay múltiples pruebas de la misma proposición en intuitionist lógica es lo que nos permite tener varios programas con el mismo tipo.

Answer 4

Yo creo que tu observación es muy buena, pero este fenómeno se limita a la lógica clásica y no seguir celebrando cuando nos movemos a intuitionistic o substructural lógicas.

Una forma de entender el papel de la sintaxis es tomar las conectivas de la lógica como la explicación de lo que cuenta como una prueba legítima de que la proposición. Así que una conjunción $A \land B$ se puede demostrar con una prueba de $A$ y una prueba de $B$, y una implicación $A \implies B$ puede ser puede ser probado con una prueba de $B$, suponiendo una hipotética prueba de $A$, y así sucesivamente. Por el contrario, damos también las reglas que explican cómo utilizar las proposiciones verdaderas-por ejemplo, de $A \land B$, podemos volver a derivar $A$, y también podemos rederive $B$.

Si el trabajo esta fuera formalmente, se obtiene Gentzen del sistema de deducción natural. La deducción natural de los sistemas para la buena lógica de admitir un teorema de la forma normal para las pruebas. El procedimiento de normalización también nos da una relación de equivalencia en las pruebas (dos pruebas son equivalentes si tienen la misma forma normal), y se da la circunstancia de que para la lógica clásica, todas las pruebas son equivalentes. (Esta es una pequeña mentira: nos puede dar más refinada de las cuentas de la equivalencia de las clásicas pruebas que no sirven de todo, pero la respuesta correcta aquí aún no está totalmente resuelto....)

La equivalencia de las pruebas significa que podemos tomar el punto de vista de que el significado de un clásico de la proposición es su valor de verdad, es decir, su provability -- y de manera algebraica de los modelos de la lógica clásica contener toda la información contenida en un clásico de la proposición. No necesitamos de las pruebas, y así sintaxis toma un papel secundario.

Pero en intuitionistic y substructural de la lógica como lógica lineal, no todas las pruebas son equiparados. Esto significa que no podemos tomar el punto de vista de que toda la información relevante acerca de una proposición contenida en su valor de verdad, y así sintaxis conserva un papel más importante.