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. 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 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.
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 onde B {\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 à ideia 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
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. 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
Restrições: Nas regras ( ∀ R ) {\displaystyle ({\forall }R)} e ( ∃ L ) {\displaystyle ({\exists }L)} , a variável y {\displaystyle y} não deve ocorrer livre dentro de Γ {\displaystyle \Gamma } e Δ {\displaystyle \Delta } . Alternativamente, a variável y {\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 (∧L1). 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.
Exemplos de derivações
Segue a derivação de " ⊢ A ∨ ¬ A {\displaystyle \vdash A\lor \lnot A} ", conhecida como a Lei do meio excluído. (tertium non datur em Latim). 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 ( ∀ R ) {\displaystyle (\forall R)} e ( ∃ L ) {\displaystyle (\exists L)} . Para algo mais interessante, provaremos que ( ( A → ( B ∨ C ) ) → ( ( ( B → ¬ A ) ∧ ¬ C ) → ¬ A ) ) {\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.
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.
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 A {\displaystyle A\,} segue semanticamente de um conjunto de premissas Γ {\displaystyle \Gamma \,} ( Γ ⊨ A ) {\displaystyle (\Gamma \vDash A)} se e somente se o sequente Γ ⊢ A {\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.
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 Γ , A ⊢ A , Δ {\displaystyle \Gamma ,A\vdash A,\Delta } pode ser concluído. Isto significa que A {\displaystyle A} prova A {\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.
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): O sistema resultante é chamado LJ. Isto é correto e completo com respeito à lógica intuicionista, e admite uma prova semelhante de eliminação do corte.
