Cálculo de sequentes

Na teoria da prova e lógica matemática, o cálculo de sequentes é um grupo de sistemas formais que compartilham de um certo estilo de inferência e propriedades formais. Os primeiros cálculos de sequente, os sistemas LK e LJ, foram introduzidos por Gerhard Gentzen em 1934 como uma ferramenta para o estudo de dedução natural na lógica de primeira ordem (nas versões clássica e intuicionista, respectivamente). O teorema de Gentzen chamado de "Teorema Principal" sobre LK e LJ foi o teorema do corte, um resultado com longo alcance nas consequências da metateoria, incluindo a consistência. Alguns anos depois, Gentzen demonstrou ainda mais o poder e a flexibilidade dessa técnica, aplicando o argumento da eliminação de corte para dar uma prova(transfinita) da consistência da aritmética de Peano, numa resposta surpreendente aos teoremas de incompletude de Gödel. Desde esse trabalho inicial, o cálculo de sequentes(também conhecido como sistemas de Gentzen) e os conceitos gerais relativos a ele são amplamente aplicados nos campos da teoria de prova, lógica matemática e dedução automática.

Introdução

Um meio de classificar diferentes estilos de sistemas de dedução é observando a forma de julgamentos no sistema, i.e., que coisas podem aparecer como conclusão de uma (sub)prova. A mais simples forma de julgamento é usada no estilo Hilbert de sistemas de dedução, onde o julgamento tem a forma

${\displaystyle B\,}$

onde ${\displaystyle B}$ é qualquer fórmula da lógica de primeira ordem(ou que a lógica de sistemas de dedução se aplica, e.g., cálculo proposicional ou lógica de ordem superior ou lógica modal). Os teoremas são aquelas fórmulas que aparecem como um julgamento conclusivo em uma prova válida. Um sistema de Hilbert não precisa de distinção entre fórmulas e julgamentos, fazemos aqui apenas uma comparação para os casos que seguem. O preço pago pela sintaxe simples de um sistema de Hilbert é que as provas formais completas tendem a ficar extremamente longas. Argumentos concretos sobre provas em tal sistema quase sempre apelam para o teorema da dedução.Isso leva à idéia de incluir o teorema da dedução como uma regra formal no sistema, o que acontece em dedução natural. Na dedução natural, julgamentos têm a forma

${\displaystyle A_{1},A_{2},\ldots ,A_{n}\vdash B}$

onde o ${\displaystyle A_{i}}$'s e ${\displaystyle B}$ são novamente fórmulas e ${\displaystyle n\geq 0}$. Ou seja, um julgamento consiste numa lista(possivelmente vazia) de fórmulas no lado esquerdo do símbolo da derivabilidade, e uma simples fórmula ao lado direito.Os teoremas são aquelas fórmulas ${\displaystyle B}$ tais que ${\displaystyle \vdash B}$ (com o lado esquerdo vazio) são a conclusão de uma prova válida. Em algumas apresentações da dedução natural o ${\displaystyle A_{i}}$s o "deriva em" não é escrito explicitamente; apesar de uma notação bidimensional em que eles podem ser inferidos ser usada.

A semântica padrão de um julgamento em dedução natural é que ele afirma que sempre que^[1] ${\displaystyle A_{1}}$, ${\displaystyle A_{2}}$, etc., são todas verdade, ${\displaystyle B}$ também será. Os julgamentos : ${\displaystyle A_{1},\ldots ,A_{n}\vdash B\quad {\mbox{e}}\quad \vdash (A_{1}\land \cdots \land A_{n})\rightarrow B}$ são equivalentes no sentido de que uma forte prova de um deles pode ser expandida para a prova do outro. Finalmente, o "Cálculo de Sequentes" generaliza a forma do julgamento da dedução natural

${\displaystyle A_{1},\ldots ,A_{n}\vdash B_{1},\ldots ,B_{k},}$

