4 votos

¿Hay una teoría decidible en lógica proposicional, cuyas consecuencias no son decidibles?

Quiero saber si hay una teoría decidible en lógica proposicional, cuyas consecuencias no son decidibles.

¿Si hay, podemos tener un ejemplo constructivo o sólo podemos probar la existencia de la misma?

Si no, ¿cómo puedo demostrar?

5voto

JoshL Puntos 290

Sí, existen, pero sólo cuando tenemos acceso a un conjunto infinito de variables proposicionales.

En ese caso, deje que las variables se $\{p_n : n \in \mathbb{N}\}$ y deje $f$ ser cualquier función computable. Definir una teoría de la $T$ tal que, para cada $x$, $T$ contiene el axioma $p_y\land p_y \land \cdots \land p_y$, donde se $x$ conjuntos y $y = f(x)$. A continuación, $T$ es decidable; para saber si una fórmula es un axioma de la $T$, pregunte si es una conjunción de alguna variable $p_m$ con algunas de número de $n$ veces y, a continuación, preguntar si $f(n) = m$; la fórmula es en $T$ si y sólo si ambas preguntas son "Sí". Pero, dado $y$, $T$ ha $p_y$ como consecuencia, si y sólo si $y$ está en el rango de $f$, así que si podemos decidir las consecuencias de $T$ entonces podemos decidir el rango de $f$. Porque hay funciones computables cuyo rango no es computable, esto le da a la deseada ejemplo.

Si sólo hay $n$ variables, a continuación, sólo hay $2^{2^n}$ fórmulas posibles hasta lógica de la equivalencia, porque cada fórmula está determinada únicamente hasta equivalencia por el conjunto de filas de la tabla de verdad de $n$ variables que hacen que la fórmula de la verdad, y hay $2^n$ filas. De este modo podemos hacer un programa en el que nos codificar una tabla que muestra si $T$ implica que cada una de estas clases de equivalencia. Dada una fórmula, acabamos de calcular qué clase de equivalencia es en y, a continuación, busque en la tabla para ver si $T$ implica que la clase.

i-Ciencias.com

I-Ciencias es una comunidad de estudiantes y amantes de la ciencia en la que puedes resolver tus problemas y dudas.
Puedes consultar las preguntas de otros usuarios, hacer tus propias preguntas o resolver las de los demás.

Powered by:

X