Una teoría recursivamente enumerable sin un conjunto decidible de axiomas.

Question

Una teoría es un conjunto de sentencias de primer orden sobre alguna firma. Un conjunto de sentencias se llaman axiomas para la teoría, si el cierre deductivo de los axiomas es igual a la teoría.

Ahora bien, si tengo un conjunto de axiomas recursivamente enumerable, entonces la teoría es recursivamente enumerable. Por ejemplo, podríamos enumerar hasta el $i$ -a axioma, calcular todas las deducciones de longitud $i$ y luego continuar con $i+1$ .

¿Conoce un ejemplo de una teoría recursivamente enumerable que no tenga un conjunto decidible de axiomas?

Answer 1

Como señaló Carl Mummert en los comentarios, Teorema de Craig dice que esto es imposible. Toda teoría de la e.r. tiene una axiomatización decidible (o incluso recursiva primitiva).

Esto no es especialmente profundo: Si tienes una máquina que acepta los axiomas de la teoría, basta con sustituir cada axioma $\phi$ con $$\phi\land (\underbrace{(x=x)\lor (x=x) \lor \cdots \lor (x=x)}_n ) $$ donde $n$ es exactamente el número de pasos que la máquina tarda en aceptar $\phi$ . Entonces, si se está ante uno de estos nuevos axiomas se puede decidir simplemente contando el número de $(x=x)$ disyuntivas a la derecha y ejecutando el aceptor durante tantos pasos en la fórmula a la izquierda de $\land$ .