Cálculo de Dedução Natural - bons e maus conectivos

O Cálculo de Dedução Natural, introduzido por Gerhard Gentzen em 1935 pretendendo aproximar-se o mais possível do modo de raciocínio humano, é ainda hoje um dos sistemas formais dedutivos mais conhecidos e estudados. Neste seminário propomo-nos introduzir, de modo sucinto, o Cálculo de Dedução Natural e apresentar trabalho recente nesta área realizado em conjunto com Fernando Ferreira. Mais especificamente, e na sequência de ser notório o facto de alguns conectivos (\bot, \vee, \exists) estarem associados a regras de eliminação de mais difícil tratamento, mostraremos uma forma de evitar esses "maus" conectivos quando lidamos com o cálculo intuicionista de predicados. Como consequência, pensamos ter obtido uma explicação bastante natural para um tipo de transformações tradicionalmente introduzidas de modo ad hoc: as "commuting conversions".