Teorema de Craig

En lógica matemática , el teorema de Craig (también conocido como el truco de Craig ) establece que cualquier conjunto recursivamente enumerable de fórmulas bien formadas de un lenguaje de primer orden es recursivamente axiomatizable , e incluso primitivamente recursivamente axiomatizable, e incluso decidible en tiempo polinomial .

Este resultado no está relacionado con el conocido teorema de interpolación de Craig , aunque ambos resultados llevan el nombre del mismo lógico, William Craig .

Sea una enumeración de los axiomas de un conjunto recursivamente enumerable de fórmulas de primer orden. Construya otro conjunto que consista en ${\displaystyle A_{1},A_{2},\dots }$${\displaystyle T}$${\displaystyle T^{*}}$

${\displaystyle \underbrace {A_{i}\land \dots \land A_{i}} _{i}}$

para cada entero positivo . Es decir, ${\displaystyle i}$

${\displaystyle T^{*}=\{A_{1},A_{2}\land A_{2},A_{3}\land A_{3}\land A_{3},\ldots \}}$

Los cierres deductivos de y son, por lo tanto, equivalentes; la demostración mostrará que es un conjunto recursivo/decidible. ${\displaystyle T^{*}}$${\displaystyle T}$${\displaystyle T^{*}}$

Dada cualquier fórmula , sea su longitud . Entonces, para decidir , basta con ejecutar primero el algoritmo de enumeración hasta que se muestren todas , y luego comprobar si es igual a una de${\displaystyle X}$${\displaystyle |X|}$${\displaystyle X\in T^{*}}$${\displaystyle A_{1},A_{2},\dots ,A_{|X|}}$${\displaystyle X}$$${\displaystyle A_{1},A_{2}\land A_{2},\dots ,\underbrace {A_{|X|}\land \dots \land A_{|X|}} _{|X|}.}$$

Un conjunto de axiomas es recursivo primitivo si existe una función recursiva primitiva que decide la pertenencia al conjunto. El algoritmo presentado anteriormente es recursivo, pero no necesariamente recursivo primitivo. El problema principal es que, en la parte donde "ejecutamos el algoritmo de enumeración hasta que se generen todos los resultados", el algoritmo de enumeración puede tardar mucho tiempo en generar todos los resultados . ${\displaystyle A_{1},A_{2},\dots ,A_{|X|}}$${\displaystyle A_{1},A_{2},\dots ,A_{|X|}}$

En la recursión primitiva, todos los bucles deben estar limitados por un límite superior precalculado. Por lo tanto, no podemos decir "ejecutar el algoritmo de enumeración hasta que...". Sin embargo, podemos decir "ejecutar el algoritmo de enumeración hasta k pasos", siempre que sepamos cuál debe ser k .

Ahora, en lugar de reemplazar una fórmula con ${\displaystyle A_{i}}$

${\displaystyle \underbrace {A_{i}\land \dots \land A_{i}} _{i}}$

uno lo reemplaza con

${\displaystyle \underbrace {A_{i}\land \dots \land A_{i}} _{f(i)}}$(*)

donde es una función que, dado , devuelve el número de pasos que la máquina de Turing de enumeración realiza para generar . De hecho, esta construcción proporciona un algoritmo de decisión que se ejecuta en tiempo polinomial , que es una clase particularmente bien comportada de funciones recursivas primitivas. ${\displaystyle f}$${\displaystyle i}$${\displaystyle A_{i}}$

The theorem has been used in proofs of Gödel's incompleteness theorems. One would first prove the theorems for all theories that with a set of axioms that is primitive recursive, then apply Craig's theorem to immediately conclude that the theorems hold for all theories with a set of axioms that is recursively enumerable.^[1]

If ${\displaystyle T}$ is a recursively axiomatizable theory and we divide its predicate symbols into two disjoint sets${\displaystyle V_{A}}$ and ${\displaystyle V_{B}}$, then those theorems of ${\displaystyle T}$ that are in the vocabulary ${\displaystyle V_{A}}$ are recursively enumerable, and hence, based on Craig's theorem, axiomatizable. Carl G. Hempel argued based on this that since all science's predictions are in the vocabulary of observation terms, the theoretical vocabulary of science is in principle eliminable. He himself raised two objections to this argument: 1) the new axioms of science are practically unmanageable, and 2) science uses inductive reasoning and eliminating theoretical terms may alter the inductive relations between observational sentences. Hilary Putnam argues that this argument is based on a misconception that the sole aim of science is successful prediction. He proposes that the main reason we need theoretical terms is that we wish to talk about theoretical entities (such as viruses, radio stars, and elementary particles).

• Hempel, C. G. (1963). "Implications of Carnap's Work for the Philosophy of Science". In Schilpp, P. A. (ed.). The Philosophy of Rudolf Carnap. La Salle, Illinois: Open Court. pp. 685–709.

• Craig, William (1953). "On Axiomatizability Within a System". The Journal of Symbolic Logic. 18 (1): 30–32. doi:10.2307/2266324.

• Putnam, Hilary (1965). "Craig's Theorem". The Journal of Philosophy. 62 (10): 251–260. doi:10.2307/2023298.