um objeto sintático chamado de sequente. As fórmulas do lado esquerdo do símbolo da derivabilidade são chamadas de antecedentes, e as fórmulas do lado direito são chamadas de sucedentes; e juntos são chamados de "cedentes". De novo, ${\displaystyle A_{i}}$ e ${\displaystyle B_{i}}$ são fórmulas, e${\displaystyle n}$ e ${\displaystyle k}$ são inteiros não negativos, isto é, no lado esquerdo ou no lado direito(nenhum ou ambos) podem estar vazios. Como em dedução natural, teoremas são esses ${\displaystyle B}$ onde ${\displaystyle \vdash B}$ é a conclusão de uma prova válida. O sequente vazio, tendo ambos os cedentes vazios, está definido para ser falso. A semântica padrão de um sequente é a afirmativa de que sempre "todo" ${\displaystyle A_{i}}$ for verdade, pelo menos um ${\displaystyle B_{i}}$ também vai ser verdade. Uma forma de expressar isto é que uma vírgula do lado esquerdo do símbolo da derivabilidade deve ser pensada como um "e", e um vírgula do lado direito do do símbolo da derivabilidade deve ser pensada como um (inclusive) "ou". Os sequentes

${\displaystyle A_{1},\ldots ,A_{n}\vdash B_{1},\ldots ,B_{k}\quad {\mbox{e}}\quad \vdash (A_{1}\land \cdots \land A_{n})\rightarrow (B_{1}\lor \cdots \lor B_{k})}$

são equivalentes no sentido de que uma forte prova de um deles pode ser expandida para a prova do outro.

À primeira vista, esta extensão da forma de julgamento pode parecer ser uma complicação estranha - não é motivado por um defeito óbvio de dedução natural, e é inicialmente confuso que a vírgula possa significar coisas totalmente diferentes nos dois lados do símbolo da derivabilidade. No entanto, no contexto da lógica clássica a semântica da subsequente também pode (por tautologia proposicional) ser expressa como

${\displaystyle \vdash \neg A_{1}\lor \neg A_{2}\lor \cdots \lor \neg A_{n}\lor B_{1}\lor B_{2}\lor \cdots \lor B_{k}}$

(pelo menos um dos As é falso, ou um dos Bs é verdadeiro) ou como

${\displaystyle \vdash \neg (A_{1}\land A_{2}\land \cdots \land A_{n}\land \neg B_{1}\land \neg B_{2}\land \cdots \land \neg B_{k})}$

(que não pode ser o caso de que todo os As são verdadeiros e todos os Bs são falsos). Nestas formulações, a única diferença entre as fórmulas de ambos os lados da derivabilidade é que um lado é negado. Assim, a troca foi para a direita em um sequentes corresponde a negar todas as fórmulas constituintes. Isto significa que uma simetria como Leis de De Morgan, que se manifesta como negação lógica no nível semântico, se traduz diretamente em uma simetria esquerda-direita de sequentes - e de fato, as regras de inferência no cálculo de sequentes para lidar com conjunto (∧) são imagens daqueles que lidam com a disjunção (∨). Muitos lógicos sentem que esta apresentação simétrica oferece uma visão mais profunda na estrutura da lógica do que outros estilos de sistema de prova, onde a dualidade clássica da negação não é tão aparente nas regras.

O sistema LK

Essa seção introduz as regras de cálculo de sequentes "LK" (Que é uma abreviação para “logistischer klassischer Kalkül”), como introduzido por Gentzen em 1934. ^[2] Uma prova (formal) nesse cálculo de sequentes é uma sequência de sequentes, onde cada um dos sequentes são derivados dos sequentes que aparecem antes na sequência usando uma das regras de inferência abaixo.

Regras de Inferência

A seguinte notação será usada:

