¿Por qué la solidez implica consistencia?

Estaba leyendo la pregunta ¿ Consistencia e integridad implican solidez? y la primera declaración dice:

Entiendo que la solidez implica consistencia.

Lo que me intrigó bastante porque pensé que la solidez era una afirmación más débil que la consistencia (es decir, pensé que los sistemas consistentes tenían que ser sólidos, pero supongo que no es cierto). Estaba usando la definición informal que Scott Aaronson estaba usando en su curso 6.045 / 18.400 en el MIT por consistencia y solidez:

1. Solidez = Un sistema de prueba es sólido si todas las afirmaciones que prueba son realmente verdaderas (todo lo que es demostrable es Verdadero). es decir, IF ( $\phi$ es demostrable)$\implies$( $\phi$ es cierto). Entonces SI (hay un camino hacia una fórmula) ENTONCES (esa fórmula es verdadera)
2. Consistencia = un sistema consistente nunca prueba A y NO (A). Entonces solo una A o su negación puede ser Verdadero.

Usando esas definiciones (quizás informales) en mente, construí el siguiente ejemplo para demostrar que hay un sistema que es sólido pero no consistente:

La razón por la que pensé que era un sistema de sonido es porque, por supuesto, los axiomas son ciertos. Entonces A y no A son ambos verdaderos (sí, sé que la ley del medio excluido no está incluida). Dado que la única regla de inferencia es la negación, obtenemos que podemos alcanzar tanto A como no A desde los axiomas y alcanzarnos entre nosotros. Por lo tanto, solo alcanzamos declaraciones Verdaderas con respecto a este sistema. Sin embargo, por supuesto, el sistema no es consistente porque podemos probar la negación de la única declaración en el sistema. Por lo tanto, he demostrado que un sistema de sonido podría no ser consistente. ¿Por qué es incorrecto este ejemplo? ¿Qué hice mal?

En mi cabeza, esto tiene sentido intuitivamente porque la solidez solo dice que una vez que comenzamos desde axioma y arrancamos las reglas de inferencia, solo llegamos a destinos (es decir, declaraciones) que son verdaderos. Sin embargo, en realidad no dice a qué destino llegamos. Sin embargo, la consistencia dice que solo podemos llegar a destinos que son o (ambos no ambos). Por lo tanto, cada sistema consistente debe incluir la ley del medio excluido como un axioma, que por supuesto no lo hice y luego simplemente incluí la negación del único axioma como el único otro axioma. Entonces, ¿no parece que hice algo demasiado inteligente, pero de alguna manera algo está mal?¬ $A$$\neg A$

Me doy cuenta de que podría ser un problema porque estoy usando la definición informal de Scott. Incluso antes de escribir la pregunta, revisé wikipedia, pero su definición no tenía sentido para mí. En particular la parte que dicen:

con respecto a la semántica del sistema

su cita completa es:

Cada fórmula que se puede probar en el sistema es lógicamente válida con respecto a la semántica del sistema.

Recomiendo buscar en la lógica formal más allá de las descripciones vagas y onduladas a mano. Es interesante y muy relevante para la informática. Desafortunadamente, la terminología y el enfoque limitado de incluso los libros de texto específicamente sobre lógica formal pueden presentar una imagen deformada de lo que es la lógica. El problema es que la mayoría de las veces cuando los matemáticos hablan de "lógica", (a menudo implícitamente) se refieren a la lógica proposicional clásica o la lógica clásica de primer orden. Si bien estos son sistemas lógicos extremadamente importantes, no están cerca de la amplitud de la lógica. En cualquier caso, lo que voy a decir se lleva a cabo en gran medida en ese contexto limitado, pero quiero dejar en claro que está sucediendo en un contexto particular y que no es necesario que sea cierto fuera de él.

Primero, si la consistencia se define como no probar tanto como , ¿qué sucede si nuestra lógica ni siquiera tiene negación o si¬ A $A$$\neg A$$\neg$significa algo más? Claramente, esta noción de consistencia hace algunas suposiciones sobre el contexto lógico dentro del cual opera. Típicamente, esto es que estamos trabajando en la lógica proposicional clásica o alguna extensión de la misma, como la lógica clásica de primer orden. Hay múltiples presentaciones, es decir, listas de axiomas y reglas, que podrían llamarse lógica clásica proposicional / de primer orden pero, para nuestros propósitos, lo que realmente no importa. Son equivalentes en algún sentido adecuado. Por lo general, cuando hablamos de un sistema lógico nos referimos a una teoría (clásica) de primer orden. Esto comienza con las reglas y los axiomas (lógicos) de la lógica clásica de primer orden, a los que se agregan símbolos de función, símbolos predicados y axiomas (llamados axiomas no lógicos). Estas teorías de primer orden suelen ser lo que '

