En terminos generales trabajamos sobre las notas de Thomas Streicher
"Introduction to Constructive Logic and Mathematics", secciones 1 al
13.

1. Introducción. Vimos diferentes pruebas no constructivas y discutimos qué aspecto
de esa prueba es el que no construye una solución del problema que
resuelve. Observamos que el carácter no constructivo está relacionado
con las pruebas de existenciales o disjunciones. Observamos que el
Principio del Tercero Excluído (PEM) y la Eliminación de Doble
Negación (DNE) se usan en las pruebas por absurdo. Semántica BHK.

2. Deducción Natural. Definimos el sistema NJ de la deducción natural
intuicionista. Propiedades del sistema desde la página 10 a la
14. Observar qué principios de dualidad se preservan en lógica
intuicionista y qué principios no.

3. Miramos muy poco al respecto de la deducción a la Hilbert. Apenas
si lo comentamos.

4. Heyting Algebras. Modelos basados en Heyting
Algebras. Soundness. Usamos estos modelos para probar el Teo 4.2.

5. Inmersión de la Lógica Clásica en la Intuicionista. A esto le
dedicamos tiempo y lo vimos con detalle. Lo central es entender por
qué Gödel-Gentzen lleva a la lógica clásica en un fragmento
de la lógica intuicionista. 

6. Aritmética constructiva y análisis. Entender con precisión las
definiciones 6.1 y 6.2 es crucial. Luego trabajamos sobre la
traducción de Friedmann y luego lo usamos para probar que PA es
conservativa sobre HA para fórmulas sigma1 (Teorema 6.1). Luego
trabajamos también con detalle lo relativo al Análisis Elemental
EL. Entender con precisión la Definición 6.4 y qué es lo que permite
expresar el lenguaje es crucial. La discusión sobre la diferencia
entre CRA y BIM es importante para las secciones siguientes.

7. Números reales constructivos. Entender las definiciones 71. y 7.2
es crucial. Tener presente que la teoría de los racionales se codifica
en la aritmética y que en la aritmética las ecuaciones son
decidibles. Eso permite probar por ejemplo la tricotomía en N, Z y
Q. Los lemas 7.1 y 7.2 son técnicos y su objetivo es llegar a probar
el Corolario 7.1 y el Lema 7.3. Observen que las ecuaciones de reales
admiten DNE pero no PEM y por lo tanto no son decidibles y en
consecuencia la tricotomía tampoco vale en general (no es un teorema
del analisis constructivo).

8. Teoría de la recursión en HA. Los Teoremas 8.1, 8.2, la Convención 8.1
y toda la discusión sobre cómo codificar secuencias finitas y sus
operaciones son cosas básicas de Teoría de la Recursión de las que nos servimos
acá. Es importante entender lo que dicen. El Teorema 8.3 es
interesante porque lo usamos para probar que el Lema de König es
inconsistente con la Tesis de Church (ver sección 11).

9. Realizabilidad de Kleene. Aca todo se trabajó con sumo detalle. La
pieza central que hay que poder entender y explicar es el Teorema 9.2
y todo lo necesario para probarlo. Lemma 9.1, Corolario 9.1 y Lema 9.2
tienen un cierto nivel técnico, pero es importante comprenderlo porque
es donde se ve la definición de la realizabilidad en acción. Lo
crucial del Teorema 9.2 es que la teoría de la Realizabilidad de
Kleene es axiomatizable agregándole a HA el ECT_0.  

Luego pasamos a la "realizabilidad combinada con verdad" y el Teorema
9.3 muestra otro punto de vista, que es definir una Realizabilidad que
en HA equivale exactamente a la teoría de HA. Comparar entonces con
el Teorema 9.2. Por último, el Teorema 9.4 da una prueba de
realizabilidad de la propiedad de la disjunción y del existencial para
HA.

10. El principio de Markov. Acá también se trabajó de manera
detallada. Hay dos resultados centrales. Uno es el Teorema 10.1, que
debe ser entendido en relación con el Teorema 9.2 y el 9.3. Se da una
presentación axiomática de la Realizabilidad de Kleene bajo HA+MP.

11. Realizabilidad de Kleene en Análisis Elemental. Es importante
entender aquí que las secuencias de naturales se usan para codificar
funcionales y funciones reales. El aspirar a que estas funciones
reales y estos funcionales sean totales lleva a trabajar en la
Topología de Baire en las sucesiones y se observa que las funciones
reales y los funcionales codificados son los continuos con esta
topología. El Teorema 11.1 es un resultado técnico que esencialmente
dice que se puede hacer recursión en el tipo 2 de las secuencias de
naturales. Luego vimos la Def 11.1 y la discusión sobre los diferentes
niveles del Axioma de Elección (AC) en el análisis elemental y
terminamos con el Teorema 11.2.

12. La definición de HA^\omega se vió con detalle, así como se
discutió la diferencia entre IHA^\omega y EHA^\omega. Visitamos
rápidamente los modelos de la subsección 12.2.

13. Definimos el lenguaje de realizadores y la Realizabilidad
Modificada de Kreisel. De nuevo, el Teorema 13.2 es una pieza central
que ha de ser comparada con los previamente vistos acerca de la
axiomatización de otras realizabilidades. Observar que el "programa"
que se sigue es muy similar y está detallado en Lema 13.1 y Corolario
13.1. El otro objetivo importante es probar que HA^\omega no prueba
MP. La prueba del Teorema 13.3 la estudiamos en detalle, excepto por
un claim que deja el autor al final. Dimos en detalle una prueba
alternativa de la independencia del MP siguiendo la sugerencia que
viene a continuación (ver notas de clase del 12 de mayo).