• ${\displaystyle \vdash }$ conhecido como símbolo da derivabilidade, separa os pressupostos à esquerda e as proposições à direita.
• ${\displaystyle A}$ e ${\displaystyle B}$ denotam fórmulas de primeira ordem na lógica de predicados (Pode-se também restringir essa a lógica proposicional).
• ${\displaystyle \Gamma ,\Delta ,\Sigma }$, and ${\displaystyle \Pi }$ são finitos (possivelmente vazias) sequências de fórmulas (De fato, a ordem das fórmulas não importam.; chamados contextos,
  • quando na “esquerda” do ${\displaystyle \vdash }$, a sequência de fórmulas é considerada “conjuntivamente” (todas assumidas ao mesmo tempo),
  • enquanto na “direita” do ${\displaystyle \vdash }$, a sequência de fórmulas é considerada “disconjuntivamente” (pelo menos uma das fórmulas deve ser mantida para alguma atribuição de variável),
• ${\displaystyle t}$ denota um termo arbitrário,
• ${\displaystyle x}$ e ${\displaystyle y}$ denotam variáveis,
• ${\displaystyle A[t/x]}$ denota a fórmula que é obtida pela substituição do termo ${\displaystyle t}$ por qualquer ocorrência livre da variável ${\displaystyle x}$ na fórmula ${\displaystyle A}$,

• uma variável é dita para ocorrer livre dentro de uma fórmula se ela ocorre fora do escopo de quantificadores ${\displaystyle \forall }$ ou ${\displaystyle \exists }$.
• ${\displaystyle WL}$ e ${\displaystyle WR}$ representam Enfraquecimento esquerda/direita, ${\displaystyle CL}$ e ${\displaystyle CR}$ Contração" e ${\displaystyle PL}$ e ${\displaystyle PR}$ Permutação.

Axioma:	Corte:
${\displaystyle {\cfrac {\qquad }{A\vdash A}}\quad (I)}$	${\displaystyle {\cfrac {\Gamma \vdash \Delta ,A\qquad A,\Sigma \vdash \Pi }{\Gamma ,\Sigma \vdash \Delta ,\Pi }}\quad ({\mathit {Cut}})}$
Regras lógicas à esquerda:	Regras lógicas à direita:
${\displaystyle {\cfrac {\Gamma ,A\vdash \Delta }{\Gamma ,A\land B\vdash \Delta }}\quad ({\land }L_{1})}$	${\displaystyle {\cfrac {\Gamma \vdash A,\Delta }{\Gamma \vdash A\lor B,\Delta }}\quad ({\lor }R_{1})}$
${\displaystyle {\cfrac {\Gamma ,B\vdash \Delta }{\Gamma ,A\land B\vdash \Delta }}\quad ({\land }L_{2})}$	${\displaystyle {\cfrac {\Gamma \vdash B,\Delta }{\Gamma \vdash A\lor B,\Delta }}\quad ({\lor }R_{2})}$
${\displaystyle {\cfrac {\Gamma ,A\vdash \Delta \qquad \Sigma ,B\vdash \Pi }{\Gamma ,\Sigma ,A\lor B\vdash \Delta ,\Pi }}\quad ({\lor }L)}$	${\displaystyle {\cfrac {\Gamma \vdash A,\Delta \qquad \Sigma \vdash B,\Pi }{\Gamma ,\Sigma \vdash A\land B,\Delta ,\Pi }}\quad ({\land }R)}$
${\displaystyle {\cfrac {\Gamma \vdash A,\Delta \qquad \Sigma ,B\vdash \Pi }{\Gamma ,\Sigma ,A\rightarrow B\vdash \Delta ,\Pi }}\quad ({\rightarrow }L)}$	${\displaystyle {\cfrac {\Gamma ,A\vdash B,\Delta }{\Gamma \vdash A\rightarrow B,\Delta }}\quad ({\rightarrow }R)}$
${\displaystyle {\cfrac {\Gamma \vdash A,\Delta }{\Gamma ,\lnot A\vdash \Delta }}\quad ({\lnot }L)}$	${\displaystyle {\cfrac {\Gamma ,A\vdash \Delta }{\Gamma \vdash \lnot A,\Delta }}\quad ({\lnot }R)}$
${\displaystyle {\cfrac {\Gamma ,A[t/x]\vdash \Delta }{\Gamma ,\forall xA\vdash \Delta }}\quad ({\forall }L)}$	${\displaystyle {\cfrac {\Gamma \vdash A[y/x],\Delta }{\Gamma \vdash \forall xA,\Delta }}\quad ({\forall }R)}$
${\displaystyle {\cfrac {\Gamma ,A[y/x]\vdash \Delta }{\Gamma ,\exists xA\vdash \Delta }}\quad ({\exists }L)}$	${\displaystyle {\cfrac {\Gamma \vdash A[t/x],\Delta }{\Gamma \vdash \exists xA,\Delta }}\quad ({\exists }R)}$
Regras estruturais à esquerda:	Regras estruturais à direita:
${\displaystyle {\cfrac {\Gamma \vdash \Delta }{\Gamma ,A\vdash \Delta }}\quad ({\mathit {WL}})}$	${\displaystyle {\cfrac {\Gamma \vdash \Delta }{\Gamma \vdash A,\Delta }}\quad ({\mathit {WR}})}$
${\displaystyle {\cfrac {\Gamma ,A,A\vdash \Delta }{\Gamma ,A\vdash \Delta }}\quad ({\mathit {CL}})}$	${\displaystyle {\cfrac {\Gamma \vdash A,A,\Delta }{\Gamma \vdash A,\Delta }}\quad ({\mathit {CR}})}$
${\displaystyle {\cfrac {\Gamma _{1},A,B,\Gamma _{2}\vdash \Delta }{\Gamma _{1},B,A,\Gamma _{2}\vdash \Delta }}\quad ({\mathit {PL}})}$	${\displaystyle {\cfrac {\Gamma \vdash \Delta _{1},A,B,\Delta _{2}}{\Gamma \vdash \Delta _{1},B,A,\Delta _{2}}}\quad ({\mathit {PR}})}$

Restrições: Nas regras ${\displaystyle ({\forall }R)}$ e ${\displaystyle ({\exists }L)}$, a variável ${\displaystyle y}$ não deve ocorrer livre dentro de ${\displaystyle \Gamma }$ e ${\displaystyle \Delta }$. Alternativamente, a variável ${\displaystyle y}$ não deve aparecer em nenhum lugar nos sequentes abaixo dele.”

Uma explicação intuitiva

As regras acima podem ser divididas em dois grupos principais: o grupo “lógico” e o “estrutural”. Cada uma das regras lógicas introduz uma nova fórmula tanto no lado esquerdo quanto do direito da derivabilidade(${\displaystyle \vdash }$). Em contraste, as regras estruturais agem na estrutura de sequentes, ignorando a forma exata da fórmula. As duas exceções para esse esquema geral é o axioma da identidade (I) e a regra do corte.

Ainda que estabelecidas de um jeito formal, as regras acima permitem uma leitura muito intuitiva em termos da lógica clássica. Considere, por exemplo, a regra (∧L₁). Ela diz que, sempre que alguém pode provar que Δ pode ser deduzido de alguma sequência de fórmulas que contém A, então também pode deduzir Δ da (mais forte) assunção, que tem A∧B. Da mesma forma, a regra (¬R) estabelece que, se Γ e A são suficientes para concluir Δ, então de Γ sozinho alguém pode ainda concluir Δ ou A deve ser falso, isto é ¬A mantém a validade. Todas as regras podem ser interpretadas dessa forma.

Para uma intuição sobre o quantificador das regras, considere a regra (∀R). Concluindo é claro que ∀x A vem apenas do fato que A[y/x] é verdadeiro não é em geral possível. Se, entretanto, a variável y não é mencionada em mais nenhum lugar, (isto é, ela ainda pode ser escolhida livremente, sem influenciar outras formulas), então podemos assumir que A[y/x] vale para qualquer valor de y. As outras regras devem então ser bastante simples.

Ao contrário da visão das regras como descrições para derivações em lógica de predicados, podemos também considera-las como instruções para a construção de uma prova para um dado comando. Neste caso as regras devem ser lidas de baixo pra cima; por exemplo, (∧R) diz que, para provar que A∧B deriva de assumir Γ e Σ, isto basta para provar que A pode ser deduzida de Γ e B pode ser deduzido de Σ, respectivamente. Note que, dado algum fato antecedente, não é Claro como isto pode ser dividido em Γ e Σ. Entretanto, há possibilidades finitas para serem verificadas desde que o antecedente é assumido finito. Isto também ilustra como uma prova teórica pode ser vista como operadores em prova de uma maneira combinatória: dadas provas para A e B, podemos construir a prova para A∧B.

Olhando para alguma prova, a maioria das regras oferecem mais ou menos receitas diretas de como faze-la. A regra de corte é diferente: estabelece que, quando a formula A pode ser deduzida e esta formula também serve como premissa para deduzir outros comandos, então a fórmula A pode ser cortada e as respectivas derivações são agregadas. Quando construindo a fórmula de baixo pra cima, esta cria o problema de adivinhar A (desde que não tenha aparecido até então). O teorema da elinação do corte é então crucial para a aplicação do cálculo sequente em dedução automática: ela estabelece que todas as utilizações da regra de corte podem ser eliminadas de uma prova, implicando que qualquer sequente passível de prova pode ser dado com uma prova livre de corte.

A segunda regra que de alguma forma especial é o axioma da identidade (I). A leitura intuitiva disso é óbvia: cada fórmula prova a si mesma. Como a regra de corte, o axioma da identidade é algo redundante: a completeza atômica dos sequentes iniciais estabelecem que a regra pode ser restrita para fórmulas atômicas sem qualquer perda de capacidade de comprovação.

Observe que todas as regras têm companheiras espelho, exceto aquelas de implicação. Isto reflete o que de que uma linguagem usual de lógica de primeira ordem não inclui o conectivo “não é implicado por” ${\displaystyle \not \leftarrow }$ que deveria ser a implicação dual de De Morgan. Adicionando tal conectivo suas regras naturais poderiam fazer o cálculo completamente simétrico da esquerda para a direita.

Exemplos de derivações

Segue a derivação de "${\displaystyle \vdash A\lor \lnot A}$", conhecida como a Lei do meio excluído. (tertium non datur em Latim).

		${\displaystyle (I)}$
${\displaystyle A\vdash A}$
		${\displaystyle (\lnot R)}$
${\displaystyle \vdash \lnot A,A}$
		${\displaystyle (\lor R_{2})}$
${\displaystyle \vdash A\lor \lnot A,A}$
		${\displaystyle (PR)}$
${\displaystyle \vdash A,A\lor \lnot A}$
		${\displaystyle (\lor R_{1})}$
${\displaystyle \vdash A\lor \lnot A,A\lor \lnot A}$
		${\displaystyle (CR)}$
${\displaystyle \vdash A\lor \lnot A}$

A seguir está a prova de um simples fato envolvendo quantificadores. Note que o oposto não é verdadeiro, e que a não veracidade pode ser vista quando se tenta derivar de baixo pra cima, porque a existência de uma variável livre não pode ser usada em substituição nas regras ${\displaystyle (\forall R)}$ e ${\displaystyle (\exists L)}$.

		${\displaystyle (I)}$
${\displaystyle p(x,y)\vdash p(x,y)}$
		${\displaystyle (\forall L)}$
${\displaystyle \forall x\left(p(x,y)\right)\vdash p(x,y)}$
		${\displaystyle (\exists R)}$
${\displaystyle \forall x\left(p(x,y)\right)\vdash \exists y\left(p(x,y)\right)}$
		${\displaystyle (\exists L)}$
${\displaystyle \exists y\left(\forall x\left(p(x,y)\right)\right)\vdash \exists y\left(p(x,y)\right)}$
		${\displaystyle (\forall R)}$
${\displaystyle \exists y\left(\forall x\left(p(x,y)\right)\right)\vdash \forall x\left(\exists y\left(p(x,y)\right)\right)}$

Para algo mais interessante, provaremos que ${\displaystyle \left(\left(A\rightarrow \left(B\lor C\right)\right)\rightarrow \left(\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right)\rightarrow \lnot A\right)\right)}$. É direto encontrar a derivação, que exemplifica a utilidade de LK em comprovação automática.

