¿Por qué deberíamos preocuparnos por las pruebas sintácticas si podemos demostrar semánticamente que los enunciados son verdaderos?

Question

Me refiero a la lógica clásica.

Admito que puede ser una pregunta ingenua, pero por lo que yo entiendo: La vinculación sintáctica significa que hay una prueba utilizando la sintaxis del lenguaje, mientras que por otro lado la vinculación semántica no se preocupa por la sintaxis, simplemente significa que una afirmación debe ser verdadera si un conjunto de otras afirmaciones también son verdaderas.

Dicho esto, ¿no es suficiente la vinculación semántica para saber si una afirmación es verdadera o no? ¿Por qué necesitamos pruebas sintácticas?

Sé que, en el caso de la lógica booleana, demostrar las afirmaciones mediante tablas de verdad se vuelve intratable muy rápidamente, pero, en esencia, ¿no es "superior" la vinculación semántica? ¿No depende de cómo construyamos la gramática?

Gracias

Edición: Supongamos que no se diera el caso de que encontrar una asignación satisfactoria a un enunciado booleano arbitrario fuera un problema exponencialmente creciente, entonces ¿necesitaríamos siquiera la vinculación sintáctica?

Answer 1

En primer lugar, permítanme aclarar la terminología:

Mediante una prueba sintáctica ( $\vdash$ ) nos referimos a una prueba que opera puramente sobre un conjunto de reglas que manipulan cadenas de símbolos, sin hablar de notaciones semánticas como asignación, verdad, modelo o interpretación. Un sistema de prueba sintáctico es aquel que dice, por ejemplo, "Si tienes $A$ escrito en una línea y $B$ en otra línea, entonces puede escribir los símbolos $A \land B$ en una línea inferior". Ejemplos de sistemas de demostración sintáctica son los cálculos de tipo Hilbert, los cálculos secuenciales y la deducción natural en sus diversos sabores o los cuadros de Beth, también conocidos como árboles de verdad.

Mediante una prueba semántica ( $\vDash$ ) nos referimos a una prueba que opera sobre las nociones semánticas del lenguaje, como asignación, verdad, modelo o interpretación. Ejemplos de pruebas semánticas son las tablas de verdad, la presentación de (contra)modelos o argumentos en texto (del tipo "Supongamos $A \to B$ es verdadera. Entonces hay una asignación tal que...").

Además, el término "vinculación" suele entenderse como una noción puramente semántica ( $\vDash$ ), mientras que la contraparte sintáctica ( $\vdash$ ) se denomina normalmente derivabilidad .

(La división " $\vDash$ = semántica/modelos y $\vdash$ = sintaxis/pruebas" es simplificar un poco las cosas semántica de la teoría de la prueba Por ejemplo, argumenta que una semántica puede establecerse en términos de pruebas formales (= "sintácticas") en lugar de sólo por consideraciones teóricas del modelo, pero en aras de esta explicación, mantengamos esta doble distinción más simple).

Lo aclaro porque la forma en que expones las cosas no es del todo exacta:

La vinculación sintáctica significa que hay una prueba utilizando la sintaxis del lenguaje

En cierto modo sí, la sintaxis de una lógica es siempre relevante cuando se habla de nociones como la de vinculación o derivabilidad -- pero la característica crucial que nos hace llamar a esta noción sintáctica no es porque la sintaxis del lenguaje esté implicada en el establecimiento de relaciones de vinculación o derivabilidad sino porque la conjunto de normas que utilizamos es puramente sintáctico, es decir, se limita a operar con cadenas de símbolos sin hacer referencia explícita al significado.

mientras que por otro lado la vinculación semántica no se preocupa por la sintaxis

Eso no es del todo exacto: para establecer el valor de verdad de una fórmula y, por tanto, nociones como validez o vinculación, tenemos que investigar la sintaxis de una fórmula para determinar cualquier valor de verdad. Al fin y al cabo, la verdad se define inductivamente sobre la estructura (= la sintaxis) de las fórmulas: " $[[A \land B]]_v = \text{true iff} [[A]]_v = \text{true and } [[B]]_v = \text{true}...$ " Si no nos importara la sintaxis, no podríamos hablar de semántica.

