Teorema de Craig

Na lógica matemática , o teorema de Craig afirma que qualquer conjunto recursivamente enumerável de fórmulas bem formadas de uma linguagem de primeira ordem é (primitivamente) recursivamente axiomatizável. Este resultado não está relacionado com o bem conhecido teorema de interpolação de Craig.

Axiomatização recursiva

Seja $A_{1},A_{2},\dots$ uma enumeração dos axiomas recursivamente enumerável de T conjunto de fórmulas de primeira ordem. Construa um outro * T conjunto que consiste em :$\underbrace {A_{i}\land \dots \land A_{i}} _{i}$ para cada inteiro positivo i. Os fechos dedutivos de T * e T são, portanto, equivalente, a prova irá mostrar que T * é um conjunto decidível. Um procedimento de decisão para * T presta-se de acordo com o seguinte raciocínio informal. Cada membro de T * é ou ou da forma

$\underbrace {B_{j}\land \dots \land B_{j}} _{j}.$

Uma vez que cada fórmula tem comprimento finito, é verificável se é ou não é ou do referido da forma.

$\underbrace {B_{j}\land \dots \land B_{j}} _{j}.$

Se é da forma dito e consiste de conjuntos de j, é em T * se que é a expressão , Caso contrário ele não estiver em T *. Novamente, é verificável se é, de fato, indo através da enumeração dos axiomas de T e em seguida, verificando-símbolo para o símbolo-se as expressões são idênticas.

Axiomatizações recursivas primitivas

A prova acima mostra que para cada conjunto recursivamente enumerável de axiomas há um conjunto recursivo de axiomas, com o encerramento mesmo dedutivo. Um conjunto de axiomas é recursivo primitivo se existe uma função primitiva recursiva que decide a adesão do conjunto. Para obter uma aximatização primitiva recursiva, em vez da substituição de uma fórmula com

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

uma vez substitui-lo com

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

em que f (x) é uma função que, dado i, retorna uma história de computação mostrando que está no conjunto original recursivamente enumerável de axiomas. É possível para uma função recursiva primitiva para analisar a expressão de forma (*) para se obter e j. Em seguida, porque predicado T Kleene é primitiva recursiva, é possível para uma função recursiva primitiva para verificar que j é de facto uma história de computação, conforme necessário.

Referências

William Craig. On Axiomatizability Within a System, The Journal of Symbolic Logic, Vol. 18, No. 1 (1953), pp. 30-32.