${\displaystyle (I)}$ ${\displaystyle A\vdash A}$     ${\displaystyle (\lnot R)}$ ${\displaystyle \vdash \lnot A,A}$     ${\displaystyle (PR)}$ ${\displaystyle \vdash A,\lnot A}$              ${\displaystyle (I)}$ ${\displaystyle B\vdash B}$              ${\displaystyle (I)}$ ${\displaystyle C\vdash C}$         ${\displaystyle (\lor L)}$ ${\displaystyle B\lor C\vdash B,C}$     ${\displaystyle (PR)}$ ${\displaystyle B\lor C\vdash C,B}$     ${\displaystyle (\lnot L)}$ ${\displaystyle B\lor C,\lnot C\vdash B}$              ${\displaystyle (I)}$ ${\displaystyle \lnot A\vdash \lnot A}$         ${\displaystyle (\rightarrow L)}$ ${\displaystyle \left(B\lor C\right),\lnot C,\left(B\rightarrow \lnot A\right)\vdash \lnot A}$     ${\displaystyle (\land L_{1})}$ ${\displaystyle \left(B\lor C\right),\lnot C,\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right)\vdash \lnot A}$     ${\displaystyle (PL)}$ ${\displaystyle \left(B\lor C\right),\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right),\lnot C\vdash \lnot A}$     ${\displaystyle (\land L_{2})}$ ${\displaystyle \left(B\lor C\right),\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right),\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right)\vdash \lnot A}$     ${\displaystyle (CL)}$ ${\displaystyle \left(B\lor C\right),\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right)\vdash \lnot A}$     ${\displaystyle (PL)}$ ${\displaystyle \left(\left(B\rightarrow \lnot A\right)\land \lnot C\right),\left(B\lor C\right)\vdash \lnot A}$		${\displaystyle (\rightarrow L)}$
${\displaystyle \left(\left(B\rightarrow \lnot A\right)\land \lnot C\right),\left(A\rightarrow \left(B\lor C\right)\right)\vdash \lnot A,\lnot A}$
		${\displaystyle (CR)}$
