Programas moleculares y sistemas lógico-formales

Abstract

Presentamos una ejemplificación de la relación entre sistemas formales y programas moleculares de un modelo de computación molecular. Para ello, se asocia un sistema lógico-formal, mediante una lógica pura de segundo orden, a cada programa molecular que resuelve un problema de decisión y se justifica que la verificación form al de dicho programa (respecto del problema en cuestión) equivale a establecer la adecuación, o corrección, y la completitud del sistema formal asociado. En un primer apartado introducimos la lógica de segundo orden, teniendo en cuenta la tradicional distinción entre semántica estándar y semántica de Henkin ; se estudia un sistema lógico- formal de segundo orden cuyo lenguaje no tiene variables individuales ni funcionales, se esboza un cálculo deductivo y se establecen su adecuación y su completitud. Sigue un apartado dedicado a introducir una sencilla explicación de qué son los programas moleculares; se da una formalización de un programa molecular y se asocia a éste un sistema lógico- formal basado en la lógica de segundo orden estudiada. En el último apartado se caracteriza la verificación formal de programas moleculares en términos de las propiedades metateóricas del sistema lógico-formal asociado. Concluimos con unas breves consideraciones finales y una bibliografía básica.