A Arquitetura das Demonstrações
Coleção Escola de Lógica Matemática
JOÃO CARLOS MOREIRA
Doutor em Matemática
Universidade Federal de Uberlândia
Copyright©2013-2025 Coleção Escola de Lógica Matemática. Todos os direitos reservados.
Imagine poder desmontar uma demonstração matemática como quem desmonta um relógio, observando cada engrenagem, cada movimento preciso que leva das hipóteses às conclusões. O cálculo de sequentes, criado pelo brilhante lógico Gerhard Gentzen na década de 1930, oferece exatamente essa visão microscópica do raciocínio dedutivo. Mais do que um sistema formal, os sequentes revelam a estrutura íntima das demonstrações, expondo os passos elementares do pensamento lógico que normalmente permanecem ocultos em argumentos informais.
Gerhard Gentzen transformou nossa compreensão das demonstrações matemáticas ao criar um sistema onde cada passo de raciocínio corresponde a uma regra explícita e verificável. Seu cálculo de sequentes não apenas formaliza o processo dedutivo, mas o torna transparente e analisável. Como um arquiteto que desenha plantas detalhadas antes de construir, Gentzen nos deu as ferramentas para projetar e verificar demonstrações com precisão cirúrgica.
Um sequente é uma afirmação sobre consequência lógica, escrita na forma Γ ⊢ Δ, onde Γ (gama) representa um conjunto de hipóteses e Δ (delta) um conjunto de conclusões. O símbolo ⊢ (torniquete) significa "implica" ou "demonstra". Intuitivamente, o sequente afirma: "das hipóteses em Γ, podemos deduzir pelo menos uma das conclusões em Δ". Esta notação elegante captura a essência do raciocínio dedutivo em sua forma mais pura.
Pense em um sequente como um julgamento lógico. O lado esquerdo contém as evidências (premissas), o lado direito as possíveis conclusões. Quando escrevemos A, B ⊢ C, D, estamos afirmando que, assumindo A e B como verdadeiros, pelo menos uma entre C ou D deve ser verdadeira. Esta interpretação disjuntiva do lado direito é fundamental para entender o poder expressivo dos sequentes.
Uma das belezas do cálculo de sequentes reside em sua simetria fundamental. Hipóteses e conclusões são tratadas de forma dual, com regras espelhadas para introdução à esquerda e à direita de cada conectivo. Esta simetria não é meramente estética; ela revela profundas conexões entre conceitos aparentemente distintos e facilita a análise sistemática de propriedades lógicas.
Enquanto a dedução natural imita o raciocínio humano informal, o cálculo de sequentes oferece uma perspectiva mais algorítmica. Cada regra de inferência transforma sequentes em outros sequentes, criando uma máquina dedutiva onde demonstrações emergem naturalmente da aplicação sistemática de regras. Esta abordagem mecânica torna os sequentes ideais para implementação computacional.
O cálculo de sequentes transcende a teoria pura, encontrando aplicações em verificação de software, inteligência artificial, bancos de dados dedutivos e síntese de programas. Compiladores usam variantes de sequentes para otimização de código. Assistentes de prova como Coq e Isabelle implementam táticas baseadas em sequentes. A linguagem de programação lógica Prolog pode ser vista como uma implementação operacional de um fragmento do cálculo de sequentes.
Nossa jornada pelo cálculo de sequentes seguirá um caminho cuidadosamente planejado. Começaremos com as regras estruturais básicas, explorando como manipular sequentes sem alterar seu conteúdo lógico. Depois, introduziremos os conectivos lógicos um a um, observando suas regras duais de introdução. Aprenderemos a construir árvores de derivação, estudaremos o fundamental teorema de eliminação do corte, e exploraremos os sistemas clássico (LK) e intuicionista (LJ). Por fim, veremos aplicações práticas e conexões com a computação moderna.
Estudar cálculo de sequentes é como aprender uma nova língua para expressar ideias matemáticas. No início, a notação pode parecer estranha, as regras mecânicas. Mas gradualmente, padrões emergem, intuições se desenvolvem, e você descobrirá uma ferramenta poderosa para pensar sobre demonstrações. Como um músico que aprende a ler partituras para entender melhor a música, dominar sequentes enriquecerá sua compreensão da matemática.
O cálculo de sequentes nos convida a repensar o que significa demonstrar. Não se trata apenas de convencer, mas de construir argumentos com a precisão de um relojoeiro, a elegância de um arquiteto e a confiabilidade de um engenheiro. Prepare-se para descobrir a beleza oculta nas engrenagens do raciocínio lógico. Nossa aventura pelo mundo dos sequentes está apenas começando!
Antes de mergulharmos nos conectivos lógicos e suas complexidades, precisamos dominar as regras estruturais — os movimentos básicos que nos permitem manipular sequentes preservando sua validade. Como um pianista que pratica escalas antes de tocar sinfonias, compreender estas regras fundamentais é essencial para navegar com fluência pelo cálculo de sequentes. As regras estruturais são o alfabeto com o qual escreveremos demonstrações mais elaboradas.
A mais fundamental de todas as regras é a identidade, também chamada de axioma inicial. Ela afirma simplesmente que qualquer fórmula implica ela mesma: A ⊢ A. Esta trivialidade aparente é o ponto de partida de toda demonstração, o alicerce sobre o qual construímos edifícios lógicos complexos. Sem identidade, não há demonstração possível.
O enfraquecimento nos permite adicionar fórmulas extras tanto às hipóteses quanto às conclusões sem invalidar um sequente. Se conseguimos demonstrar Γ ⊢ Δ, então certamente podemos demonstrar Γ, A ⊢ Δ (enfraquecimento à esquerda) ou Γ ⊢ Δ, B (enfraquecimento à direita). É como dizer: se um argumento funciona, adicionar hipóteses desnecessárias ou conclusões alternativas não o invalida.
A contração elimina duplicações desnecessárias de fórmulas. Se temos Γ, A, A ⊢ Δ, podemos contrair para Γ, A ⊢ Δ. Similarmente, Γ ⊢ Δ, B, B contrai para Γ ⊢ Δ, B. Esta regra reflete a ideia de que ter múltiplas cópias da mesma hipótese ou conclusão não adiciona poder dedutivo — em lógica clássica, repetição não fortalece argumentos.
A ordem das fórmulas em um sequente não importa — esta é a essência da regra de permutação. Podemos reorganizar livremente as fórmulas tanto no antecedente quanto no consequente. De Γ, A, B, Γ' ⊢ Δ obtemos Γ, B, A, Γ' ⊢ Δ. Esta propriedade reflete o fato de que conjunção e disjunção são comutativas em suas interpretações semânticas.
A regra do corte é simultaneamente a mais poderosa e a mais controversa das regras estruturais. Ela afirma: se temos Γ ⊢ Δ, A e A, Γ' ⊢ Δ', então podemos deduzir Γ, Γ' ⊢ Δ, Δ'. Intuitivamente, se podemos provar A e depois usar A para provar algo mais, podemos combinar as duas demonstrações eliminando A como intermediário. O corte representa o uso de lemas em demonstrações.
Em lógicas sub-estruturais, algumas regras estruturais são restringidas ou eliminadas, criando sistemas que modelam recursos limitados. Lógica linear, por exemplo, rejeita contração e enfraquecimento, tratando hipóteses como recursos consumíveis. Lógica relevante elimina enfraquecimento, garantindo que todas as premissas sejam usadas. Estas variações têm aplicações em ciência da computação, modelando memória, tempo e outros recursos computacionais.
Uma propriedade notável das regras estruturais é sua inversibilidade em muitos contextos. Se podemos derivar Γ, A ⊢ Δ usando enfraquecimento, frequentemente podemos derivar Γ ⊢ Δ sem A. Esta propriedade é crucial para busca de provas e implementação de provadores automáticos, permitindo estratégias de busca mais eficientes.
Ao construir demonstrações, as regras estruturais funcionam como ferramentas de organização. Permutação nos deixa reordenar para clareza. Contração elimina redundâncias. Enfraquecimento adiciona contexto quando necessário. O corte permite modularização, dividindo provas complexas em partes gerenciáveis. Dominar estas regras é essencial para construir demonstrações elegantes e eficientes.
As regras estruturais permitem transformar demonstrações em formas canônicas. Eliminando redundâncias com contração, organizando com permutação, e eventualmente eliminando cortes, podemos obter demonstrações em forma normal. Esta normalização é fundamental para comparar demonstrações, determinar equivalências e analisar complexidade.
As regras estruturais são o esqueleto invisível que sustenta toda demonstração no cálculo de sequentes. Como as regras de harmonia na música, elas operam nos bastidores, organizando e estruturando nossos argumentos. Embora possam parecer técnicas e abstratas, são elas que garantem a flexibilidade e o poder do sistema. Com este fundamento sólido, estamos prontos para adicionar os conectivos lógicos e ver como eles dançam dentro desta estrutura!
Os conectivos lógicos ganham vida nova no cálculo de sequentes. Cada conectivo — conjunção, disjunção, implicação, negação — possui regras duais de introdução: uma para quando aparece nas hipóteses (lado esquerdo) e outra para quando surge nas conclusões (lado direito). Esta simetria elegante revela a natureza profunda destes operadores e como eles tecem a trama do raciocínio lógico. Vamos explorar como cada conectivo se comporta neste teatro formal das demonstrações.
A conjunção (∧) representa a simultaneidade de verdades. No lado direito de um sequente, introduzir A ∧ B exige demonstrar tanto A quanto B separadamente. No lado esquerdo, ter A ∧ B como hipótese nos dá acesso tanto a A quanto a B. Esta dualidade reflete perfeitamente nossa intuição: para afirmar "A e B", precisamos de ambos; ao assumir "A e B", podemos usar cada um.
A disjunção (∨) expressa alternativas. Para concluir A ∨ B (lado direito), basta demonstrar A ou demonstrar B — temos escolha. Mas quando A ∨ B é hipótese (lado esquerdo), devemos considerar ambos os casos, demonstrando nossa conclusão tanto assumindo A quanto assumindo B. Esta inversão de papéis ilustra a dualidade fundamental entre conjunção e disjunção.
A implicação (→) captura a essência da dedução. Para demonstrar A → B (lado direito), assumimos A e demonstramos B. Quando temos A → B como hipótese (lado esquerdo), podemos usá-la fornecendo uma prova de A para obter B. Esta regra esquerda incorpora o modus ponens, a mais fundamental das regras de inferência.
A negação (¬) inverte papéis de forma dramática. Para demonstrar ¬A (lado direito), assumimos A e derivamos contradição. Quando temos ¬A como hipótese (lado esquerdo), podemos concluir qualquer coisa se conseguirmos demonstrar A — ex falso quodlibet. A negação revela a natureza dual de hipóteses e conclusões no cálculo de sequentes.
O bicondicional (↔) expressa equivalência. A ↔ B significa simultaneamente A → B e B → A. As regras refletem esta decomposição: demonstrar A ↔ B requer provar ambas as direções; usar A ↔ B como hipótese permite inferir em qualquer direção. O bicondicional estabelece pontes bidirecionais no raciocínio.
Os quantificadores universal (∀) e existencial (∃) também possuem regras duais. Para demonstrar ∀x.A(x), provamos A(a) para uma variável fresca a. Para usar ∀x.A(x), instanciamos com qualquer termo. O existencial inverte estes papéis: demonstramos ∃x.A(x) exibindo um termo específico, mas usamos ∃x.A(x) com uma variável fresca.
Nem todas as regras são criadas iguais. Algumas são inversíveis — aplicá-las não compromete a completude da busca por provas. Regras inversíveis podem ser aplicadas avidamente. Outras requerem escolhas (qual disjunto provar?) ou comprometimentos (qual termo usar para instanciar?). Compreender estas distinções é crucial para construir demonstrações eficientemente.
Cada conectivo corresponde a um padrão computacional. Conjunção modela produtos e registros. Disjunção representa somas e variantes. Implicação codifica funções. Negação relaciona-se com continuações. Esta correspondência, conhecida como isomorfismo de Curry-Howard, revela que demonstrações são programas e proposições são tipos.
Dominar os conectivos significa saber quando e como aplicar cada regra. Começamos identificando a estrutura principal da fórmula-alvo. Aplicamos regras inversíveis imediatamente. Para regras com escolhas, analisamos o contexto para guiar decisões. A prática desenvolve intuição sobre qual caminho seguir em cada bifurcação da demonstração.
Os conectivos lógicos são os verbos do cálculo de sequentes, expressando como proposições se relacionam e interagem. Suas regras duais revelam simetrias profundas no coração da lógica. Como notas musicais que se combinam em acordes, os conectivos se entrelaçam para formar argumentos complexos. Com este vocabulário lógico em mãos, estamos prontos para explorar como estas regras se compõem em demonstrações completas!
As regras de inferência são os motores que movem o cálculo de sequentes, transformando sequentes em outros sequentes, tecendo a trama das demonstrações. Como receitas culinárias que transformam ingredientes em pratos elaborados, estas regras pegam premissas e produzem conclusões através de transformações precisas e verificáveis. Neste capítulo, exploraremos o rico repertório de regras que tornam o cálculo de sequentes uma máquina dedutiva poderosa e elegante.
Cada regra de inferência possui premissas (sequentes acima da linha) e uma conclusão (sequente abaixo da linha). A linha horizontal age como um operador de transformação: se podemos demonstrar as premissas, então podemos deduzir a conclusão. Algumas regras não têm premissas — são axiomas, pontos de partida de nossas demonstrações. Outras têm múltiplas premissas, exigindo que provemos várias condições.
Distinguimos entre regras estruturais, que manipulam a forma dos sequentes sem examinar fórmulas específicas, e regras operacionais, que decompõem conectivos lógicos. As estruturais são como movimentos de organização — rearranjam, simplificam, preparam. As operacionais são transformações químicas — quebram moléculas lógicas em seus componentes ou sintetizam novas estruturas.
Para demonstrar uma implicação A → B, assumimos A e provamos B. No cálculo de sequentes, isto se traduz na regra: de Γ, A ⊢ B, Δ podemos deduzir Γ ⊢ A → B, Δ. Esta regra captura o raciocínio hipotético, fundamental em matemática. Note como A migra do lado esquerdo (hipótese) para dentro da implicação no lado direito (conclusão).
Quando temos A → B como hipótese, podemos usá-la através da regra esquerda da implicação. Esta regra tem duas premissas: devemos provar A e, assumindo B, provar nossa conclusão. É a formalização do modus ponens, o mais fundamental dos padrões de raciocínio. A regra reflete como "gastamos" uma implicação para obter sua conclusão.
A disjunção apresenta assimetria interessante. Para provar A ∨ B (regra direita), escolhemos provar A ou B — temos liberdade. Mas quando A ∨ B é hipótese (regra esquerda), devemos considerar ambos os casos, provando nossa conclusão tanto de A quanto de B. Esta análise de casos é ubíqua em demonstrações matemáticas.
A conjunção inverte o padrão da disjunção. Para provar A ∧ B (regra direita), devemos provar ambos A e B — sem escolha. Quando A ∧ B é hipótese (regra esquerda), podemos escolher usar A ou B conforme necessário. Esta dualidade entre conjunção e disjunção é uma das simetrias mais elegantes do cálculo de sequentes.
A negação conecta os dois lados do sequente de forma surpreendente. Para provar ¬A, assumimos A e derivamos contradição. No cálculo de sequentes, isto significa mover A para o lado esquerdo: de Γ, A ⊢ Δ deduzimos Γ ⊢ ¬A, Δ. A regra esquerda faz o movimento inverso. A negação revela que hipóteses e conclusões são faces da mesma moeda.
Algumas sequências comuns de regras podem ser empacotadas em regras derivadas. Por exemplo, a regra de contraposição (de A → B deduzir ¬B → ¬A) pode ser vista como uma regra derivada, obtida por composição de regras básicas. Estas macro-regras aceleram demonstrações sem adicionar poder ao sistema.
A ordem em que aplicamos regras impacta dramaticamente a dificuldade de construir uma prova. Regras inversíveis devem ser aplicadas primeiro — não há risco. Regras que introduzem escolhas devem ser adiadas. Quando múltiplas regras competem, análise do contexto guia a decisão. Desenvolver intuição para esta coreografia é uma arte que vem com prática.
O conjunto de regras do cálculo de sequentes é completo: toda fórmula válida tem uma demonstração. É também correto: toda fórmula demonstrável é válida. Esta correspondência perfeita entre sintaxe (demonstrações) e semântica (verdade) é o triunfo do sistema de Gentzen. As regras capturam exatamente o raciocínio lógico válido, nem mais, nem menos.
As regras de inferência são as ferramentas com as quais esculpimos demonstrações do bloco bruto da lógica. Cada regra é um cinzel especializado, projetado para um tipo específico de transformação. Juntas, formam um kit completo para construir qualquer argumento válido. Como um artesão que conhece intimamente suas ferramentas, dominar estas regras nos torna arquitetos habilidosos de demonstrações. Com este arsenal em mãos, estamos prontos para construir as majestosas catedrais lógicas que são as árvores de derivação!
Uma demonstração no cálculo de sequentes cresce como uma árvore invertida, com a conclusão na raiz e os axiomas nas folhas. Cada nó representa um sequente, cada galho uma aplicação de regra. Estas árvores de derivação não são meras representações visuais — elas são a própria substância das demonstrações, capturando não apenas o que provamos, mas como provamos. Neste capítulo, aprenderemos a cultivar estas árvores lógicas, desde a semente da conclusão até a floração dos axiomas.
Uma árvore de derivação começa com o sequente que queremos provar — a raiz. Aplicamos regras de inferência de baixo para cima, decompondo o objetivo em sub-objetivos mais simples. Cada aplicação de regra cria novos galhos, cada um com seu próprio sequente para provar. O processo continua até que todos os galhos terminam em axiomas (geralmente instâncias da identidade A ⊢ A). Uma árvore completa, sem galhos em aberto, constitui uma demonstração.
Construímos árvores de derivação de baixo para cima, começando com o objetivo e trabalhando em direção aos axiomas. Esta abordagem goal-directed é natural e eficiente: sabemos onde queremos chegar e procuramos caminhos para lá. Como um montanhista que planeja a escalada olhando do cume para a base, identificamos os passos necessários decompondo o problema.
Vamos demonstrar ((A → B) → A) → A, a lei de Pierce. Começamos com ⊢ ((A → B) → A) → A. Aplicando →-direita, obtemos (A → B) → A ⊢ A. Agora precisamos usar a hipótese (A → B) → A. Aplicando →-esquerda, geramos dois sub-objetivos: provar A → B e, assumindo A, provar A. O segundo é trivial (identidade). Para o primeiro, aplicamos →-direita novamente, obtendo A ⊢ B, A, que é válido por enfraquecimento da identidade.
Frequentemente, múltiplas regras podem ser aplicadas a um sequente. Algumas escolhas levam a demonstrações elegantes, outras a becos sem saída. Quando provamos A ∨ B, devemos escolher provar A ou B. Quando usamos ∃x.P(x), devemos escolher uma testemunha. Estas escolhas tornam a busca por demonstrações não-determinística, exigindo estratégia e, às vezes, backtracking.
Uma árvore está fechada quando todos os seus galhos terminam em axiomas — temos uma demonstração completa. Uma árvore aberta tem pelo menos um galho que não pode ser fechado, indicando que o sequente pode não ser demonstrável. Galhos abertos frequentemente revelam contraexemplos, mostrando por que a fórmula não é válida.
Nem todas as demonstrações são criadas iguais. Algumas são elegantes e concisas, outras desnecessariamente complexas. Podemos otimizar árvores eliminando desvios, combinando galhos similares, e escolhendo regras que minimizam o tamanho da árvore. Uma demonstração ótima não é apenas correta, mas também clara e eficiente.
Sob a correspondência de Curry-Howard, cada demonstração é também um programa. A estrutura da árvore de derivação corresponde à estrutura do programa. Aplicações de regras são construções de termos. Axiomas são variáveis. Uma demonstração de A → B é literalmente uma função de A para B. Esta dualidade profunda conecta lógica e computação.
A estrutura sistemática do cálculo de sequentes o torna ideal para automação. Provadores automáticos exploram o espaço de possíveis árvores, aplicando regras sistematicamente. Estratégias incluem busca em profundidade, largura, ou best-first. Heurísticas guiam a escolha de regras. Poda elimina galhos não-promissores. Modernos provadores podem encontrar demonstrações complexas em segundos.
Uma árvore de derivação bem apresentada conta uma história lógica. Cada passo deve ser claro e justificado. Anotações explicam escolhas não-óbvias. A estrutura visual ajuda a compreensão. Como um texto bem escrito, uma demonstração bem documentada comunica não apenas correção, mas entendimento.
Construir árvores de derivação é tanto arte quanto ciência. A mecânica das regras fornece a técnica, mas escolher o caminho certo requer intuição, experiência e criatividade. Como um jardineiro que conhece quando podar e quando deixar crescer, o matemático habilidoso sabe quando insistir em uma abordagem e quando buscar alternativas.
As árvores de derivação são mais que representações de demonstrações — elas são as demonstrações em si, capturando cada nuance do raciocínio lógico em sua estrutura ramificada. Como genealogias do pensamento, traçam a linhagem de cada conclusão até seus ancestrais axiomáticos. Dominar sua construção é dominar a arte da demonstração formal. Com esta habilidade fundamental estabelecida, estamos prontos para explorar um dos teoremas mais profundos do cálculo de sequentes: a eliminação do corte!
O teorema da eliminação do corte é a joia da coroa do cálculo de sequentes, um resultado tão profundo que Gentzen o considerou sua maior descoberta. A regra do corte permite usar resultados intermediários — provar A e depois usar A para provar B. Surpreendentemente, Gentzen mostrou que todo uso de corte pode ser eliminado, que toda demonstração com cortes pode ser transformada em uma sem cortes. Esta descoberta revolucionou nossa compreensão da natureza das demonstrações matemáticas.
A regra do corte formaliza o uso de lemas em matemática. Se podemos provar Γ ⊢ Δ, A e também A, Γ' ⊢ Δ', então podemos concluir Γ, Γ' ⊢ Δ, Δ'. A fórmula A, que aparece à direita na primeira premissa e à esquerda na segunda, é "cortada" — usada como ponte mas não aparece na conclusão. O corte representa composição de demonstrações, um princípio fundamental do raciocínio modular.
A eliminação do corte pode parecer contraproducente — por que remover uma ferramenta tão útil? A resposta revela profundidade surpreendente. Demonstrações sem corte têm a propriedade da subfórmula: cada fórmula que aparece na derivação é subfórmula do sequente final. Isto garante que a demonstração não invoca conceitos externos, trabalhando apenas com os componentes do problema original. É uma forma de pureza lógica.
O Hauptsatz (teorema principal) de Gentzen afirma: se um sequente é demonstrável no cálculo de sequentes com corte, então é demonstrável sem corte. A prova é construtiva — Gentzen forneceu um algoritmo para transformar qualquer demonstração com cortes em uma sem cortes. Este algoritmo, embora possa aumentar exponencialmente o tamanho da demonstração, sempre termina com sucesso.
Eliminar um corte envolve "empurrar" a regra do corte para cima na árvore de derivação, diminuindo gradualmente a complexidade da fórmula cortada. Quando o corte envolve uma fórmula composta, decompomos em cortes de componentes mais simples. Eventualmente, chegamos a cortes atômicos que podem ser eliminados diretamente ou se tornam triviais.
A eliminação procede por casos, dependendo das últimas regras aplicadas antes do corte. Se a fórmula de corte foi introduzida por uma regra à direita na premissa esquerda e usada por uma regra à esquerda na premissa direita, temos um "corte principal" que pode ser reduzido. Casos não-principais requerem comutações que movem o corte para cima na árvore.
Considere uma demonstração que usa A ∧ B como lema intermediário. O corte em A ∧ B pode ser substituído por dois cortes menores, um em A e outro em B. Se a demonstração original prova A ∧ B e depois usa apenas A, a eliminação mostra que B nunca era necessário. Este processo revela a estrutura essencial do argumento, removendo desvios desnecessários.
A eliminação do corte tem um preço: demonstrações sem corte podem ser exponencialmente maiores que suas versões com corte. Um único corte bem escolhido pode comprimir dramaticamente uma demonstração. Este trade-off entre tamanho e pureza estrutural é fundamental. Na prática, usamos cortes para modularidade e clareza, sabendo que em princípio poderiam ser eliminados.
A eliminação do corte tem aplicações profundas. Prova a consistência da aritmética de Peano (relativa a uma teoria mais fraca). Garante que demonstrações construtivas produzem testemunhas. Em ciência da computação, inspira a normalização em cálculo lambda e otimização de programas. O teorema fundamenta a análise ordinal e a teoria da demonstração reversa.
Paradoxalmente, embora o corte seja eliminável, é indispensável para a prática matemática. Lemas intermediários organizam nosso pensamento, modularizam argumentos complexos, e revelam conexões entre áreas. A criatividade matemática frequentemente reside em identificar o lema certo — o corte perfeito que ilumina uma demonstração. A eliminabilidade do corte não diminui seu valor pragmático.
O teorema de eliminação do corte se estende a muitos sistemas lógicos. Em lógica intuicionista, preserva propriedades construtivas. Em lógica linear, revela uso de recursos. Em lógica modal, mantém propriedades de necessidade. Cada extensão revela novos aspectos da eliminação do corte, confirmando sua centralidade na teoria da demonstração.
O teorema da eliminação do corte é um daqueles resultados que quanto mais se estuda, mais profundo parece. Como um cristal que revela novas facetas sob diferentes luzes, a eliminação do corte ilumina conexões entre lógica, computação, e os fundamentos da matemática. É simultaneamente um resultado técnico sobre manipulação de símbolos e uma verdade filosófica sobre a natureza do raciocínio. Com esta compreensão profunda, estamos prontos para explorar como diferentes escolhas de regras levam a diferentes sistemas lógicos!
Gentzen não criou apenas um cálculo de sequentes, mas dois: LK para lógica clássica e LJ para lógica intuicionista. Como gêmeos com personalidades distintas, estes sistemas compartilham a mesma estrutura fundamental mas diferem em aspectos cruciais. LK abraça o terceiro excluído e a prova por contradição, enquanto LJ exige construções explícitas e rejeita argumentos não-construtivos. Neste capítulo, exploraremos ambos os sistemas, suas diferenças sutis e suas profundas implicações filosóficas e computacionais.
LK (Logistischer Klassischer Kalkül) formaliza a lógica clássica em toda sua glória. Sequentes podem ter múltiplas fórmulas em ambos os lados, interpretadas conjuntivamente à esquerda e disjuntivamente à direita. Esta simetria permite expressar naturalmente princípios clássicos como o terceiro excluído (⊢ A ∨ ¬A) e a dupla negação (¬¬A ⊢ A). LK é o sistema onde matemáticos clássicos se sentem em casa.
LJ (Logistischer Intuitionistischer Kalkül) restringe sequentes a no máximo uma fórmula no consequente. Esta restrição aparentemente simples tem consequências profundas: elimina o terceiro excluído, invalida dupla negação, e força demonstrações a serem construtivas. Em LJ, provar que algo existe requer construí-lo explicitamente. É a lógica dos algoritmos e das construções efetivas.
A diferença entre LK e LJ se manifesta mais claramente nas regras para implicação e negação no lado direito. Em LK, para provar Γ ⊢ A → B, Δ, movemos A para a esquerda obtendo Γ, A ⊢ B, Δ. As fórmulas extras em Δ permanecem. Em LJ, com no máximo uma conclusão, temos apenas Γ ⊢ A → B, levando a Γ, A ⊢ B. Esta restrição força a implicação intuicionista a ser mais "focada".
Muitos teoremas clássicos falham em LJ. O terceiro excluído ⊢ A ∨ ¬A não é demonstrável — precisaríamos construir A ou ¬A sem saber nada sobre A. A eliminação da dupla negação ¬¬A ⊢ A falha similarmente. A lei de Pierce ((A → B) → A) → A, demonstrável em LK, não tem prova em LJ. Estes "falhas" não são defeitos, mas características que garantem construtividade.
Tudo demonstrável em LJ também é em LK — intuicionismo é um fragmento do classicismo. Mas demonstrações em LJ têm propriedades especiais. Se provamos ∃x.P(x) em LJ, podemos extrair uma testemunha específica. Se provamos A ∨ B, sabemos qual disjunto vale. Esta propriedade de disjunção e existência torna LJ ideal para computação.
Surpreendentemente, podemos traduzir LK em LJ através da tradução de dupla negação. Substituímos cada fórmula atômica A por ¬¬A e propagamos. Sob esta tradução, todo teorema clássico se torna intuicionisticamente válido (em forma modificada). Isto mostra que lógica clássica pode ser vista como intuicionista com dupla negação sistemática — classicismo é intuicionismo "com óculos de negação".
LK tem semântica booleana clássica — duas valores de verdade, tabelas-verdade usuais. LJ requer semântica mais sofisticada: modelos de Kripke, álgebras de Heyting, ou interpretação BHK (Brouwer-Heyting-Kolmogorov). Nestas semânticas, verdade é substituída por "construtibilidade" ou "verificabilidade", capturando a natureza construtiva do intuicionismo.
LJ é a lógica natural da computação. Através de Curry-Howard, demonstrações em LJ correspondem a programas funcionais tipados. Linguagens como ML, Haskell e Agda implementam fragmentos de LJ. Assistentes de prova como Coq usam lógica intuicionista por default. A restrição de uma conclusão garante que programas extraídos são determinísticos e bem-comportados.
A escolha entre LK e LJ não é apenas técnica, mas filosófica. LK oferece poder e familiaridade, permitindo argumentos não-construtivos elegantes. LJ garante construtividade e computabilidade, ao custo de rejeitar alguns princípios clássicos. Muitos sistemas modernos permitem misturar os dois, usando lógica clássica quando conveniente mas marcando claramente onde construtividade é perdida.
LK e LJ representam duas visões da verdade matemática: clássica/platônica versus construtiva/computacional. Como duas lentes através das quais podemos ver o mundo lógico, cada uma revela aspectos que a outra obscurece. LK nos dá o poder do raciocínio indireto e a elegância do terceiro excluído. LJ nos dá construções explícitas e garantias computacionais. Juntos, formam um dueto harmonioso que enriquece nossa compreensão da lógica e da computação. Com este entendimento dos sistemas fundamentais, podemos agora explorar suas aplicações práticas em demonstrações matemáticas!
O cálculo de sequentes não é apenas uma curiosidade teórica — é uma ferramenta poderosa para formalizar e verificar demonstrações matemáticas reais. Desde teoremas elementares de álgebra até resultados sofisticados de análise, o cálculo de sequentes fornece uma linguagem precisa para expressar e validar argumentos matemáticos. Neste capítulo, veremos como traduzir demonstrações informais para o mundo formal dos sequentes e como esta tradução revela a estrutura profunda do raciocínio matemático.
Considere o teorema: "Em um grupo, o elemento neutro é único". Informalmente, assumimos dois neutros e mostramos que são iguais. No cálculo de sequentes, expressamos isto como: ∀e₁,e₂ ((∀x (e₁ · x = x) ∧ ∀x (e₂ · x = x)) → e₁ = e₂). A demonstração procede aplicando regras de quantificadores e usando propriedades do grupo sistematicamente, revelando cada passo lógico normalmente oculto.
As definições épsilon-delta do cálculo são naturalmente expressas com quantificadores alternados. A continuidade de f em a: ∀ε>0 ∃δ>0 ∀x (|x-a|<δ → |f(x)-f(a)|<ε). Demonstrar que a composição de funções contínuas é contínua requer manipulação cuidadosa destes quantificadores. O cálculo de sequentes torna explícita a coreografia de épsilons e deltas.
Propriedades dos números naturais são elegantemente expressas em sequentes. A infinitude dos primos: ∀n ∃p (p > n ∧ primo(p)). A demonstração clássica de Euclides, que constrói um novo primo de uma lista finita, traduz-se em uma derivação que usa o axioma do boa-ordenação e propriedades de divisibilidade. Cada passo da construção corresponde a regras específicas.
Indução matemática tem uma representação natural no cálculo de sequentes. O princípio de indução pode ser expresso como uma regra: de ⊢ P(0) e n, P(n) ⊢ P(n+1), deduzir ⊢ ∀n P(n). Esta regra captura a essência da indução. Demonstrações por indução se tornam árvores onde o caso base e o passo indutivo são sub-árvores distintas.
Problemas de contagem frequentemente envolvem análise de casos e o princípio da inclusão-exclusão. O cálculo de sequentes organiza estes argumentos sistematicamente. Por exemplo, provar |A ∪ B| = |A| + |B| - |A ∩ B| requer decomposição em casos disjuntos, cada um formalizado como um galho na árvore de derivação.
Teoremas geométricos, embora visuais, têm estrutura lógica precisa. "Todo triângulo tem soma dos ângulos igual a 180°" esconde quantificadores e implicações. Propriedades topológicas como compacidade (toda cobertura aberta tem subcobertura finita) são intrinsecamente declarações sobre quantificadores alternados, naturalmente expressas em sequentes.
O cálculo de sequentes revela claramente onde demonstrações usam princípios não-construtivos. Uma prova que "existe irracional elevado a irracional que é racional" usando √2^√2 procede por casos no terceiro excluído. Em LK, isto é direto. Em LJ, precisaríamos construir explicitamente o exemplo, forçando uma demonstração diferente.
Assistentes de prova como Coq, Lean e Isabelle implementam variantes do cálculo de sequentes. Matemáticos podem escrever demonstrações que são verificadas mecanicamente. O Four Color Theorem e o Kepler Conjecture foram verificados desta forma. O cálculo de sequentes fornece a fundação teórica para esta verificação.
O cálculo de sequentes não apenas verifica, mas sugere demonstrações. A estrutura das regras guia a busca. Tentando provar um sequente, as regras aplicáveis sugerem estratégias. Falhas revelam contraexemplos ou lemas necessários. O processo de construção da árvore é também um processo de descoberta.
O cálculo de sequentes oferece uma maneira sistemática de ensinar demonstração. Estudantes aprendem a estrutura lógica explicitamente. Erros comuns (quantificadores trocados, hipóteses esquecidas) tornam-se impossíveis. A construção passo-a-passo desenvolve rigor. A visualização em árvore clarifica estrutura de argumentos complexos.
O cálculo de sequentes transforma demonstrações de arte em engenharia, de intuição em algoritmo. Mas longe de mecanizar a matemática, ele revela sua estrutura profunda, tornando explícito o que antes era implícito. Como um microscópio que revela células em tecido vivo, o cálculo de sequentes mostra os átomos lógicos dos quais argumentos matemáticos são construídos. Esta clareza não diminui a beleza da matemática — pelo contrário, revela uma elegância estrutural ainda mais profunda. Com esta apreciação das aplicações práticas, vamos agora explorar como o cálculo de sequentes se conecta com o mundo da computação!
A conexão entre cálculo de sequentes e computação é uma das descobertas mais surpreendentes da ciência da computação. Demonstrações são programas, proposições são tipos, e a normalização de provas corresponde à execução de código. Esta correspondência, conhecida como isomorfismo de Curry-Howard, revela que lógica e computação são duas faces da mesma moeda. Neste capítulo, exploraremos como o cálculo de sequentes fundamenta linguagens de programação, sistemas de tipos, e verificação de software.
Sob a correspondência de Curry-Howard, cada demonstração no cálculo de sequentes corresponde a um programa funcional. Uma prova de A → B é literalmente uma função que transforma provas de A em provas de B. Conjunção corresponde a pares, disjunção a tipos soma, quantificador universal a polimorfismo. Esta correspondência é tão precisa que podemos executar demonstrações como programas.
Linguagens como ML, Haskell e OCaml implementam fragmentos do cálculo de sequentes. O sistema de tipos dessas linguagens é essencialmente um cálculo de sequentes disfarçado. Type checking é verificação de provas. Type inference é busca de demonstrações. Programar nestas linguagens é, literalmente, construir demonstrações matemáticas executáveis.
Sistemas como Coq, Agda, Lean e Idris levam Curry-Howard ao extremo. São simultaneamente linguagens de programação e provadores de teoremas. Você escreve programas que são provas, e o compilador verifica tanto correção lógica quanto computacional. Estes sistemas usam variantes do cálculo de sequentes como fundação teórica.
Provadores automáticos de teoremas implementam busca no espaço de possíveis árvores de derivação. Isto é um problema computacional desafiador — o espaço é infinito e altamente ramificado. Heurísticas baseadas na estrutura do cálculo de sequentes guiam a busca. Unificação resolve escolhas de instanciação. Backtracking explora alternativas.
Lógica linear, uma variante do cálculo de sequentes sem contração e enfraquecimento, modela recursos computacionais. Cada hipótese deve ser usada exatamente uma vez — como memória que é consumida. Isto permite raciocinar sobre alocação de recursos, concorrência, e estado mutável de forma puramente lógica. Linguagens como Rust incorporam ideias de lógica linear em seus sistemas de tipos.
Compiladores modernos usam técnicas inspiradas no cálculo de sequentes. Verificação de tipos é essencialmente verificação de provas. Otimizações correspondem a transformações que preservam equivalência lógica. A eliminação do corte inspira técnicas de inlining e eliminação de código morto. Análise de fluxo usa princípios de propagação de sequentes.
Verificação formal de software usa cálculo de sequentes para provar propriedades de programas. Pré e pós-condições são sequentes. Invariantes de loop são sequentes preservados. Lógica de Hoare, base da verificação, é essencialmente cálculo de sequentes aplicado a programas imperativos. Ferramentas como Dafny e Why3 automatizam este processo.
Datalog e outras linguagens de consulta lógica são fragmentos do cálculo de sequentes. Queries são sequentes, fatos são axiomas, regras são implicações. O motor de inferência busca derivações. Otimização de queries corresponde a transformações de provas. Esta conexão permite aplicar décadas de pesquisa em teoria da prova a sistemas de banco de dados.
Sistemas de IA que raciocinam logicamente usam variantes do cálculo de sequentes. Planejadores automáticos buscam sequências de ações (provas) que levam do estado inicial ao objetivo. Sistemas especialistas codificam conhecimento como sequentes. Aprendizado de máquina simbólico induz regras de inferência de exemplos.
Smart contracts são programas cuja correção é crítica. Verificação formal usando cálculo de sequentes garante ausência de bugs. Linguagens como Michelson (Tezos) têm semântica formal baseada em sequentes. Propriedades de segurança são expressas como sequentes. Verificação acontece antes do deployment, prevenindo vulnerabilidades caras.
Mesmo computação quântica tem conexões com cálculo de sequentes. Lógica quântica modifica regras estruturais. Quantum lambda calculus estende Curry-Howard ao domínio quântico. Verificação de algoritmos quânticos usa sequentes adaptados. A estrutura fundamental do raciocínio lógico transcende o substrato computacional.
A conexão entre cálculo de sequentes e computação é uma das pontes mais profundas da ciência moderna, unindo matemática pura e engenharia prática. Cada programa é uma prova, cada compilação uma verificação, cada execução uma normalização. Esta unidade revela que computação não é apenas sobre mover bits, mas sobre transformar evidências lógicas. O cálculo de sequentes fornece a linguagem universal para expressar e verificar estas transformações. Com esta visão computacional estabelecida, vamos explorar como estas ideias se desenvolvem na teoria da demonstração moderna!
O cálculo de sequentes de Gentzen foi apenas o começo. Nas décadas desde sua criação, floresceu um campo rico e profundo — a teoria da demonstração moderna. Novas lógicas, sistemas mais expressivos, conexões surpreendentes com outras áreas da matemática e computação continuam a ser descobertas. Neste capítulo final, exploraremos as fronteiras atuais da teoria da demonstração, vendo como as ideias de Gentzen evoluíram e se ramificaram em direções que ele mal poderia imaginar.
Uma das aplicações mais profundas do cálculo de sequentes é a análise ordinal de teorias matemáticas. A cada teoria formal podemos associar um ordinal que mede sua "força de consistência". A eliminação do corte em extensões infinitárias do cálculo de sequentes permite calcular estes ordinais. Aritmética de Peano tem ordinal ε₀. Teorias mais fortes têm ordinais maiores. Esta hierarquia ordinal mapeia o universo das teorias matemáticas.
Andreoli descobriu que podemos restringir o espaço de busca sem perder completude através da focalização. Em sequentes focados, alternamos entre fases de decomposição invertível e escolhas focadas. Isto reduz dramaticamente o não-determinismo, tornando a busca mais eficiente. Focalização revela a estrutura computacional escondida nas provas.
Removendo ou modificando regras estruturais, obtemos lógicas que modelam fenômenos diversos. Lógica linear modela recursos. Lógica relevante garante uso de premissas. Lógica não-comutativa modela ordem e processo. Bunched logic combina aspectos clássicos e sub-estruturais. Estas lógicas encontram aplicações em verificação, linguística e filosofia.
Extensões do cálculo de sequentes para tipos dependentes permitem expressar especificações precisas. Em sistemas como Coq e Agda, tipos podem depender de valores, permitindo expressar propriedades complexas. A teoria de tipos de Martin-Löf, uma extensão construtiva do cálculo de sequentes, fundamenta matemática construtiva moderna.
Uma revolução recente conecta teoria de tipos com topologia algébrica. Tipos são espaços, termos são pontos, provas de igualdade são caminhos. Esta visão geométrica do cálculo de sequentes revela estruturas surpreendentes. Univalência — isomorfismo implica igualdade — fundamenta nova matemática. HoTT promete unificar fundamentos construtivos e clássicos.
Quão grandes precisam ser as provas? O cálculo de sequentes permite estudar esta questão precisamente. Alguns teoremas têm apenas provas exponencialmente longas. Outros admitem provas polinomiais. Esta análise conecta teoria da demonstração com complexidade computacional. P vs NP pode ser reformulado em termos de tamanho de provas.
Sistemas de deep inference permitem aplicar regras dentro de fórmulas, não apenas no nível superior. Isto aumenta expressividade e permite provas mais diretas. O cálculo de estruturas é um exemplo onde toda regra pode ser aplicada em qualquer contexto. Deep inference revela simetrias ocultas e simplifica meta-teoria.
Demonstrações podem ser vistas como estratégias vencedoras em jogos lógicos. Cada conectivo define um tipo de movimento. Proponente tenta verificar, Oponente tenta refutar. Esta visão lúdica ilumina aspectos computacionais e fornece semântica para lógicas complexas. Jogos infinitos modelam coinduçã̃o e processos infinitos.
Cálculo de sequentes tem interpretação categórica profunda. Demonstrações são morfismos, corte é composição, eliminação do corte é associatividade. Categorias monoidais modelam multiplicativos lineares. Toposes interpretam lógica intuicionista. Esta visão abstrata unifica diferentes sistemas e revela estruturas comuns.
A teoria da demonstração continua evoluindo rapidamente. Conexões com física quântica, machine learning, criptografia e biologia surgem constantemente. Novos sistemas são propostos para modelar fenômenos cada vez mais complexos. A busca por fundamentos mais expressivos e naturais continua. O cálculo de sequentes, em suas muitas encarnações, permanece no centro desta aventura intelectual.
A teoria da demonstração moderna transcendeu suas origens em fundamentos da matemática para se tornar uma ciência da estrutura do raciocínio em si. O cálculo de sequentes, criado para resolver questões sobre consistência, revelou-se uma linguagem universal para expressar e analisar argumentos dedutivos em todos os domínios. Como DNA lógico, codifica os padrões fundamentais do pensamento racional. À medida que enfrentamos desafios cada vez mais complexos — verificar sistemas críticos, raciocinar sobre incerteza, integrar humanos e máquinas — a teoria da demonstração fornece as ferramentas conceituais essenciais. O legado de Gentzen não é apenas um sistema formal, mas uma nova maneira de entender a própria natureza da demonstração e da verdade.
Este volume sobre o Cálculo de Sequentes foi construído sobre décadas de pesquisa em teoria da demonstração, lógica matemática e ciência da computação. As referências abrangem desde os trabalhos pioneiros de Gentzen até desenvolvimentos contemporâneos em teoria de tipos e verificação formal. Esta bibliografia oferece recursos para aprofundamento em cada aspecto do cálculo de sequentes, desde fundamentos teóricos até aplicações práticas em computação e matemática.
ANDREOLI, Jean-Marc. Logic Programming with Focusing Proofs in Linear Logic. Journal of Logic and Computation, v. 2, n. 3, p. 297-347, 1992.
AVIGAD, Jeremy; FEFERMAN, Solomon. Gödel's Functional Interpretation. In: Handbook of Proof Theory. Amsterdam: Elsevier, 1998. p. 337-405.
BARENDREGT, Henk; DEKKERS, Wil; STATMAN, Richard. Lambda Calculus with Types. Cambridge: Cambridge University Press, 2013.
BARWISE, Jon (Ed.). Handbook of Mathematical Logic. Amsterdam: North-Holland, 1977.
BEESON, Michael. Foundations of Constructive Mathematics. Berlin: Springer-Verlag, 1985.
BRASIL. Base Nacional Comum Curricular: Educação é a Base. Brasília: MEC/CONSED/UNDIME, 2018.
BUCHHOLZ, Wilfried. Proof Theory of Impredicative Subsystems of Analysis. Naples: Bibliopolis, 1988.
BUSS, Samuel R. (Ed.). Handbook of Proof Theory. Amsterdam: Elsevier, 1998.
CARNIELLI, Walter; CONIGLIO, Marcelo. Paraconsistent Logic: Consistency, Contradiction and Negation. Cham: Springer, 2016.
COQUAND, Thierry; HUET, Gérard. The Calculus of Constructions. Information and Computation, v. 76, n. 2-3, p. 95-120, 1988.
CURRY, Haskell B.; FEYS, Robert. Combinatory Logic. Amsterdam: North-Holland, 1958. v. 1.
DUMMETT, Michael. Elements of Intuitionism. 2nd ed. Oxford: Oxford University Press, 2000.
FITTING, Melvin. First-Order Logic and Automated Theorem Proving. 2nd ed. New York: Springer, 1996.
GALLIER, Jean. Logic for Computer Science: Foundations of Automatic Theorem Proving. 2nd ed. New York: Dover Publications, 2015.
GENTZEN, Gerhard. Untersuchungen über das logische Schließen. Mathematische Zeitschrift, v. 39, p. 176-210, 405-431, 1935.
GENTZEN, Gerhard. Die Widerspruchsfreiheit der reinen Zahlentheorie. Mathematische Annalen, v. 112, p. 493-565, 1936.
GIRARD, Jean-Yves. Linear Logic. Theoretical Computer Science, v. 50, n. 1, p. 1-102, 1987.
GIRARD, Jean-Yves; LAFONT, Yves; TAYLOR, Paul. Proofs and Types. Cambridge: Cambridge University Press, 1989.
GÖDEL, Kurt. Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes. Dialectica, v. 12, p. 280-287, 1958.
HARPER, Robert. Practical Foundations for Programming Languages. 2nd ed. Cambridge: Cambridge University Press, 2016.
HINDLEY, J. Roger; SELDIN, Jonathan P. Lambda-Calculus and Combinators: An Introduction. 2nd ed. Cambridge: Cambridge University Press, 2008.
HOWARD, William A. The Formulae-as-Types Notion of Construction. In: To H. B. Curry: Essays on Combinatory Logic. New York: Academic Press, 1980. p. 479-490.
KLEENE, Stephen Cole. Introduction to Metamathematics. Amsterdam: North-Holland, 1952.
KREISEL, Georg. A Survey of Proof Theory. Journal of Symbolic Logic, v. 33, n. 3, p. 321-388, 1968.
LAMBEK, Joachim; SCOTT, Philip J. Introduction to Higher Order Categorical Logic. Cambridge: Cambridge University Press, 1986.
LEITSCH, Alexander. The Resolution Calculus. Berlin: Springer, 1997.
MARTIN-LÖF, Per. Intuitionistic Type Theory. Naples: Bibliopolis, 1984.
MILLER, Dale; NADATHUR, Gopalan. Programming with Higher-Order Logic. Cambridge: Cambridge University Press, 2012.
MINTS, Grigori. A Short Introduction to Intuitionistic Logic. New York: Kluwer Academic, 2000.
MOREIRA, João Carlos. Lógica Matemática: Uma Introdução. Uberlândia: EDUFU, 2019.
NEGRI, Sara; VON PLATO, Jan. Structural Proof Theory. Cambridge: Cambridge University Press, 2001.
NORDSTRÖM, Bengt; PETERSSON, Kent; SMITH, Jan M. Programming in Martin-Löf's Type Theory. Oxford: Oxford University Press, 1990.
PAULSON, Lawrence C. ML for the Working Programmer. 2nd ed. Cambridge: Cambridge University Press, 1996.
PFENNING, Frank. Structural Cut Elimination. In: Logic in Computer Science. IEEE, 1995. p. 156-166.
PIERCE, Benjamin C. Types and Programming Languages. Cambridge: MIT Press, 2002.
POHLERS, Wolfram. Proof Theory: The First Step into Impredicativity. Berlin: Springer, 2009.
PRAWITZ, Dag. Natural Deduction: A Proof-Theoretical Study. Stockholm: Almqvist & Wiksell, 1965.
RATHJEN, Michael. The Art of Ordinal Analysis. In: International Congress of Mathematicians. Zürich: EMS, 2006. v. 2, p. 45-69.
RESTALL, Greg. An Introduction to Substructural Logics. London: Routledge, 2000.
ROBINSON, J. Alan. A Machine-Oriented Logic Based on the Resolution Principle. Journal of the ACM, v. 12, n. 1, p. 23-41, 1965.
SCHROEDER-HEISTER, Peter. A Natural Extension of Natural Deduction. Journal of Symbolic Logic, v. 49, n. 4, p. 1284-1300, 1984.
SCHÜTTE, Kurt. Proof Theory. Berlin: Springer-Verlag, 1977.
SCHWICHTENBERG, Helmut; WAINER, Stanley S. Proofs and Computations. Cambridge: Cambridge University Press, 2012.
SIMPSON, Stephen G. Subsystems of Second Order Arithmetic. 2nd ed. Cambridge: Cambridge University Press, 2009.
SMULLYAN, Raymond M. First-Order Logic. New York: Dover Publications, 1995.
SORENSEN, Morten Heine; URZYCZYN, Pawel. Lectures on the Curry-Howard Isomorphism. Amsterdam: Elsevier, 2006.
STATMAN, Richard. Lower Bounds on Herbrand's Theorem. Proceedings of the American Mathematical Society, v. 75, n. 1, p. 104-107, 1979.
TAKEUTI, Gaisi. Proof Theory. 2nd ed. Amsterdam: North-Holland, 1987.
TAIT, William W. Normal Derivability in Classical Logic. In: The Syntax and Semantics of Infinitary Languages. Berlin: Springer, 1968. p. 204-236.
TROELSTRA, Anne S.; SCHWICHTENBERG, Helmut. Basic Proof Theory. 2nd ed. Cambridge: Cambridge University Press, 2000.
TROELSTRA, Anne S.; VAN DALEN, Dirk. Constructivism in Mathematics. Amsterdam: North-Holland, 1988. 2 v.
UNIVALENT FOUNDATIONS PROGRAM. Homotopy Type Theory: Univalent Foundations of Mathematics. Princeton: Institute for Advanced Study, 2013.
VAN BENTHEM, Johan. A Manual of Intensional Logic. 2nd ed. Stanford: CSLI Publications, 1988.
VAN DALEN, Dirk. Logic and Structure. 5th ed. London: Springer, 2013.
VON PLATO, Jan. Elements of Logical Reasoning. Cambridge: Cambridge University Press, 2013.
WADLER, Philip. Propositions as Types. Communications of the ACM, v. 58, n. 12, p. 75-84, 2015.
WANSING, Heinrich. The Logic of Information Structures. Berlin: Springer, 1993.