---

Ahora a su pregunta real:

¿Por qué deberíamos preocuparnos por las pruebas sintácticas si podemos demostrar semánticamente que los enunciados son verdaderos?

La respuesta corta es: porque las pruebas sintácticas suelen ser mucho más fáciles.

Para la lógica proposicional, el mundo sigue siendo relativamente inocente: Podemos simplemente escribir una tabla de verdad, mirar el valor de verdad de cada fórmula y decidir si se da el caso de que todas las líneas en las que las columnas de todas las premisas tienen un "verdadero" también tienen la columna de la conclusión como "verdadero". Como señalas, este procedimiento explota rápidamente para fórmulas con muchas variables proposicionales, pero sigue siendo un procedimiento determinista que se puede hacer en tiempo finito.

También podríamos presentar una prueba en lenguaje natural argumentando en términos de asignaciones de verdad. Esto puede ser un poco más engorroso, pero podría ser más instructivo, y sigue siendo relativamente manejable para el lenguaje y la interpretación relativamente simples de la lógica proposicional.

Pero las cosas empeoran cuando entramos en la lógica de primer orden. Aquí nos enfrentamos a fórmulas que cuantifican sobre modelos cuyos dominios son potencialmente infinitos. Peor aún, en contraste con la lógica proposicional donde el número de asignaciones es (~= interpretaciones) siempre finito y completamente determinado por el número de variables proposicionales, las estructuras (~= interpretaciones) en las que una fórmula de primer orden puede o no ser verdadera son ilimitadas en tamaño y forma. Es decir, no sólo las estructuras en sí pueden ser infinitas, sino que ahora nos enfrentamos a una cantidad infinita de estructuras en las que nuestras fórmulas pueden ser interpretadas en primer lugar. Escribir simplemente una tabla de verdad ya no funcionará para el lenguaje de la lógica de predicados, por lo que determinar el valor de verdad, y por lo tanto las propiedades y relaciones semánticas como la validez y la vinculación, ya no es un simple procedimiento determinista para la lógica de predicados.

Por tanto, si queremos presentar una prueba semántica, tenemos que recurrir a argumentos sobre las estructuras que satisface o no satisface una fórmula. Aquí es donde entra una interesante dualidad:

• Para demostrar que

  • una meta-afirmación semántica cuantificada existencialmente es verdadera (Por ejemplo "La fórmula $\phi$ es satisfacible", es decir, " Existe un modelo de $\phi$ ) o
  • una meta-afirmación semántica universalmente cuantificada es falsa (Por ejemplo $\not \vDash \phi$ La fórmula fórmula $\phi$ no es válido", es decir, " No se trata de que todos los las estructuras satisfacen $\phi$ )

  basta con proporcionar un (contra)modelo y ya está: Si encontramos una sola estructura en la que $\phi$ es cierto, entonces sabemos que $\phi$ es satisfacible, y a la inversa, si encontramos una estructura en la que $\phi$ no es cierto entonces ahora que $\phi$ no es válido.

  Análogamente, para demostrar que

  • una fórmula existencialmente cuantificada del lenguaje de objetos ( $\exists x ...$ ) es verdadera en una estructura o
  • una fórmula universalmente cuantificada del lenguaje de objetos ( $\forall x ...$ ) es falso en una estructura,

  basta con encontrar un elemento en el dominio de la estructura que proporcione un ejemplo para la fórmula cuantificada existencialmente o, respectivamente, un contraejemplo a la cuantificación universal y ya está.

Sin embargo,

• para demostrar que

  • una meta-afirmación semántica universalmente cuantificada es verdadera (Por ejemplo $\vDash \phi$ La fórmula fórmula $\phi$ es válido", es decir, " Todo las estructuras satisfacen $\phi$ ), o
  • una meta-afirmación semántica cuantificada existencialmente es falsa (Por ejemplo "La fórmula $\phi$ es insatisfactible", es decir, " No existe ningún modelo de $\phi$ ),

  de repente nos enfrentamos a la difícil tarea de hacer una afirmación sobre todo posibles estructuras. No podemos simplemente enumerarlas, ya que hay ininitadamente muchas, así que lo único que podemos hacer es escribir un texto en lenguaje natural argumentando sobre los posibles valores de verdad de las fórmulas mostrando finalmente que todas las estructuras deben cumplir o no un determinado requisito.

  Análogamente, para demostrar que

  • una fórmula universalmente cuantificada del lenguaje de objetos ( $\forall x ...$ ) es verdadera en una estructura o
  • una fórmula existencialmente cuantificada del lenguaje de objetos ( $\exists x ...$ ) es falso en una estructura,

  tenemos que iterar sobre todos los elementos del dominio de la estructura. Si el dominio es finito, tenemos suerte y podemos simplemente pasar por todos los valores posibles (aunque esto puede llevar bastante tiempo si el dominio es lo suficientemente grande), pero si es infinito, no hay manera de que podamos terminar si simplemente comprobamos por fuerza bruta la fórmula de los elementos uno tras otro.

Esta es una situación bastante desagradable, y exactamente el punto en el que las pruebas sintácticas son muy útiles.

Recordemos la definición de vinculación:

$\Gamma \vDash \phi$ si todo interpretaciones que satisfacen todas las fórmulas de $\Gamma$ también satisfacen $\phi$

o de forma equivalente

$\Gamma \vDash \phi$ si no hay interpretación que satisface todas las fórmulas de $\Gamma$ pero no $\phi$ .

Este es precisamente el tipo de cuantificación universal que dificulta las pruebas puramente semánticas: Tendríamos que establecer una prueba sobre la infinidad de todas las estructuras posibles para comprobar si la relación de vinculación semántica se mantiene o no.
Pero ahora mira la definición de derivabilidad sintáctica:

$\Gamma \vdash \phi$ si hay un derivación con premisas de $\Gamma$ y conclusión $\phi$ .

El desagradable cuantificador universal se convirtió de repente en uno existencial. En lugar de tener que discutir sobre todo las posibles estructuras, ahora basta con mostrar sólo un derivación sintáctica y ya está. (Lo mismo ocurre en el caso de que no tengamos ninguna premisa, es decir $\vDash \phi$ (" $\phi$ es válido" = "verdadero en todas las estructuras" vs. $\vdash \phi$ (= " $\phi$ es derivable" = "existe una derivación sin supuestos abiertos y $\phi$ como conclusión). Esta es una enorme ventaja, llámala "superior" si quieres.

Ahora tenemos una especie de disparidad: Para algunas cosas la semántica es difícil mientras que la sintaxis es fácil, así que ¿cómo podemos utilizar esta disparidad para el bien?
Por suerte, en el caso de la lógica clásica, disponemos de solidez y completitud:

Solidez: Si $\Gamma \vdash \phi$ entonces $\Gamma \vDash \phi$ -- si encontramos una derivación sintáctica, entonces sabemos que la vinculación se mantiene semánticamente.

Completo: Si $\Gamma \vDash \phi$ entonces $\Gamma \vdash \phi$ -- si una vinculación semántica se mantiene, entonces podemos encontrar una derivación sintáctica.

Aunque cualquier sistema de derivación razonable será sólido con respecto a la semántica del lenguaje, la completitud es un resultado no trivial y muy poderoso: Si queremos demostrar una vinculación semántica, por completitud sabemos que debe haber una derivación sintáctica, por lo que podemos ir a buscar una de esas derivaciones, y en cuanto lo hagamos, la solidez nos asegura que se trata de una prueba de que la vinculación es semánticamente válida. Por lo tanto, podemos utilizar las pruebas sintácticas para evitar los engorrosos argumentos semánticos que implican la cuantificación meta-lógica sobre todas las estructuras. Esto está muy bien.

Ahora observa cómo se invierten las cosas para el cálculo sintáctico:

• Para demostrar que
  • un meta-enunciado sintáctico cuantificado universalmente es verdadero o un meta-enunciado sintáctico cuantificado existencialmente es falso (Por ejemplo $\not \vdash \phi$ La fórmula fórmula $\phi$ es sub-vivible", es decir, " No hay derivación con conclusión $\phi$ "/" Todo intenta encontrar una derivación con conclusión $\phi$ eventualmente fallan)

tendríamos que argumentar sobre todas las posibles pruebas sintácticas, lo que de nuevo puede ser difícil.

Ahora podemos aplicar los resultados de solidez y plenitud en la otra dirección: Si queremos demostrar que una fórmula no es derivable, entonces por contraposición en la completitud sabemos que no es válida (porque si lo fuera, entonces por completitud habría una derivación), así que podemos realizar una prueba semántica proporcionando sólo un contramodelo a la validez de $\phi$ y casi hemos terminado; porque entonces, de nuevo por contraposición a la solidez, podemos estar seguros de que si la fórmula no es válida, no habrá derivación (porque si hubiera una derivación para algo que no es semánticamente válido, nuestro sistema no sería sólido), así que tenemos nuestra prueba de la infravalidez sin necesidad de discutir sobre hipotéticas derivaciones que no pueden existir.

Y es precisamente así como se produce la mencionada dualidad:

--------------------------------------------------------------------------------
            semantic                          syntactic
--------------------------------------------------------------------------------
positive    ⊨                                 ⊢                                 
            universal quantif.                existential quantif.
            ("all structures"/                ("there is a derivation"/
             "no structure such that not")     "not all derivations fail")
            => difficult

Answer 2

La principal razón para preocuparse por las pruebas sintácticas es que son cruciales para los fundamentos de las matemáticas. Si estamos formulando axiomas para la teoría de conjuntos, que utilizaremos como base para todas las matemáticas, necesitamos una noción inequívoca de prueba que se base en un mínimo absoluto de conceptos previos (ya que estamos intentando construir todo el resto de las matemáticas a partir de esto). Las pruebas sintácticas son perfectas para esto: sólo son cadenas finitas de símbolos que siguen ciertas reglas simples. Las pruebas semánticas, por otro lado, sólo tienen sentido una vez que se tiene una metateoría potente que puede razonar sobre cosas como los modelos. Esto es bastante inútil para los propósitos fundacionales, ya que sólo devuelve la cuestión fundacional a la metateoría.

Para decirlo de otra manera, digamos que estás trabajando con ZFC como tu metateoría, como es habitual en las matemáticas modernas. Si quieres estudiar una teoría de primer orden, no necesitas pruebas sintácticas, puedes usar siempre el razonamiento semántico. ¿Pero qué es una prueba semántica? No es más que una prueba sintáctica en tu metateoría ZFC, que habla de modelos de tu teoría de primer orden dentro del lenguaje de primer orden de la teoría de conjuntos.

---

Por otro lado, me gustaría enfatizar que si no te preocupas por los fundamentos y sólo estás haciendo teoría de modelos dentro de ZFC, no hay prácticamente ninguna razón para pensar en pruebas sintácticas.* Aunque lemontree mencionó en su respuesta que las pruebas sintácticas dan una manera más fácil de razonar sobre todo eso no es realmente exacto, porque puedes imitar los pasos de una prueba sintáctica en términos semánticos. Por ejemplo, una de las reglas de inferencia que se pueden utilizar en las pruebas sintácticas es que si tienes $\varphi$ y $\psi$ se puede deducir $\varphi\wedge\psi$ . Pues bien, ¿adivina qué? ¡También se puede hacer esto en las pruebas semánticas! Si tienes un modelo que satisface tanto $\varphi$ y $\psi$ entonces también satisface $\varphi\wedge\psi$ por definición de satisfacción. Del mismo modo, todas las demás reglas de inferencia sintáctica pueden traducirse trivialmente en argumentos semánticos.

_{*Ok, esto es un poco exagerado. Incluso si no estás haciendo fundamentos, puedes preocuparte por las pruebas sintácticas por razones similares a las de los fundamentos, a saber, su naturaleza finita. Así que, por ejemplo, si tienes una teoría finitamente axiomatizable que sabes (quizás por medios semánticos) que es completa, entonces usando pruebas sintácticas (y el teorema de completitud) puedes deducir que existe un algoritmo que decide si cualquier frase está en la teoría.}

Answer 3

La buena noticia es que para la lógica de primer orden tenemos los teoremas de solidez y completitud: Para cualquier teoría de primer orden $T$ y cualquier frase $\sigma$ en el mismo idioma, $T \models \sigma$ si y sólo si $T \vdash \sigma$ . Es decir, la verdad semántica y sintáctica son equivalentes.

A la luz de ese teorema, podrías, si lo deseas, centrarte totalmente en la verdad semántica (como hacen a veces los teóricos del modelo) o totalmente en la verdad sintáctica (como hacen a veces los teóricos de la prueba). Cada área tiene sus propias preguntas y técnicas, pero están estrechamente vinculadas, por lo que también hay oportunidad de mezclar ambas.

Una consecuencia directa del teorema de la completitud es el teorema de la compacidad, que es absolutamente fundamental para la teoría de modelos de primer orden. Dice que si todo subconjunto finito de alguna teoría $T$ tiene un modelo, entonces $T$ tiene un modelo. Se puede demostrar esto observando que si $T$ no tuviera un modelo, entonces se podría escribir una prueba de una contradicción a partir de $T$ . Como toda prueba es finita, sólo un número finito de afirmaciones de $T$ son necesarios en su prueba, por lo que debe haber un subconjunto finito de $T$ que demuestra una contradicción, y por lo tanto no tiene modelos. (Es posible demostrar la compacidad por métodos que parecen más semánticos, como los ultraproductos, pero la prueba esbozada aquí es la primera que ve mucha gente).

Answer 4

La respuesta aceptada es buena y amplia, pero permítanme intentar destilar un poco el punto clave:

¿Cómo se justifica que una prueba semántica sea correcta?

Una "prueba semántica" debe seguir siendo una prueba, en algún sentido rigurosamente comprobable. Si yo afirmo que tengo una prueba semántica y tú la impugnas, ¿cómo la perseguimos con un criterio claro de corrección? Desglosándola en pasos básicos mínimos y acordando cuáles son los pasos básicos válidos. En otras palabras, nos ponemos de acuerdo en una noción sintáctica de prueba para la metateoría, y luego exponemos la prueba semántica como una prueba sintáctica para la metateoría. Así que, en resumen:

Cada Una noción de prueba suficientemente rigurosa debe ser, en su base, sintáctica. Una "prueba semántica" significa "una prueba en la sintaxis de la metateoría, sobre la teoría del objeto", por lo que sigue dependiendo de una noción de prueba sintáctica.

---

Con respecto a su edición:

Supongamos que no se diera el caso de que encontrar una asignación satisfactoria a un enunciado booleano arbitrario fuera un problema exponencialmente creciente, entonces ¿necesitaríamos siquiera la vinculación sintáctica?

La semántica por asignación booleana finitaria sólo cubre el caso específico de la clásica proposicional lógica. Para este caso restringido, se es más razonable sugerir que se tome la semántica como primitiva, ya que la semántica es tan simple y finita como la sintaxis.

Sin embargo, la lógica proposicional no es lo suficientemente expresiva para hacer matemáticas serias en ella: las matemáticas requieren cuantificación. Para los sistemas con cuantificación, como la lógica de predicados de primer orden, la semántica no es finitista, por lo que razonar sobre ellos requiere una metateoría no trivial, y volvemos a la regresión anterior: una noción rigurosa de "prueba semántica" depende de que ya se tenga alguna noción rigurosa de prueba para la metateoría.

Answer 5

Otros ya han señalado que aunque se puede "salir del paso" con las tablas de verdad para verificar la verdad de una tautología en la lógica proposicional, y no se necesita un sistema deductivo llamado "sintáctico" para ello, necesitamos un sistema de prueba "sintáctico" para la lógica de primer orden (FOL), porque es imposible utilizar sólo tablas de verdad.

Me gustaría profundizar en ello. En primer lugar, hay una gran variedad de sistemas deductivos para la lógica de primer orden, pero en mi opinión sólo es necesario aprender uno de ellos para poder no sólo entender sino también reconstruir casi todos los demás, concretamente Deducción natural al estilo de Fitch para la lógica de primer orden . Obsérvese que hay muchas variantes de sistemas tipo Fitch para FOL, pero todas se basan en la idea de realizar la deducción en contextos explícitos visualmente estructurados. Para la lógica proposicional, sólo necesitamos el subcontexto if (introducido por el encabezado "If ..." en mi post). Para la FOL, sólo necesitamos eso y el subcontexto universal (introducido por el encabezado "Dado..."). Como referencia, aquí es otra variante del estilo Fitch, pero las diferencias no son importantes por ahora.

Lo importante es que para FOL, el subcontexto universal es extremadamente crucial para permitir que el sistema deductivo funcione. Una prueba de un enunciado universal, concretamente de la forma " $∀x∈S\ ( Q(x) )$ " tiene que llevarse a cabo introduciendo un subcontexto en el que se nos da " $x∈S$ " y luego dentro de ese subcontexto demostrar que " $Q(x)$ " es cierto. El hermoso es que no tenemos que razonar sobre todo miembros de $S$ sino simplemente sobre un solo dado arbitrariamente miembro $x$ de $S$ . Si podemos demostrar que tal $x$ satisface $Q$ entonces hemos demostrado efectivamente que cada miembro de $S$ satisface $Q$ porque nuestra prueba no depende de qué $x∈S$ se dio. Esta idea es capturada por la regla ∀-intro, y es crítica al permitir que un objeto sintáctico finito (una prueba) capture una noción semántica potencialmente infinita (la verdad para cada miembro de $S$ ).

Esta semántica "potencialmente infinita" es también lo que hace que imposible utilizar tablas de verdad para averiguar el valor de verdad de una frase en FOL. Resulta que ningún programa de ordenador puede determinar correctamente si una frase en FOL es o no una tautología. (Esto se llama la indecidibilidad de FOL, y una forma de demostrarlo es probar que cualquier programa de este tipo puede utilizarse para construir un programa que pueda resolver el problema de detención). Esto implica que ningún procedimiento sistemático (utilizando tablas de verdad o de otro tipo) puede determinar si una sentencia en FOL es o no una tautología. Esto hace que FOL sea muy diferente a la lógica proposicional, porque las tablas de verdad proporcionan un procedimiento sistemático para determinar si una fórmula proposicional es una tautología o no.

Por cierto, incluso para la lógica proposicional se puede argumentar que las tablas de verdad son de hecho pruebas sintácticas en disfrazarse ¡! Una "prueba" de la tabla de verdad está afirmando implícitamente que las filas mostradas representan todo casos posibles, y la evaluación del valor de verdad de la fórmula en cada fila está realizando implícitamente un análisis sintáctico de la fórmula para determinar su valor de verdad. ¿Cómo se "sabe" que no se ha omitido un caso? En observar sintácticamente que cada posible asignación de valores de verdad está en la tabla. Esto no es muy diferente de realizar una prueba al estilo de Fitch de la siguiente forma:

A∨¬A.
If A:
  ...
  B.
If ¬A:
  ...
  B.
B.

Lo mismo ocurre aquí, la única manera de saber si una prueba formal es correcta es observar sintácticamente que cada paso está permitido por las reglas deductivas. Por lo tanto, se puede decir que el método de usar tablas de verdad para la lógica proposicional es en realidad un sistema deductivo sintáctico primitivo. Simplemente aparece semántica, pero definitivamente no se trata de valores de verdad reales y sólo jugando con símbolos sintácticos para los valores de verdad, a menudo "0" y "1".