Nateoria da prova, um sequente é uma declaraçãoformalizada deverificação que é frequentemente usada quando se está especificando cálculo para ométodo dedutivo. Nocálculo de sequentes, o nome sequente é usado para representar uma estrutura que pode ser considerada como um tipo específico dejulgamento, característico do cálculo de sequentes.

Sequentes tem o formato

${\displaystyle \mathrm{\Gamma }⊢\mathrm{\Sigma }}$

onde tanto Γ como Σ sãosequências de fórmulasló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${\displaystyle ⊢}$ comoCatraca 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.

O significado intuitivo de um sequente${\displaystyle \mathrm{\Gamma }⊢\mathrm{\Sigma }}$ é tal que, sob a suposição de Γ, a conclusão de Σ é demonstrável.Classicamente, as fórmulas à esquerda dacatraca podem ser interpretadas como umaconjunção, enquanto as fórmulas à direita podem ser consideradas como umadisjunçã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 comofalsidade, i.e.${\displaystyle \mathrm{\Gamma }⊢}$ significa que Γ prova/acarretafalsidade e, portanto, éinconsistente. Por outro lado, assumimos um antecedente vazio como sendo verdadeiro, i.e.${\displaystyle ⊢\mathrm{\Sigma }}$ significa que Σ procede sem quaisquer suposições, ou seja, a disjunção é sempre verdadeira. Um sequente no formato${\displaystyle ⊢\mathrm{\Sigma }}$ é tido como umaassertiva lógica.

Outras explicações intuitivas equivalentes são possíveis. Por exemplo,${\displaystyle \mathrm{\Gamma }⊢\mathrm{\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 dadupla negação).

Em qualquer caso, essas leituras intuitivas são de propósito meramente pedagógico. Como as provas formais nateoria da prova são puramentesintáticas, asemântica de (ou da derivação de) um sequente é dada apenas pelas propriedades docálculo que dita asregras de inferência.

Salvo quaisquer contradições na definição técnica precisa dada acima, podemos descrever sequentes naforma lógica introdutória dos mesmos. A expressão${\displaystyle \mathrm{\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${\displaystyle \mathrm{\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,${\displaystyle \mathrm{\Sigma }}$, dacatraca. Sendo assim, o símbolo${\displaystyle ⊢}$ pode ser interpretado como o processo de raciocínio, ou "portanto" em português.

Um típico sequente pode ser:

${\displaystyle \varphi ,\psi ⊢\alpha ,\beta }$

Esse sequente afirma que ou${\displaystyle \alpha }$ ou${\displaystyle \beta }$ podem ser demonstradas a partir de${\displaystyle \varphi }$ e${\displaystyle \psi }$.

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

A maioria dos sistemas de prova provém maneiras para deduzir um sequente a partir de outro. Essasregras 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 é:

${\displaystyle \frac{\mathrm{\Gamma },\alpha ⊢\mathrm{\Sigma }\mathrm{\Gamma }⊢\mathrm{\Sigma },\alpha }{\mathrm{\Gamma }⊢\mathrm{\Sigma }}}$

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

A noção geral de um sequente, introduzida nesse artigo, pode ser especializada de diversas maneiras. Um sequente é dito umsequente 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 alógica intuicionista. Similarmente, pode-se obter métodos de cálculo para alógica intuicionista dual, que é um tipo delógica paraconsistente, exigindo que os sequentes possuam apenas uma fórmula no antecedente.

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

Historicamente, sequentes foram introduzidos porGerhard Gentzen, com o objetivo de especificar o famosocálculo de sequentes. A palavra usada originalmente foi a palavra alemãSequenz. Nalíngua inglesa, porém, a palavraSequence já é tida como uma tradução para a palavra alemãFolge, e é utilizada frequentemente na matemática. O termoSequent, 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".

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

Este artigo sobrelógica é umesboço. Você pode ajudar a Wikipédiaexpandindo-o. v d e

• Lógica matemática
• Teoria da computação

• !Esboços sobre filosofia
• !Esboços maiores que 5000 bytes