Wikipedia dice que el secuente cálculo es sólido y completo (http://en.wikipedia.org/wiki/Sequent_calculus#Properties_of_the_system_LK). Gödel primer teorema de la incompletitud dice que el sistema es capaz de hacer aritmética puede no ser completa y coherente. Qué significa que el Secuente Cálculo no es capaz de hacer aritmética o es incompleta o se me olvida algún punto sutil de teorema de la incompletitud?
Respuestas
¿Demasiados anuncios?
Hay un desafortunado choque de la terminología cuando se habla de integridad en la lógica (agravado por el hecho de que hay un Gödel integridad del teorema así como Gödel del teorema de la incompletitud).
Un sistema formal (como el secuente cálculo o la más conocida de la deducción natural o de Hilbert-estilo de los sistemas de prueba, posiblemente con la debida axiomas etc.) se llama completa si semántica de la verdad implica sintáctica de la verdad. Es decir, si una declaración es verdadera en todos los modelos del sistema (que es semánticamente cierto), a continuación, en realidad, es demostrable en el sistema (que es sintácticamente válida). Esta noción de integridad es lo que se entiende en el artículo de wiki en el secuente cálculo. Es también el contenido de Gödel integridad del teorema: cualquier Hilbert o deducción natural estilo del sistema en primer orden la lógica es completa. El recíproco de esta propiedad, que todo lo que es comprobable es siempre cierto, es conocida como la solidez.
Por otro lado, un sistema formal es (también) llamado completa si es consistente y para cualquier frase, $\varphi$ $\varphi$ o $\lnot\varphi$ es demostrable en la teoría. Esta noción de integridad es lo que se discute en Gödel los teoremas de incompletitud.
Estos dos significados de la integridad, son independientes uno de otro; la mayoría de los sistemas de interés se completa en el antiguo sentido, pero puede o no puede ser completa, en este último sentido.
Njax3SmmM2x2a0Zf7Hpd
Puntos
146
Miha Habič la respuesta es exactamente la correcta, así que esto es sólo por medio de la amplificación y de un comentario sobre el doble uso de "completo".
Poner simbólicamente puede ayudar.
Una teoría de la $T$ con el conjunto de axiomas $\Sigma$ es la negación-completa el fib, para cualquier frase, $\varphi$ de su idioma, $\Sigma \vdash \varphi$ o $\Sigma \vdash \neg\varphi$.
Así que una teoría completa decide cada frase de su lenguaje.
Un sistema lógico [como el secuente cálculo] es semánticamente completa iff para cualquier conjunto de wffs $\Sigma$ y cualquier frase, $\varphi$ si $\Sigma \vDash \varphi$ $\Sigma \vdash \varphi$
donde como de costumbre '$\vdash$' significa la relación de formal deducibility en la prueba lógica del sistema, y '$\vDash$' significa la pertinente relación de consecuencia semántica. Para una completa deductivo de la lógica nos permite dar formal derivaciones de todo lo que es semánticamente supone dadas las premisas.
Estas nociones de integridad, son claramente diferentes. Mientras eso sucede, la primera prueba de la semántica de la integridad de un sistema a prueba de quantificational lógica también fue debido a Gödel, y el resultado es a menudo referido como Gödel 'Teorema de Completitud'. El tema de que el teorema es, por tanto, evidentemente no debe ser confundido con el tema de Gödel (Primera) 'Teorema de la Incompletitud": la semántica de la integridad de un sistema a prueba de quantificational la lógica es una cosa, la negación de la incompletitud de ciertas teorías como suficiente aritmética muy otra cosa.
OK, aquí hay una situación potencialmente peligrosa doble uso del término 'completa'. Pero este doble uso no es un caso de terminológico perversidad, incluso a pesar de los lógicos, puede ser culpable de eso! De allí el siguiente paralelo vale la pena destacar (y que explica por qué "completa" es el apt plazo en ambos casos):
Una negación-completo de la teoría es uno de esos que, si se agrega como un nuevo axioma algunos proposición que no puede ya ser derivado en la teoría, entonces la teoría se vuelve inútil por la virtud de volverse incoherente. Asimismo, un semánticamente completo sistema deductivo es uno de esos que, si se agrega una nueva lógica axioma que no puede ya ser derivados (o una nueva regla de inferencia que no puede ser establecido como un derivado de la regla del sistema), entonces la lógica se vuelve inútil en virtud de que la justifican argumentos que no son semánticamente válido.
