Polimorfismo atómico e o teorema de normalização forte
A teoria da demonstração é um dos quatro pilares da Lógica Matemática e tem como principal objetivo estudar e compreender a estrutura das provas matemáticas através da sua representação em sistemas formais. Os sistemas dedutivos formais permitem a utilização de técnicas matemáticas na análise das demonstrações. Um dos sistemas formais mais usados, com semelhanças claras com o processo de raciocínio humano, é o sistema de Dedução Natural.
O Cálculo de Dedução Natural relaciona-se, através do isomorfismo de Curry-Howard, com um outro sistema formal muito útil na área da ciência da computação, o cálculo lambda.
A dicotomia dedutivo/operacional do cálculo é usada no estudo de dois sistemas: F e Fat.
O sistema Fat consiste na restrição do bem conhecido sistema F a instanciações universais atómicas. Apesar da restrição, Fat é ainda suficientemente expressivo para interpretar o cálculo proposicional intuicionista.
Certos resultados, no contexto de Fat, admitem estratégias de demonstração mais simples do que no contexto impredicativo de F. Esta simplificação está patente na demonstração do teorema da normalização forte que é apresentada nesta dissertação de mestrado.
Estudante do MEMeC, Universidade Aberta
Universidade Aberta e CMAF-UL