Um estudo sobre a normalização de provas em dedução natural no fragmento proposicional

Abstract

O sistema de dedução natural proposto por Gentzen foi um dos principais avanços na formalização matemática proposta inicialmente por Hilbert e seu sistema axiomático. A criação desse sistema foi um dos primeiros passos para o estudo das deduções como um objeto da matemática, criando uma mudança de paradigma que permitiu o desenvolvimento da teoria de prova moderna. Prawitz, com seu estudo das normalizações de provas, foi capaz de provar características importantes sobre esse sistema, como sua consistência, atráves da análise da complexidade das provas, definida por ele como sendo a quantidade de "desvios" contidos numa derivação. Um estudo dos trabalhos desses dois matemáticos é aqui apresentada de forma intuitiva, menos rigorosa, com o objetivo de criar um material introdutório ao tema para a leitura de alunos de gradução iniciando seus aprendizados de lógica.