Ambigüedad y Lógica

En la teoría de los autómatas (autómatas finitos, autómatas pushdown, ...) y en la complejidad, existe una noción de "ambigüedad". Un autómata es ambiguo si hay una palabra $w$ con al menos dos ejecuciones de aceptación distintas. Una máquina es $k$ ambigua si por cada palabra $w$ aceptada por la máquina hay a lo sumo $k$ ejecuciones distintas para aceptar $w$ .

Esta noción también se define sobre gramáticas libres de contexto: una gramática es ambigua si existe una palabra que se pueda derivar de dos maneras diferentes.

También se sabe que muchos idiomas tienen una buena caracterización lógica sobre modelos finitos. (Si un lenguaje $L$ es regular, existe una fórmula monádica de segundo orden $\phi$ sobre las palabras de modo que cada palabra $w$ de $L$ sea ​​un modelo de $\phi$ , de manera similar NP si es equivalente a las fórmulas de segundo orden donde cada cuantificador de segundo orden es existencial).

Por lo tanto, mi pregunta está en los bordes de los dos dominios: ¿hay algún resultado, o incluso una definición canónica, de "ambigüedad" de las fórmulas de una lógica dada?

Puedo imaginar algunas definiciones:

• $\exists x \phi(x)$ es no ambigua si existe como máximo un$x$ tal que$\phi(x)$ sostiene y que$\phi(x)$ es no ambigua.
• $\phi_0\lor\phi_1$ sería ambiguo si existe un modelo de$\phi_0$ y$\phi_1$ , o si$\phi_i$ es ambiguo.
• Una fórmula SAT no sería ambigua si hubiera, como máximo, una asignación correcta.

Por lo tanto, me pregunto si es una noción bien conocida, de lo contrario, puede ser interesante intentar investigar sobre este tema. Si se conoce la noción, ¿alguien podría darme palabras clave que podría usar para buscar información sobre el tema (porque la "ambigüedad lógica" da muchos resultados no relacionados), o un libro / pdf / referencias de artículos?

Las reglas en una gramática y las reglas de inferencia en lógica pueden considerarse como reglas de producción que nos dan "cosas nuevas" de "cosas conocidas". Así como puede haber muchas formas de producir (o analizar) una palabra con respecto a una gramática, también puede haber muchas formas de producir (o probar) una fórmula lógica. Esta analogía se puede extraer más. Por ejemplo, ciertos sistemas lógicos admiten formas normales de pruebas. Del mismo modo, ciertas gramáticas admiten árboles de análisis canónicos.

Entonces diría que sus ejemplos de lógica van en la dirección incorrecta. La analogía correcta es

"parse tree": "word" = "proof": "fórmula lógica"

De hecho, un tipo de gramática suficientemente general será capaz de expresar reglas de inferencia típicas de la lógica, de modo que las palabras gramaticalmente correctas serán precisamente las fórmulas comprobables. En este caso los árboles de análisis serán en realidad ser las pruebas.

En la dirección opuesta, si estamos dispuestos a pensar en reglas de inferencia muy generales (que no necesariamente tienen un sabor lógico tradicional), entonces cada gramática se podrá expresar como un sistema de axiomas (terminales) y reglas de inferencia (producciones). Y una vez más, veremos que una prueba es lo mismo que un árbol de análisis.

Solo dos comentarios. Espero que te ayuden.

Las definiciones estándar de semántica de una lógica y de verdad siguen la presentación de Tarski, procediendo por inducción en la estructura de la fórmula. Otra posibilidad es dar una semántica basada en el juego como lo sugiere Hintikka. La verdad y la satisfacción se definen en términos de estrategias en un juego. Para las fórmulas de primer orden, se puede demostrar que una fórmula es verdadera según la noción de Tarski si y solo si existe una estrategia ganadora en el juego Hintikka.

