Sequente

Na teoria da prova, um sequente é uma declaração formalizada de verificação que é frequentemente usada quando se está especificando cálculo para o método dedutivo. No cálculo de sequentes, o nome sequente é usado para representar uma estrutura que pode ser considerada como um tipo específico de julgamento, característico do cálculo de sequentes.

Explicação

Sequentes tem o formato

$\Gamma \vdash \Sigma$

onde tanto Γ como Σ são sequências de fórmulas lógicas (i.e., tanto o número como a ordem das fórmulas são levados em consideração). Normalmente, nos referimos ao símbolo $\vdash$ como Catraca que, geralmente, é lido/interpretado como "prova" ou "acarreta". O referido símbolo não pertence à linguagem, mas sim à metalinguagem utilizada na discussão de provas. Em um sequente, Γ é chamado de antecedente e Σ é chamado de sucedente.

Significado Intuitivo

O significado intuitivo de um sequente $\Gamma \vdash \Sigma$ é tal que, sob a suposição de Γ, a conclusão de Σ é demonstrável. Classicamente, as fórmulas à esquerda da catraca podem ser interpretadas como uma conjunção, enquanto as fórmulas à direita podem ser consideradas como uma disjunção. Isso significa que se todas as fórmulas no conjunto Γ forem verdadeiras, então pelo menos uma fórmula em Σ também há de ser verdadeira. Caso o sucedente for vazio, interpretamos tal situação como falsidade, i.e. $\Gamma \vdash$ significa que Γ prova/acarreta falsidade e, portanto, é inconsistente. Por outro lado, assumimos um antecedente vazio como sendo verdadeiro, i.e. $\vdash \Sigma$ significa que Σ procede sem quaisquer suposições, ou seja, a disjunção é sempre verdadeira. Um sequente no formato $\vdash \Sigma$ é tido como uma assertiva lógica.

Outras explicações intuitivas equivalentes são possíveis. Por exemplo, $\Gamma \vdash \Sigma$ pode ser lido como uma assertiva de que não é possível que ocorra um caso no qual todas as fórmulas em Γ sejam verdadeiras e todas as fórmulas em Σ sejam falsas (isso está relacionado com a regra de inferência da dupla negação).

Em qualquer caso, essas leituras intuitivas são de propósito meramente pedagógico. Como as provas formais na teoria da prova são puramente sintáticas, a semântica de (ou da derivação de) um sequente é dada apenas pelas propriedades do cálculo que dita as regras de inferência.

Salvo quaisquer contradições na definição técnica precisa dada acima, podemos descrever sequentes na forma lógica introdutória dos mesmos. A expressão $\Gamma$ representa um conjunto de suposições com as quais começamos nosso processo lógico. Por exemplo: "Socrátes é humano" e "Todos os humanos são mortais". O símbolo $\Sigma$ representa uma conclusão lógica que é fruto dessas premissas. Por exemplo: a conclusão "Socrates é mortal" é fruto de uma formalização razoável das premissas previamente citadas, e, portanto, pode ser inserida no lado direito, $\Sigma$, da catraca. Sendo assim, o símbolo $\vdash$ pode ser interpretado como o processo de raciocínio, ou "portanto" em português.

Exemplo

Um típico sequente pode ser:

$\phi ,\psi \vdash \alpha ,\beta$

Esse sequente afirma que ou $\alpha$ ou $\beta$ podem ser demonstradas a partir de $\phi$ e $\psi$.

Propriedade

Como toda fórmula no antecedente (lado esquerdo da catraca) há de ser verdadeiro para que possamos concluir como verdadeira pelo menos uma das fórmulas presentes no sucedente (lado direito da catraca), o ato de adicionar fórmulas a qualquer um dos lados resulta em um sequente mais fraco, enquanto o ato de remover fórmulas de qualquer um dos lados resulta em um sequente mais forte.

Regras

A maioria dos sistemas de prova provém maneiras para deduzir um sequente a partir de outro. Essas regras de inferência são escritas com uma lista de sequentes acima e abaixo de uma linha. Essa regra indica que, se tudo acima da linha é verdadeiro, então tudo abaixo da linha também é verdadeiro.

Uma típica regra é:

${\frac {\Gamma ,\alpha \vdash \Sigma \qquad \Gamma \vdash \Sigma ,\alpha }{\Gamma \vdash \Sigma }}$

Esse exemplo indica que, se é possível deduzir que $\Gamma ,\alpha$ acarreta em $\Sigma$ e que $\Gamma$ acarreta em $\Sigma ,\alpha$, então é possível também deduzir que $\Gamma$ acarreta em $\Sigma$.

Variações

A noção geral de um sequente, introduzida nesse artigo, pode ser especializada de diversas maneiras. Um sequente é dito um sequente intuicionístico se existe no máximo uma fórmula no sucedente. Essa forma é necessária para se obter métodos de cálculo para a lógica intuicionista. Similarmente, pode-se obter métodos de cálculo para a lógica intuicionista dual, que é um tipo de lógica paraconsistente, exigindo que os sequentes possuam apenas uma fórmula no antecedente.

Em vários casos, também é assumido que sequentes consistem em multiconjuntos ou conjuntos ao invés de sequências matemáticas. Sendo assim, é possível desconsiderar a ordem ou até mesmo o número de ocorrências das fórmulas. Para a lógica proposicional isso não representa um problema, vez que as conclusões que podem ser tiradas a partir de uma coleção de premissas não dependem desses dados. Na lógica subestrutural, porém, esses dados podem ter certa importância.

História

Historicamente, sequentes foram introduzidos por Gerhard Gentzen, com o objetivo de especificar o famoso cálculo de sequentes. A palavra usada originalmente foi a palavra alemã Sequenz. Na língua inglesa, porém, a palavra Sequence já é tida como uma tradução para a palavra alemã Folge, e é utilizada frequentemente na matemática. O termo Sequent, portanto, foi criado como uma tradução alternativa da expressão em alemão. De forma similar, na língua portuguesa, utilizou-se o termo "Sequente".

Ver também

• Logica intuicionista
• Gerhard Gentzen
• Cálculo de sequentes