Introdução ao cálculo de sequentes de Gentzen

Abstract

O cálculo de sequentes, desenvolvido por Gentzen no início do século, é uma ferramenta essencial na lógica matemática, usada para demonstrar a validade de argumentos ao resolver o desafio de verificar se uma fórmula segue logicamente de um conjunto de premissas. Isso é facilitado pelo uso de regras formais. Uma de suas maiores conquistas é o Teorema da Eliminação do Corte. Ao evitar a introdução arbitrária de cortes nas deduções, asseguramos que todas as provas válidas possam ser construídas sistematicamente, e nenhum argumento válido escape à nossa análise. Este trabalho se concentra em examinar o cálculo de sequentes de Gentzen, incluindo seus princípios fundamentais, regras de inferência e na introdução breve do Teorema da Eliminação do Corte, juntamente com suas implicações práticas e teóricas.