logica

Notas de L´gica Matem´tica
o
a
Hector Luis Gramaglia

1

Introducci´n
o

En este breve apunte vamos a abordar algunos t´picos importantes de L´gica Matem´tica, la cual
o
o
a
se ocupa del estudio del lenguaje y los m´todos de razonamiento de la matem´tica utilizando como
e
a
herramienta la misma matem´tica. Nos vamos a concentrar en una formalizaci´n de la noci´n de
a
o
odemostraci´n conocida como deducci´n natural de Gentzen-Prawitz. Existen numerosas formalo
o
izaciones de esta noci´n que poseen todas ellas virtudes diferentes. Algunas tienen como objetivo
o
modelar la actividad del matem´tico, y permiten emprender de manera sencilla la construcci´n
a
o
formal del edificio matem´tico. Las formalizaciones de este tipo suelen ser bastante extensas ya que
atartan de incorporar en forma de ”reglas” todos los recursos de los cuales dispone un matem´tico
a
en su trabajo cotidiano. La deducci´n natural de Gentzen-Prawitz no se encuentra dentro de
o
este grupo. De hecho una prueba tiene forma de ”´rbol”, en el cual el n´mero de hojas depende
a
u
exponencialmente de la altura, de manera que la prueba de los resultados m´s elementales de la
aaritm´tica requerir´ de un ancho de hoja dif´ de encontrar. La virtud de este sistema es sin
e
ıan
ıcil
duda su simpleza, que permite abordar el estudio de ciertas propiedades sint´cticas (eliminaci´n
a
o
de cortes, normalizaci´n, etc.) de una manera adecuada. Por otro lado este sistema nos permite
o
”llevar en paralelo” el estudio de cuestiones relativas a las l´gicas cl´sica e intuicionista,debido a
o
a
que la incorporaci´n de una una sola regla, la reducci´n al absurdo, permite extender la noci´n
o
o
o
de prueba intuicionista al contexto cl´sico.
a
El ”hilo conductor” del apunte es la secuencia: ”noci´n de prueba - sem´ntica - correcci´n y
o
a
o
completitud”. Esta secuencia ser´ respetada para las l´gicas proposicionales cl´sica e intuicionista.
a
o
a
Para el casointuicionista se introduce la sem´ntica de Kripke, que extiende la sem´ntica cl´sica
a
a
a
dada por las tablas de verdad. Se posterga para el final del apunte la extensi´n del sistema a los
o
cuantificadores. Se remite al lector a los ap´ndices para abordar algunas cuestiones de inter´s, de
e
e
manera de no distraer el desarrollo de los t´picos fundamentales. Los temas de mayor complejidad
oson sin duda las nociones de estructuras algebraicas (Secci´n 7) que nos permiten obtener las
o
pruebas de completitud.
El unico prerequisito para la lectura de este material es un curso b´sico de ´lgebra, en el
´
a
a
cual asumimos que el lector tomo contacto con las nociones de f´rmula proposicional y tablas de
o
verdad. Por cuestiones de espacio, no pondremos demasiado enf´sis en lasdefiniciones formales de
a
los lenguajes de las respectivas l´gicas. Todos los temas, inclusive este ultimo, son acompa˜ado con
o
´
n
referencias bibliogr´ficas para que el lector interesado pueda ampliar los contenidos aqu´
a
ıvertidos.

1

2

Contenidos
1.
2.
3.
4.
5.
6.
7.
8.

Introducci´n.
o
Contenidos
Deducci´n Natural de Gentzen-Prawitz.
o
Algunas propiedadessint´cticas relevantes.
a
Deducci´n Natural para la l´gica cl´sica.
o
o
a
Sem´ntica de Kripke.
a
Correcci´n y Completitud.
o
Los cuantificadores.

Referencias.
Ap´ndice 1: El c´lculo lambda y el isomorfismo de Curry-Howard.
e
a
1. La interpretaci´n de Brower-Heyting y Kolmogorov.
o
2. El c´lculo lambda tipado.
a
3. El isomorfismo de de Curry-Howard.
Ap´ndice 2: Prueba del lema 13.
eAp´ndice 3: C´lculo de Secuentes de Gentzen.
e
a

2

3

Deducci´n Natural de Gentzen-Prawitz
o

En esta secci´n vamos a introducir el sistema de deducci´n natural propuesto por Gentzen, cuyo
o
o
estudio sistem´tico fue realizado por Prawitz en [10]. Este sistema, originalmente pensado para la
a
l´gica intuicionista, se extiende tambi´n a la l´gica cl´sica, perdiendo en esta...