Teorías Lógicas y Máquinas de Turing

se tiene una presentación detallada de la Lógica de Primer Orden. En esta sección recordaremos los conceptos necesarios para establecer la relación de una teoría lógica en general con los Autómatas de Turing, y en general con la disciplina de Computación.

Una teoría lógica (TL) se define a partir de un conjunto de enunciados dados llamados axiomas, unas reglas de inferencia y un esquema de derivación. A partir de los axiomas y aplicando las reglas de inferencia y

el esquema de derivación se infieren los teoremas de la teoría. El conjunto de teoremas de la teoría forman un lenguaje formal.

Si es posible definir una máquina de Turing tal que reconozca al lenguaje de los teoremas, este lenguaje es decidible y la teoría también lo es en consecuencia. Dicho en otras palabras, si el conjunto de teoremas visto como un lenguaje es reconocido por una máquina de Turing, entonces la TL es decidible. Y viceversa.

Puede hablarse entonces de manera indistinta de teorías lógicas o de lenguajes decidibles, como aquellos para los que existe una máquina de Turing capaz de reconocerlos. Luego, la correspondencia entre la sintaxis de una teoría lógica (lenguaje formal) y el reconocimiento simbólico de la mismo por parte de un autómata queda establecida.

Desde el punto de vista semántico, las interpretaciones de las cadenas del lenguaje se realizan ya sea por el intérprete ó bien por el compilador del lenguaje de programación en el cual se dan las instrucciones (ver Sección de Autómatas de Pila). Las cadenas que resultan en instrucciones realizadas por la computadora pueden considerarse interpretadas como verdaderas y por tanto tienen, al menos, un modelo de la Teoría Lógica formada por tales cadenas.

En particular, los axiomas se consideran teoremas de la teoría, los cuales se derivan aplicando cero veces las reglas de inferencia