${\displaystyle \left(\left(B\rightarrow \lnot A\right)\land \lnot C\right),\left(A\rightarrow \left(B\lor C\right)\right)\vdash \lnot A}$
		${\displaystyle (PL)}$
${\displaystyle \left(A\rightarrow \left(B\lor C\right)\right),\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right)\vdash \lnot A}$
		${\displaystyle (\rightarrow R)}$
${\displaystyle \left(A\rightarrow \left(B\lor C\right)\right)\vdash \left(\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right)\rightarrow \lnot A\right)}$
		${\displaystyle (\rightarrow R)}$
${\displaystyle \vdash \left(\left(A\rightarrow \left(B\lor C\right)\right)\rightarrow \left(\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right)\rightarrow \lnot A\right)\right)}$

Essas derivações também enfatizam a estrutura estritamente formal do cálculo de sequentes. Por exemplo, as regras lógicas como definidas acima sempre agem em uma fórmula imediatamente adjacente a derivabilidade, tal que a permutação de regras seja necessária. Note entretanto, que ela é parte de um artefato de apresentação, no estilo original de Gentzen. Uma simplificação simples envolve o uso de vários conjuntos de fórmulas na interpretação do sequente, ao contrário de sequências, eliminando a necessidade de uma regra explícita de permutação. Isso corresponde a mudar a comutatividade de presunções e derivações fora do cálculo de sequentes, onde LK incorpora no próprio sistema.

