Decision problems and recursiveness in formal logic systems

ResumenEn la teoría de la recursión se dice que un problema de decisión es recursivamente resoluble si existe un procedimiento mecánico para resolverlo. Dentro del contexto de las lógicas formales, el problema de decisión consiste simplemente en determinar si una fórmula bien formada cualquiera del sistema es, o no es, un teorema.En este trabajo se analizan, entre otros asuntos, primeramente el famoso problema de decisión de la lógica canónica de primer orden F0 (también llamado Entscheidungsproblem) desde una perspectiva moderna. Luego se estudian los problemas de decisión de las lógicas proposicionales parciales. Se aprovecha el desarrollo alcanzado por la teoría de la recursión y de los sistemas productivos semi-Thue, luego de los trabajos de Post y Kleene en los años 40's y de Davis en la década de los 70's, entre otros, para explicar una solución a estos problemas de decisión. AbstractThe recursion theory states that a decision problem is recursively solvable if there is a mechanical process to solve it. Within the context of formal logic, the decision problem consist to determine whether any wellformed formula of the system is a theorem or not.This paper first discusses, among other things, the famous problem of decision of the canonical first-order logic F0 (also called Entscheidungsproblem) from a modern perspective. Then we study the decision problem of the partial propositional logics. It exploits the development achieved by recursion theory and semi-Thue production systems after the work of Post and Kleene in the 40's and Davis in the early 70's, among others, to explain a solution to these decision problems.