Lógica minimal, intuicionista y clásica

Abstract

The classical systems traditionally accepted within formal mathematical reasoning coexists with other branches of logic that are based on constructive aspects of deduction processes. Minimal logic and intuitionistic logic stand out from among these branches. The present study offers an analysis of these two logics, based on a series of deduction systems and varied semantics. Thus, some of their most characteristic features can be successfully proved, such as the Soundness Theorem and the Completeness Theorem. Moreover, the relationship between classic logic and these two branches of constructive logic will also be considered in order to assess whether a verifiable result in the former can also be verified by any of the two latter ones. For this purpose, Gödel-Gentzen’s negative translation will be presented together with Glivenko’s Theorem, among others.

Además de los sistemas clásicos habitualmente aceptados para el razonamiento matemático formal, existen otras ramas de la lógica que se basan en los aspectos constructivos de los procesos de deducción. Entre éstos destacan la lógica minimal y la lógica intuicionista. A lo largo de este trabajo se realiza un estudio de estas lógicas, presentando diversos cálculos deductivos y distintas semánticas que nos permiten demostrar algunas de sus propiedades ḿas importantes, como son el Teorema de Corrección y el Teorema de Completitud. Así mismo, se estudia la relación existente entre estas dos lógicas constructivas y la lógica clásica con el fin de determinar cuándo una fórmula válida en lógica clásica lo es también en lógica intuicionista o minimal. Para ello, presentamos la traducción negativa de Gödel-Gentzen y el Teorema de Glivenko, entre otros.