Regras estruturais

As regras estruturais merecem alguma discussão adicional.

O enfraquecimento (W) permite a adição de um elemento arbitrário a uma sequência. Intuitivamente, isso é permitido no antecedente porque nós sempre podemos restringir o escopo da nossa prova (se todos os carros têm rodas, então é seguro dizer que todos os carros pretos têm roda); e no sucessivo porque nós podemos sempre permitir conclusões alternativas (se todos os carros têm rodas, então é seguro dizer que todos os carros têm rodas ou asas).

Contração (C) e Permutação (P) asseguram que nem a ordem (P) nem a multiplicidade de ocorrências (C ) de elementos das sequencias importam. Entretanto, alguém poderia ao invés das sequências também considerar os conjuntos.

O esforço extra do uso de sequências, entretanto, é justificado desde que toda as regras estruturais ou parte devem ser omitidas. Dessa forma, se obtém as chamadas lógicas substruturais.

Propriedades do sistema LK

Este sistema de regras pode ser mostrado ao mesmo tempo como um sistema correto e completo com respeito à lógica de primeira ordem, ou seja, um comando ${\displaystyle A\,}$ segue semanticamente de um conjunto de premissas ${\displaystyle \Gamma \,}$ ${\displaystyle (\Gamma \vDash A)}$ se e somente se o sequente ${\displaystyle \Gamma \vdash A}$ pode ser derivado das regras acima.

