Resumo:
Na monografia de 1965 que fundou o estudo da dedução natural, Prawitz considera adequado omitir as operações de disjunção e quantificação existencial no tratamento da lógica clássica. O argumento é o de que nenhum teorema é perdido com essa omissão, ou seja, a demonstrabilidade clássica reduz-se à demonstrabilidade no sistema com as referidas operações omitidas. Porém, como foi observado entretanto, não é claro que haja uma redução semelhante para propriedades como a normalização. Ora, foi justamente o trabalho de Prawitz que mostrou o elevado interesse dessas propriedades, pelo que se pode considerar incompleto o tratamento da lógica clássica na monografia de Prawitz. Neste seminário, iremos mostrar como fazer uma tal redução para a propriedade da normalização forte. O sistema dedutivo será tratado como um sistema de tipos para o cálculo-lambda de Rehof-Sorensen 1994. |