Luego, solidez generalmente significa solidez con respecto a una semántica. La consistencia es una propiedad sintáctica que tiene que ver con las pruebas formales que podemos hacer. La solidez es una propiedad semántica que tiene que ver con la forma en que interpretamos las fórmulas, los símbolos de función y los símbolos predicados en objetos y enunciados matemáticos. Incluso para comenzar a hablar sobre la solidez, debe dar una semántica, es decir, una interpretación de las cosas antes mencionadas. Nuevamente, tenemos una separación entre los conectivos lógicos y los axiomas lógicos, y los símbolos de función, símbolos predicados y axiomas no lógicos. Lo que hace que los conectivos conectivos y los axiomas lógicos sean lógicos desde el punto de vista semántico es que son tratados especialmente por la semántica, mientras que los símbolos de función, los símbolos predicados y los axiomas no lógicos no.$[\![\varphi\land\psi]\!]=[\![\varphi]\!]\cap[\![\psi]\!]$ donde uso como la interpretación de la fórmula . En particular, Donde es el conjunto de dominios. La idea es que una fórmula se interpreta como el conjunto de (tuplas de) elementos de dominio que satisfacen la fórmula. Una fórmula cerrada (es decir, una sin variables libres) se interpreta como una relación nula, es decir, un subconjunto de un conjunto singleton que solo puede ser ese singleton o el conjunto vacío. Una fórmula cerrada es "verdadera" si no se interpreta como el conjunto vacío. La solidez es entonces la afirmación de que cada fórmula demostrable (cerrada) es "verdadera" en el sentido anterior.$[\![\varphi]\!]$$\varphi$$[\![\neg\varphi]\!]=D\setminus[\![\varphi]\!]$$D$

Es fácil desde aquí, incluso a partir del bosquejo que he dado, demostrar que la solidez implica consistencia (en el contexto de las lógicas clásicas de primer orden y la semántica que he bosquejado). Si su lógica es el sonido, luego cada demostrables interpreta fórmula como un conjunto no vacío, sino está siempre interpretado como el conjunto vacío, no importa qué fórmula es, y por lo tanto no puede ser demostrable, es decir, su lógica es consistente.

La solidez y la consistencia son propiedades de los sistemas deductivos. La solidez solo se puede definir con respecto a alguna semántica que se supone que se proporciona independientemente del sistema deductivo.

En el ámbito de la semántica, las dos propiedades están relacionadas

Definición 1 ( Solidez [Semántica] - tomado de Wikipedia ) La solidez de un sistema deductivo es la propiedad de que cualquier oración que sea demostrable en ese sistema deductivo también es verdadera en todas las interpretaciones o estructuras de la teoría semántica para el lenguaje sobre el cual esa teoría Es basado.

Definición 2 ( Consistencia [Semántica] ) Un conjunto de oraciones en el idioma es consistente si y sólo si existe una estructura de la lengua que satisface todas las oraciones en . Un sistema deductivo es consistente si existe una estructura que satisfaga todas las fórmulas demostrables en él.$A$$\mathfrak{L}$$\mathfrak{L}$$A$

Con las dos definiciones dadas anteriormente, está claro que la solidez implica consistencia. Es decir, si el conjunto de todas las oraciones comprobables se mantiene en todas las estructuras del lenguaje, entonces existe al menos una estructura que las satisface.

Su sistema de prueba no es sólido ni consistente, ya que no es una proposición verdadera a menos que , en cuyo caso no es una proposición verdadera. Este argumento muestra que cada sistema de prueba de sonido también es consistente.A ≡ ⊤ ¬ A ≡ $A$$A \equiv \top$$\lnot A \equiv \bot$

A menudo, cuando encontramos sistemas lógicos, están motivados por un intento de describir un fenómeno preexistente. Por ejemplo, la aritmética de Peano es un intento de axiomatizar los números naturales junto con las operaciones de suma y multiplicación.

La solidez solo se puede definir en relación con el fenómeno que está intentando describir, y esencialmente significa que sus axiomas y reglas de inferencia realmente describen la cosa en cuestión. Entonces, por ejemplo, la aritmética de Peano es sólida porque sus axiomas y reglas de inferencia realmente son verdaderas para los números naturales.

