Dedução Natural e Cálculo de Sequentes

A dedução natural e o cálculo de sequentes são os dois sistemas formais do tipo Gentzen que representam provas através de regras de introdução e eliminação para os conectivos lógicos, formando o maquinário básico da teoria da prova estrutural.

Definition

A dedução natural deriva fórmulas a partir de suposições usando regras de introdução e eliminação que espelham o raciocínio informal, enquanto o cálculo de sequentes manipula sequentes, asserções de que uma lista de fórmulas implica outra, através de regras que atuam à esquerda e à direita de uma implicação.

Scope

Este tópico abrange as regras da dedução natural com seus pares de introdução e eliminação, a estrutura do cálculo de sequentes com suas regras à esquerda e à direita e regras estruturais, a normalização para a dedução natural, a relação entre os dois sistemas e suas variantes intuicionistas e clássicas.

Core questions

• Como as regras de introdução e eliminação conferem significado aos conectivos lógicos?
• O que é um sequente e como suas regras diferem das da dedução natural?
• Como a normalização simplifica as provas de dedução natural?
• Como as versões clássica e intuicionista desses cálculos estão relacionadas?

Key theories

Regras de introdução e eliminação

Cada conectivo é governado por regras que o introduzem e regras que o exploram, e sua harmonia, que a eliminação recupera exatamente o que a introdução insere, expressa o significado do conectivo.

Teorema da normalização

Prawitz mostrou que as provas de dedução natural podem ser reduzidas a uma forma normal livre de desvios, onde uma introdução é imediatamente desfeita por uma eliminação, o análogo da dedução natural à eliminação do corte.

Correspondência dos dois cálculos

A dedução natural e o cálculo de sequentes provam os mesmos teoremas e podem ser traduzidos um para o outro, com as regras à esquerda do sequente correspondendo às regras de eliminação da dedução natural.

Clinical relevance

Esses cálculos são os formatos padrão para o estudo estrutural das provas: a dedução natural fundamenta a teoria dos tipos e os assistentes de prova através da correspondência provas-como-programas, enquanto o cálculo de sequentes, com sua propriedade de subfórmula após a eliminação do corte, é a base da busca automatizada de provas e dos tableaux analíticos.

History

Gentzen introduziu tanto a dedução natural quanto o cálculo de sequentes em 1934 e 1935, desenvolvendo o cálculo de sequentes para obter seu teorema de eliminação do corte após considerar a dedução natural mais difícil de analisar. Prawitz reviveu a dedução natural em 1965 com um estudo aprofundado de normalização, e os sistemas tornaram-se centrais para os desenvolvimentos posteriores de provas-como-programas.

Key figures

• Gerhard Gentzen
• Dag Prawitz
• Stanislaw Jaskowski
• Jan von Plato

Seminal works

• troelstra2000
• prawitz1965
• negri2001

Frequently asked questions

Qual a diferença entre dedução natural e cálculo de sequentes?

A dedução natural opera com fórmulas sob um contexto de suposições e usa regras de eliminação, correspondendo de perto à prova informal. O cálculo de sequentes opera com implicações explícitas e substitui as regras de eliminação por regras de introdução à esquerda, um formato que torna a eliminação do corte e a propriedade de subfórmula transparentes.

Por que a normalização é importante?

Uma prova normal não contém desvios e possui a propriedade de subfórmula, de modo que cada fórmula nela é uma subfórmula da conclusão ou das premissas. Isso restringe a forma das provas, produz resultados de consistência e, via correspondência provas-como-programas, corresponde à avaliação de um programa para um valor.