No cálculo de sequentes, a regra do corte é admissível. Este resultado é também conhecido como o Teorema Principal de Gentzen.

Variantes

As regras acima podem ser mudadas em várias formas:

Alternativas estruturais menores

Há alguma liberdade de escolha com referência aos detalhes de como sequentes e regras estruturais são formalizados. Tanto quanto cada derivação no sistema LK pode ser transformado em uma derivação usando as novas regras e vice-versa, as regras modificadas podem ainda ser chamadas de LK.

Primeiro de tudo, como mencionado acima, os sequentes podem ser vistos como conjuntos ou vários conjuntos. Neste caso, as regras de permuta e (quando usados conjuntos) fórmulas de contração são obsoletos.

A regra de enfraquecimento se tornará admissível, quando o axioma (I) é mudado, tal que qualquer sequente da forma ${\displaystyle \Gamma ,A\vdash A,\Delta }$ pode ser concluído. Isto significa que ${\displaystyle A}$ prova ${\displaystyle A}$ em qualquer contexto. Qualquer enfraquecimento que apareça em uma derivação pode então ser realizada à direita do início. Esta pode ser uma mudança conveniente quando se está construindo provas de baixo pra cima.

Independente deste caso pode também mudar a forma em que contextos são divididos dentro das regras: Nos casos (∧R), (∨L), e (→L) o contexto da esquerda é de alguma forma dividida dentro de Γ e Σ quando se está subindo. Desde que a contração permite a duplicação deste, alguém pode assumir que o contexto completo é usado em ambos os braços de derivação.

Lógica Substrutural

Alternativamente, alguém pode restringir ou proibir o uso de algumas regras estruturais. Isto dá uma variedade de sistemas de subestrutura lógica. Eles são genericamente mais fracos que os LK (isto é, eles têm ainda menos teoremas) e portanto não completo com respeito aos padrões semânticos da lógica de primeira ordem. Entretanto, eles têm outras propriedades interessantes que têm aplicação em ciência da computação teórica e inteligência articicial.

Cálculo de sequentes intuitivo: Sistema LJ

Surpreendentemente, algumas mudanças nas regras de LK bastam para torna-la um sistema de provas para lógica intuitiva. Para este fim, temos que restringir os sequentes com exatamente uma fórmula no lado direito e modificar as regras para manter estes sequentes invariantes. Por exemplo, (∨L) é reformulado para (onde C é uma fórmula arbitrária):

${\displaystyle {\cfrac {\Gamma ,A\vdash C\qquad \Sigma ,B\vdash C}{\Gamma ,\Sigma ,A\lor B\vdash C}}\quad ({\lor }L)}$

O sistema resultante é chamado LJ. Isto é correto e completo com respeito à lógica intuicionista, e admite uma prova semelhante de eliminação do corte.

Notas

1. Aqui, "sempre" é usada como uma abreviação informal "para cada atribuição de valores para as variáveis livres no julgamento""
2. Gentzen, Gerhard (1934–1935). «Untersuchungen über das logische Schließen. I». Mathematische Zeitschrift. 39 (2): 191. doi:10.1007/BF01201353 

Referências

• Girard, Jean-Yves; Paul Taylor, Yves Lafont (1990) [1989]. Proofs and Types. [S.l.]: Cambridge University Press (Cambridge Tracts in Theoretical Computer Science, 7). ISBN 0-521-37181-3  A referência emprega parâmetros obsoletos |coautor= (ajuda)
• Samuel R. Buss (1998). «An introduction to proof theory». In: Samuel R. Buss. Handbook of proof theory. [S.l.]: Elsevier. pp. 1–78. ISBN 0-444-89840-9 

Ligações externas

• A Brief Diversion: Sequent Calculus
• Interactive tutorial of the Sequent Calculus