Para formalizar su pregunta, uno puede preguntar si el juego admite múltiples estrategias. También está la interesante pregunta sobre si las estrategias deberían ser deterministas. Hintikka requería que fueran deterministas. La prueba de que la semántica original de Hintikka y la semántica de Tarski son equivalentes requiere el Axioma de Elección. También se puede formalizar la verdad en términos de juegos con estrategias no deterministas con menos complicaciones.

Su ejemplo de teoría del lenguaje le trajo a la mente el determinismo, las relaciones de simulación y la aceptación del lenguaje. Una relación de simulación entre autómatas implica la inclusión del lenguaje entre sus idiomas, aunque lo contrario no es cierto. Para autómatas deterministas las dos nociones coinciden. Uno puede preguntarse si es posible extender las relaciones de simulación de una manera 'uniforme' para capturar la equivalencia del lenguaje para autómatas no deterministas. Kousha Etessami tiene un muy buen artículo que muestra cómo hacer esto usando simulaciones k ( Una jerarquía de simulaciones computables en tiempo polinómico para autómatas) Intuitivamente, la 'k' refleja el grado de no determinismo que la relación de simulación puede capturar. Cuando 'k' es igual al nivel de no determinismo en el autómata, la simulación y la equivalencia del lenguaje coinciden. Ese documento también ofrece una caracterización lógica de las simulaciones k en términos de lógica modal poliádica y un fragmento variable limitado de lógica de primer orden. Obtiene inclusión de lenguaje, determinismo, juegos, lógica modal y lógica de primer orden, todo en un paquete de parachoques.

Esto comenzó como un comentario bajo la respuesta de Andrej Bauer, pero se hizo demasiado grande.

Creo que una definición obvia de ambigüedad desde el punto de vista de la Teoría del Modelo Finito sería: $ambiguous(\phi) \implies \exists M_1,M_2 | M_1 \vDash \phi \wedge M_2 \vDash \phi \wedge M_1 \vDash \psi \wedge M_2 \nvDash \psi$

En palabras, existen distintos modelos de su gramática codificada como una fórmula que puede distinguirse por alguna fórmula ψ , tal vez una sub-fórmula de ϕ .$\phi$$\psi$$\phi$

Puede conectar esto con la respuesta de Andrej sobre las pruebas a través de la complejidad descriptiva. La combinación de la existencia de una codificación de un modelo particular más su aceptación por un TM apropiado como modelo de una fórmula dada ES una prueba de que los axiomas e inferencias (y, por lo tanto, una gramática equivalente) codificada en esa fórmula son consistentes.

Para que esto sea totalmente compatible con la respuesta de Andrej, tendría que decir que el modelo es "generado" por la fórmula que actúa como un filtro en el espacio de todos los modelos finitos posibles (o algo así), con la codificación y la acción de filtrado en el modelo de entrada como la "prueba". Las pruebas distintas son testigos de la ambigüedad.

Puede que este no sea un sentimiento popular, pero tiendo a pensar que la teoría de modelos finitos y la teoría de pruebas son lo mismo visto desde diferentes ángulos. ;-)

No estoy seguro acerca de la pregunta aplicada a CS, pero intente buscar el término Vagueness y lógica. En filosofía de la lógica, la ambigüedad generalmente se distingue de la vaguedad (ver aquí, por ejemplo), y creo que lo que busca es la vaguedad (ya que la vaguedad se define como términos donde hay casos límite). El libro principal en esta área es La vaguedad de Timothy Williamson (pero también vea la bibliografía en el sitio de Stanford arriba).

Estoy (también) de acuerdo con Anrej.

Creo que la complejidad descriptiva es una caracterización sin cómputo (lo que lo hace interesante a su manera) y, por lo tanto, los ejemplos de ambigüedad computacional de la teoría de los lenguajes formales (autómatas / gramáticas / ...) que consideró que estaban en un dominio bastante diferente . En la complejidad descriptiva, los lenguajes corresponden a clases de complejidad y las consultas (en un lenguaje) corresponden a problemas computacionales (no algoritmos). No hay una forma prevista de verificar / calcular una consulta AFAIK, por lo que si no está buscando ambigüedad computacional, en mi humilde opinión, esos ejemplos son engañosos.