Esto, por supuesto, implica que usted tiene un concepto de "números naturales" más allá de la definición de Peano de ellos, y alguna noción de lo que es verdadero o falso para los números naturales sin haber derivado estas verdades de ningún conjunto particular de axiomas. Intentar explicar de dónde provienen esas verdades o cómo se pueden verificar puede llevarte a aguas filosóficas. Pero si se da por sentado que hay números naturales, y hay una colección de hechos verdaderos sobre ellos, entonces puede ver el proyecto de axiomatización como un simple intento de llegar a una especificación formal concisa a partir de la cual muchos de los más importantes las verdades se pueden derivar. Entonces, una axiomatización es sólida si todo lo que puede probar realmente está en la colección de verdades especificada previamente, es decir,

(Tenga en cuenta en particular que su especificación formal no probará todo lo que es cierto sobre los números naturales, y además no describirá de manera única los números naturales en el sentido de que hay otras estructuras, diferentes de los números naturales, en las que los axiomas de Peano son también cierto)

En la lógica de primer orden, al menos, una teoría es coherente si tiene algún modelo. La solidez significa que tiene el modelo específico que deseaba: la estructura particular que intentaba describir con su teoría realmente es un modelo de su teoría. Desde esta perspectiva, está claro por qué la solidez implica consistencia.

Como ejemplo de una teoría que es consistente pero no sólida: la aritmética de Peano, PA, es capaz de codificar fórmulas lógicas como construcciones aritméticas, y en particular puede codificar la oración "PA es consistente" ("no hay prueba de falsedad de los axiomas de la AP "). Llama a esta oración Con (PA). También puede ser consciente de que (dado que es sólido y, por lo tanto, consistente), PA no puede probar Con (PA), según el primer teorema de incompletitud de Gödel. Esto también significa que la teoría PA +$\neg$Con (PA) no puede probar una contradicción, por lo que debe ser consistente. Pero no es sólido: afirma que existe un número natural que codifica una prueba de falsedad de los axiomas de la AP, pero no es posible que exista tal número en los números naturales "reales", ya que de lo contrario podríamos extraer una prueba genuina de la inconsistencia de PA de ella.

PA + Con (PA) tiene modelos, pero son modelos que deben incluir objetos "extra", "números naturales no estándar", incluido uno que, según afirma, codifica la "prueba" en cuestión. La teoría simplemente no está equipada con las herramientas necesarias para distinguir estos elementos no estándar de los miembros genuinos de , o para demostrar que la prueba no es una prueba legítima.$\neg$$\mathbb N$

Alternativamente, puede interpretar esto como: PA + Con (PA) es un sistema lógico perfectamente legítimo: simplemente no describe con precisión los números naturales, y los números naturales no son un modelo de ello.$\neg$

Una cosa más: no asumimos que los axiomas son verdaderos por definición. Todos los axiomas son, por definición, solo los componentes básicos de las pruebas. Son solo afirmaciones: solo son verdaderas o falsas cuando se aplican a objetos matemáticos particulares. Puede tener axiomas falsos, es bastante tonto, porque su sistema no necesariamente será sólido e inmediato.

Para tener una respuesta concisa (e intuitiva) parafrasearé lo que Scott Aaronson dijo en su conferencia MIT 6.045 / 18.400. Él dijo algo como esto:

La solidez significa que todo lo comprobable es cierto. Dado que la coherencia significa que no hay contradicciones y que la solidez ya está involucrada, el concepto de verdad y la verdad deben ser consistentes (es decir, ¡Verdadero! = Falso), entonces debe significar que los sistemas de sonido también son consistentes. Entonces, la solidez implica consistencia porque (verdaderamente) las cosas verdaderas no tienen contradicciones.

Ahora que reflexiono, me doy cuenta de que tenía algunas suposiciones / ideas incorrectas:

1. No me di cuenta de que la solidez era sobre semántica. Por lo tanto, no me di cuenta de que el solo uso de reglas de inferencia de los axiomas no es suficiente para conducir a verdaderas consecuencias (y que no lo garantiza, lo que pensé que era imposible alcanzar cosas contradictorias siempre que comenzáramos desde los axiomas y reglas de inferencia válidas).
2. Pensé que mientras los axiomas fueran ciertos y las reglas de inferencia tuvieran sentido, todo lo que procediera sería cierto. De lo que ahora me doy cuenta podría no ser cierto, ya que si solo tenemos una lista gigante de axiomas y reglas de inferencia, es difícil razonar si todo lo que sigue será cierto. es decir, simplemente comenzar desde un axioma y usar una regla de inferencia válida no es suficiente para garantizar que el siguiente paso sea verdadero.
3. Lo anterior se combina esencialmente con el hecho de que no me di cuenta de que hay dos niveles de complejidad, 1) semántica 2) sintáctica. Arrancar el juego de símbolos crujientes puede conducir a contradicciones.
4. No me di cuenta de que no conocía la caracterización adecuada de la verdad, que Derek hizo un gran trabajo en la caracterización.