Mostrar código-fonte de Sequente

Na [[teoria da prova]], um sequente é uma declaração [[Formalismo|formalizada]] de [[Verificação formal|verificação]] que é frequentemente usada quando se está especificando [[Cálculos de prova|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
:<math>\Gamma\vdash\Sigma</math>
onde tanto Γ como Σ são [[Sequência (matemática)|sequências]] de fórmulas [[Lógica matemática|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 <math>\vdash</math> 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 <math>\Gamma\vdash\Sigma</math> é 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 lógica|conjunção]], enquanto as fórmulas à direita podem ser consideradas como uma [[Disjunção lógica|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. <math>\Gamma\vdash</math> significa que Γ prova/acarreta [[falsidade]] e, portanto, é [[Inconsistência|inconsistente]]. Por outro lado, assumimos um antecedente vazio como sendo verdadeiro, i.e. <math>\vdash\Sigma</math> significa que Σ procede sem quaisquer suposições, ou seja, a disjunção é sempre verdadeira. Um sequente no formato <math>\vdash\Sigma</math> é tido como uma [[assertiva lógica]].

Outras explicações intuitivas equivalentes são possíveis. Por exemplo, <math>\Gamma\vdash\Sigma</math> 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 [[Sintaxe|sintáticas]], a [[semântica]] de (ou da derivação de) um sequente é dada apenas pelas propriedades do [[Cálculo de sequentes|cálculo]] que dita as [[Regra de inferência|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 <math>\Gamma</math> 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 <math>\Sigma</math> 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, <math>\Sigma</math>,  da ''catraca''. Sendo assim, o símbolo <math>\vdash</math> pode ser interpretado como o processo de raciocínio, ou "portanto" em português.

== Exemplo ==

Um típico sequente pode ser:

:<math> \phi,\psi\vdash\alpha,\beta</math>

Esse sequente afirma que ou <math>\alpha</math> ou <math>\beta</math> podem ser demonstradas a partir de <math>\phi</math> e <math>\psi</math>.

== 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 [[Regra de inferência|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 é:

:<math> \frac{\Gamma,\alpha\vdash\Sigma\qquad \Gamma\vdash\Sigma,\alpha}{\Gamma\vdash\Sigma}</math>

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

== 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 [[multiconjunto]]s ou [[conjuntos]] ao invés de [[Sequência (matemática)|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]]

{{esboço-lógica}}

[[Category:Lógica matemática]]
[[Category:Teoria da computação]]