Plano de Estudos

Teoria da Demonstração TDem

Contextos

ECTS

6.0 (para cálculo da média)

Objectivos

Introduzir o aluno doutoral à teoria da demonstração e às suas técnicas principais, tendo em conta uma possível dissertação que se apoie nesta temática. Pretende-se que a cadeira seja também interessante para o não especialista em lógica matemática (p.ex., para o estudante em ciência da computação teórica ou o estudante interessado em matemática construtiva). Por isso, a disciplina não deve focar tópicos demasiado especializados (estes tópicos devem ser deixados ao aluno especialmente motivado).

Programa

Sugerem-se três tópicos principais, abordando-se pelo menos dois deles. Esta sugestão pode não ser seguida caso se decida focar profundamente num só tópico (apenas recomendável caso o curso tenha somente estudantes de lógica) ou se decida incluir um novo tópico. Para cada tópico escolhido, sugere-se fortemente a discussão de, pelo menos, o seguinte: (1) Lógica intuicionista. Sistemas de dedução natural. Deduções normais e normalização. O cálculo lambda tipado e a correspondência de Curry-Howard. Modelos de Kripke. Relações com a lógica clássica: traduções negativas. Aritmética de Peano e aritmética de Heyting. (2) Sistemas de aritmética de tipos finitos. A realizabilidade modificada de Kreisel. Majoração e a regra FAN. A interpretação funcional de Gödel. A conservação do lema fraco de König. (3) Teorema de eliminação do corte em lógica clássica. O cálculo de Tait estendido a sistemas semi-formais da aritmética. A computação do ordinal da aritmética de Peano.

Método de Avaliação

Exposição teórica.Trabalhos para casa dados durante a aula teórica. Possível discussão oral.

Carga Horária

Bibliografia

Principal

• Constructivism in Mathematics, vol. I, A. S. Troelstra e D. van Dalen. North-Holland, Amsterdam (1988). Troelstra, A.S. & Schwichtenberg, H.: Basic Proof Theory, Cambridge University Press, 2000. Ferreira, F. & Ferreira, G.: "Atomic Polymorphism", The Journal of Symbolic Logic 78, pp. 260-274 (2013) Ferreira, F.: "Proof interpretations and majorizability". Em Logic Colloquium'07, Françoise Delon et al. org., Cambridge University Press 2010, pp. 32-81. In http://www.ciul.ul.pt/~ferferr/proof_interpretations.pdf. Avigad, J. & Feferman, S.: "Gödel's functional ('Dialectica') interpretation". Em Handbook of Proof Theory, pp. 337-405, organizado por S. Buss, Elsevier, 1998. Applied Proof Theory, U. Kohlenbach. Springer (2008).:

Secundária

Disciplinas de Execução

2015/2016 - 1 Semestre