A dualidade entre verdade e falsidade, conjunção e disjunção é uma propriedade da lógica clássica. A teoria da demonstração revela não só a razão profunda desta dualidade, mas também outra dualidade de carácter mais dinâmico, que relaciona as duas soluções de um certo dilema no processo de normalização de provas formais. Ora, surpreendentemente, este dilema está relacionado com o dilema fundamental que surge na execução de programas funcionais: devo ou não devo avaliar o argumento de uma função? O seminário pretende sobretudo explicar estas relações, que são a motivação para trabalho em curso sobre as mesmas questões no caso da lógica intuicionista. Se o tempo permitir, os resultados preliminares desse trabalho serão referidos.
|