UNIVERSIDADE FEDERAL DE PERNAMBUCO

CENTRO DE INFORMÁTICA
GRADUAÇÃO EM CIÊNCIA DA COMPUTAÇÃO

Jefferson Elder da Mota Nascimento

Introdução ao Cálculo de Sequentes de Gentzen

RECIFE
2023
 UNIVERSIDADE FEDERAL DE PERNAMBUCO
CENTRO DE INFORMÁTICA
CURSO DE BACHARELADO EM CIÊNCIA DA COMPUTAÇÃO

Jefferson Elder da Mota Nascimento

Introdução ao Cálculo de Sequentes de Gentzen

RECIFE
2023
 Ficha de identificação da obra elaborada pelo autor,
através do programa de geração automática do SIB/UFPE

Nascimento, Jefferson Elder da Mota.

Introdução ao cálculo de sequentes de Gentzen / Jefferson Elder da Mota
Nascimento. - Recife, 2023.
32

Orientador(a): Anjolina Grisi de Oliveira

Trabalho de Conclusão de Curso (Graduação) - Universidade Federal de
Pernambuco, Centro de Informática, Ciências da Computação - Bacharelado,
2023.

1. Cálculo de sequentes. I. de Oliveira, Anjolina Grisi. (Orientação). II.

Título.

160 CDD (22.ed.)

 AGRADECIMENTOS

Com profunda gratidão, expresso minha reverência a Deus, o supremo criador e

arquiteto do universo, por me permitir explorar as complexidades da expressão da razão
humana, a qual é reflexo da ordem e harmonia presentes em Sua divina criação. À medida que
desvendo os segredos dessa intrincada manifestação tangível da mente humana, encontro uma
prova vívida da grandiosidade da mente divina que permeia todas as coisas. Esse
reconhecimento é uma homenagem à majestade daquele sem o qual nada pode ser realizado e
também é um testemunho da busca humana pela verdade, guiada pela sabedoria divina
infinita.
Gostaria de agradecer à professora Anjolina Grisi, pois sem sua disponibilidade e
orientação, este projeto não teria sido viável. Sua generosidade, atenção e gentileza me
ajudaram a perceber que a jornada de aprendizado pode ser menos árdua.
Agradeço também a painho, que sempre se manteve como um apoio sólido e
inabalável durante minha juventude. Foi graças ao seu incansável sacrifício, esforço e
dedicação que consegui chegar até onde estou. Sua presença constante e seu exemplo
desempenharam um papel fundamental na formação da pessoa que sou hoje.
Agradeço à mainha por ter me carregado em seus braços, desde o seu ventre até os
mais altos patamares do saber, por ter pessoalmente se encarregado de cada uma das minhas
conquistas acadêmicas e por ter me oferecido um imenso amor e apoio permanente que foram
cruciais para o meu desenvolvimento como pessoa humana, estudante e profissional.
E finalmente agradeço aquela que fez tudo isso finalmente valer a pena, minha
namorada Andrea. Por seu companheirismo, amizade e amor que me levantaram, sustentaram
e guiaram desde os nossos primeiros dias. Por ter sido um presente repentino e muito bem
vindo e por ter sido uma inesperada firme alavanca em minha vida acadêmica até esse final de
jornada.
 RESUMO

O cálculo de sequentes, desenvolvido por Gentzen no início do século, é uma

ferramenta essencial na lógica matemática, usada para demonstrar a validade de argumentos
ao resolver o desafio de verificar se uma fórmula segue logicamente de um conjunto de
premissas. Isso é facilitado pelo uso de regras formais. Uma de suas maiores conquistas é o
Teorema da Eliminação do Corte. Ao evitar a introdução arbitrária de cortes nas deduções,
asseguramos que todas as provas válidas possam ser construídas sistematicamente, e nenhum
argumento válido escape à nossa análise. Este trabalho se concentra em examinar o cálculo de
sequentes de Gentzen, incluindo seus princípios fundamentais, regras de inferência e na
introdução breve do Teorema da Eliminação do Corte, juntamente com suas implicações
práticas e teóricas.

Palavras-chave: Cálculo de sequentes, Teorema da Eliminação do Corte, Lógica matemática

 ABSTRACT

The sequent calculus, developed by Gentzen in the early 20th century, is an essential
tool in mathematical logic used to demonstrate the validity of arguments when addressing the
challenge of verifying whether a formula logically follows from a set of premises. This is
facilitated by the use of formal rules. One of its major achievements is the Cut Elimination
Theorem. By avoiding the arbitrary introduction of cuts in deductions, we ensure that all valid
proofs can be systematically constructed, and no valid argument escapes our analysis. This
work focuses on examining Gentzen's sequent calculus, including its fundamental principles,
inference rules, and a brief introduction to the Cut Elimination Theorem, along with its
practical and theoretical implications.

Keywords: Sequent calculus, Cut Elimination Theorem, Mathematical logic

Sumário
1. Introdução........................................................................................................................................... 8
2. Lógica Proposicional............................................................................................................................ 9
3. Introdução aos sequentes de Gentzen.............................................................................................. 12
3.1. Significado do sequente..................................................................................................................12
4 O cálculo de sequentes....................................................................................................................... 14
5 A regra do corte.................................................................................................................................. 20
5.1 Síntese de prova........................................................................................................................ 21
6 Teorema da eliminação do corte (“Hauptsatz” de Gentzen).............................................................. 24
6.1 Casos-chave...............................................................................................................................24
6.2 Lemas fundamentais................................................................................................................. 27
7 Conclusão...........................................................................................................................31
8 Bibliografia.......................................................................................................................................... 32
1. Introdução

Na década de 1930, Gerhard Gentzen introduziu o cálculo de sequentes, uma

contribuição crucial para o desenvolvimento da lógica matemática no século XX. Essa
abordagem desempenhou um papel fundamental ao buscar uma maneira mais abrangente e
elegante de lidar com a lógica formal. David Hilbert, um matemático proeminente da época,
também fez contribuições significativas para este campo.
Antes disso, no início do século XX, figuras como Gottlob Frege, Bertrand Russell,
Alfred North Whitehead e David Hilbert já haviam feito contribuições importantes para a
lógica formal. No entanto, havia uma necessidade urgente de um sistema lógico que pudesse
unificar a lógica clássica de maneira mais rigorosa.
Gentzen desenvolveu o cálculo de sequentes com o propósito de unir os aspectos
matemáticos e filosóficos da lógica, preenchendo uma lacuna importante naquele período.
Essa abordagem representou uma mudança radical em relação à lógica convencional, pois, em
vez de depender dos axiomas lógicos tradicionais e das regras de inferência, Gentzen
introduziu o conceito de "sequente". Essa ideia era uma maneira estruturada de afirmar que, a
partir de uma série de premissas, era possível derivar logicamente uma série de conclusões.
Com o cálculo de sequentes, tornou-se possível o desenvolvimento de um sistema dedutivo
que permitia a formalização de um raciocínio preciso e sistemático.
A importância histórica do cálculo de sequentes se manifestou de várias formas.
Primeiro, sua expressividade possibilitou acomodar diversos sistemas lógicos, tornando-se
uma ferramenta valiosa para explorar as diferentes abordagens lógicas da época. Além disso,
a estrutura dos sequentes introduziu um nível de clareza no raciocínio, tornando mais fácil a
análise rigorosa das provas. Assim, desempenhou um papel crucial na teoria da prova,
enriquecendo nossa compreensão do raciocínio matemático e das relações entre diferentes
sistemas lógicos. Também teve aplicações em áreas como linguística, filosofia e teoria dos
jogos, contribuindo para a diversificação das pesquisas.
O cálculo de sequentes possui vantagens notáveis em comparação com outros sistemas
dedutivos, sendo particularmente eficaz na abordagem de questões intrincadas em matemática
e lógica. Além disso, permite a demonstração de um teorema fundamental na teoria da prova:
o teorema da eliminação do corte.
Este trabalho tem como objetivo apresentar os principais conceitos e características do
cálculo de sequentes, incluindo a construção de provas com sequentes e o uso das regras de
inferência. Com isso, buscamos aprofundar nosso conhecimento em lógica, analisando a
estrutura lógica de proposições complexas, identificando argumentos válidos e construindo
demonstrações coerentes. Durante este documento, exploraremos os fundamentos teóricos
desse sistema, apresentando regras básicas e princípios de dedução lógica, além de discutir
suas vantagens, limitações e contribuições para a lógica, um tópico que geralmente não é
abordado durante a graduação.
2. Lógica Proposicional

A lógica clássica, também conhecida como lógica aristotélica, é uma forma de lógica
que se baseia nos princípios estabelecidos pelo filósofo grego Aristóteles. Ela forma a base do
pensamento lógico e se desdobra em dois ramos principais: a lógica proposicional e a lógica
de lógica de predicados.
Ao abordar o poder expressivo na lógica, é crucial distinguir entre essas duas
categorias fundamentais. A lógica de predicados, com sua capacidade de representar não
apenas proposições, mas também objetos e suas complexas relações, possui um espectro mais
amplo de capacidades expressivas. Entretanto, é importante notar que, do ponto de vista
computacional, a lógica de predicados é classificada como semi-decidível. Isso implica que,
enquanto algumas sentenças em lógica de predicados podem ser decididas de forma
algorítmica, outras não podem, tornando-a um campo de estudo desafiador em termos de
computação.
No entanto, no contexto deste estudo, focaremos principalmente na lógica
proposicional, deixando de lado as complexidades da lógica de predicados. Isso nos permitirá
explorar os fundamentos da lógica clássica e suas aplicações de forma mais abrangente.
Neste estudo, estamos desenvolvendo um sistema abrangente para analisar e derivar
conclusões lógicas de proposições complexas. Começaremos explorando os componentes e
princípios fundamentais deste trabalho e seu papel no aprimoramento do raciocínio lógico
avançado:

1. Sintaxe: Refere-se à estrutura gramatical e às regras formais que governam a

construção de fórmulas ou sentenças na lógica proposicional. Ela lida com a forma
como os símbolos e operadores são usados para criar expressões lógicas válidas. Aqui
estão algumas de suas ideias principais:

a. Proposições: Na lógica proposicional, uma afirmação (ou proposição) é

representada por um símbolo (ou letra) cuja relação com outras declarações é
definida por meio de um conjunto de símbolos (ou conectivos). A declaração é
descrita pelo seu valor-verdade, que pode ser verdadeiro ou falso. Elas podem
ser de dois tipos: atômicas e compostas.

b. Proposições atômicas: são afirmações simples que não podem ser divididas em
partes menores. São como peças básicas de um quebra-cabeça. Por exemplo:
Exemplo: "O sol está brilhando." "Está chovendo." Essas são proposições
atômicas porque são declarações diretas sem partes extras.

c. Proposições compostas: são criadas combinando proposições atômicas usando

palavras como "e", "ou" e "não". É como criar quebra-cabeças mais complexos
juntando peças. Exemplo: "O sol está brilhando e é um dia lindo." "Não está
chovendo ou nevando." Essas são proposições compostas porque envolvem a
 combinação de afirmações mais simples com palavras como "e" ou "não" para
criar afirmações mais complexas.

d. Conectivos lógicos: também conhecidos como operadores lógicos ou símbolos

lógicos, desempenham um papel fundamental na lógica proposicional,
ajudando a combinar e manipular afirmações (proposições) para criar
afirmações mais complexas. Existem vários conectivos lógicos principais na
lógica proposicional, cada um servindo a um propósito específico. Aqui estão
os principais:

i. Negação (¬ ou ~): Representa o NOT lógico. Inverte o valor-verdade

de uma proposição. Em termos simples, se uma afirmação P é
verdadeira, então ¬P é falsa, e vice-versa.

ii. Conjunção (∧ ou &): Representa o AND lógico. Conecta duas

proposições e gera um resultado verdadeiro apenas quando ambas as
proposições são verdadeiras. Em linguagem cotidiana, se tanto P
quanto Q são verdadeiras, então P ∧ Q é verdadeira; caso contrário, é
falsa.

iii. Disjunção (∨ ou |): Representa o OR lógico. Conecta duas proposições

e é verdadeira se pelo menos uma das proposições for verdadeira. Para
simplificar, se P ou Q (ou ambos) forem verdadeiros, então P ∨ Q é
verdadeira.

iv. Implicação (→): Representa a implicação lógica ou condicional. É

verdadeira, exceto quando a proposição inicial (aquela à esquerda) é
verdadeira e a consequência (aquela à direita) é falsa. Em termos
simples, P → Q é falso apenas quando P é verdadeira e Q é falsa.

v. Bicondicional (↔): Representa a equivalência lógica. É verdadeira se e

somente se ambas as proposições compartilharem o mesmo valor de
verdade. Para esclarecer, P ↔ Q é verdadeira quando tanto P quanto Q
são verdadeiras ou ambas são falsas.

2. Tabela-verdade: Oferecem uma maneira sistemática de exibir todos os possíveis

valores lógicos (verdadeiro ou falso) para uma dada expressão lógica. Elas nos ajudam
a avaliar a verdade ou falsidade de proposições compostas considerando todas as
combinações possíveis de valores lógicos das proposições componentes. Tipicamente,
uma tabela-verdade consiste em colunas que representam as proposições
componentes, os operadores lógicos usados para combiná-las e uma coluna para o
resultado final da expressão. O resultado final representa o valor lógico global da
expressão para cada combinação de valores lógicos das proposições componentes.
 Isso geralmente é feito aplicando os operadores lógicos passo a passo até que o
resultado final seja determinado.

Por exemplo, considere a expressão lógica P ∧ Q:

P Q P∧Q

V V V

V F F

F V F

F F F

Nesta tabela-verdade, "P" e "Q" representam as proposições componentes, e "P ∧ Q"

representa o resultado da operação lógica E entre P e Q. A tabela cobre todas as
combinações possíveis de valores lógicos para P e Q e mostra o valor lógico resultante
da expressão para cada combinação.

3. Semântica: Trata da interpretação de significados em expressões lógicas. A

tabela-verdade é uma ferramenta crucial nesse processo, ajudando a determinar
quando uma afirmação é verdadeira ou falsa através da análise das combinações
possíveis de valores verdadeiros e falsos das variáveis envolvidas.

A lógica proposicional oferece um sistema preciso para raciocinar sobre afirmações e como
elas se relacionam entre si. Ao utilizar seus métodos, podemos examinar e trabalhar com as
afirmações para tirar conclusões e tomar decisões bem fundamentadas com base em seus
valores-verdade.
3. Introdução aos sequentes de Gentzen

Um sequente é uma expressão que relaciona logicamente duas sequências de fórmulas.

É dividido em duas partes essenciais: o antecedente (também conhecido como premissas) e o
consequente (que corresponde à conclusão). A validade lógica de um sequente está
relacionada à capacidade de inferir com segurança o consequente, ou seja, determinar se é
possível deduzir a sequência de fórmulas que se encontra no lado direito da catraca (⊢), a
partir das fórmulas presentes no seu lado esquerdo.
A representação simbólica de um sequente pode ser expressa da seguinte forma:

Γ⊢Δ

onde:
Γ chamado antecedente, é uma sequência de fórmulas (que pode estar vazio).
⊢ chamado catraca, é o símbolo que indica que o as fórmulas do antecedente implicam
ou demonstram as fórmulas do consequente.
Δ chamado consequente, é uma sequência o de fórmulas (que pode estar vazio). Essas
fórmulas devem ser derivadas a partir da sequência em Γ.

Exemplo: Vamos considerar um exemplo simples usando lógica proposicional: Se tivermos o

antecedente Γ = {P ∧ Q} e quisermos derivar o consequente Δ = {P}, o sequente
correspondente seria:
P∧Q⊢P
Esse sequente afirma que se assumirmos P ∧ Q como premissa, podemos derivar P como
conclusão. Em um sistema formal de prova, como a dedução natural, usaríamos regras de
eliminação da conjunção para justificar essa implicação e mostrar que o sequente é provável.

3.1. Significado do sequente

O valor-verdade de um sequente está intrinsecamente ligado à sua correspondente

interpretação na forma "Γ implica Δ".
Para determinar a verdade de um sequente Γ ⊢ Δ, segue-se um processo sistemático:

1. Combine todos os elementos no antecedente (Γ) usando a conjunção (∧).

2. Substitua o símbolo de sequente (⊢) por um símbolo de implicação (→).

3. Combine todos os elementos no consequente (Δ) usando a disjunção (∨).

A interpretação resultante é expressa como "Γ implica Δ", onde Γ representa a

conjunção de todos os elementos no antecedente e Δ representa a disjunção de todos os
elementos no consequente.
 Essa transformação estabelece uma conexão direta entre os valores-verdade dos
sequentes e suas interpretações correspondentes. Em termos simples, um sequente Γ ⊢ Δ é
considerado verdadeiro se e somente se a interpretação correspondente "Γ implica Δ" for
verdadeira. Essa observação permite uma expansão eficaz da semântica da linguagem
proposicional para o cálculo de sequentes.
Podemos concluir então que, sendo "n" o número de fórmulas no lado esquerdo e "m"
o número de fórmulas do lado direito, temos o seguinte:

1. Se n ≠ 0 e m ≠ 0, então um sequente na forma 𝐴1, . . . , 𝐴𝑛 ⊢ 𝐵1, . . . , 𝐵𝑚 tem o

significado de (𝐴1 ∧ · · · ∧ 𝐴𝑛) → (𝐵1 ∨ · · · ∨ 𝐵𝑚).
2. Se n = 0 e m ≠ 0, então um sequente na forma ⊢ 𝐵1, . . . , 𝐵𝑚 tem o significado
de 𝐵1 ∨ · · · ∨ 𝐵𝑚.
3. Se n ≠ 0 e m = 0, então um sequente na forma 𝐴1, . . . , 𝐴𝑛 ⊢ tem o significado
de ¬(𝐴1 ∧ · · · ∧ 𝐴𝑛).
4. Se n = 0 e m = 0, então um sequente na forma ⊢ (ou seja, o sequente vazio)
significa a contradição ⊥.

Consideremos, por exemplo, o seguinte sequente: Γ = {p, p → q, p → q} e Δ = {r, ¬p}.

Para obter a interpretação correspondente ao sequente Γ ⊢ Δ, seguimos um processo
sistemático:

1. Combinamos os elementos no antecedente (Γ) usando a conjunção (∧): p ∧ (p → q)

∧ (p → q).

2. Substituímos o símbolo de consequência (⊢) por um símbolo de implicação (→): p ∧

(p → q) ∧ (p → q) →.

3. Combinamos os elementos no consequente (Δ) usando a disjunção (∨): p ∧ (p → q)

∧ (p → q) → (r ∨ ¬p).

Dessa forma, a interpretação correspondente ao sequente dado é: "p ∧ (p → q) ∧ (p

→ q) → (r ∨ ¬p)." Consequentemente, a determinação da verdade do sequente depende da
verdade dessa interpretação. Se essa interpretação for verdadeira, o sequente é considerado
verdadeiro; caso contrário, se a interpretação for falsa, o sequente é considerado falso.
4 O cálculo de sequentes

No cálculo de sequentes de Gentzen, existem duas versões essenciais: LK (Logistische

Kalkül ou 'Cálculo Lógico' em alemão) e LJ (Logistische Intuitionistisch ou 'Lógica
Intuicionista' em alemão). Essas variantes diferem significativamente em sua lógica
subjacente e aplicação.
O LK é especificamente desenvolvido para a lógica clássica, onde a lei do terceiro
excluído é válida, o que implica que as proposições são estritamente verdadeiras ou falsas.
Por outro lado, o LJ foi concebido para a lógica intuicionista, na qual as proposições não são
categorizadas tão rigidamente como verdadeiras ou falsas. Gentzen introduziu uma restrição
no LJ, limitando a cardinalidade da sequência de fórmulas do lado direito da catraca a apenas
uma fórmula. Isso significa que o LJ não permite a derivação de teoremas rejeitados pela
lógica intuicionista, como o princípio do terceiro excluído (A ou não A). Em contraste, essa
restrição não se aplica ao LK, que é adequado para lidar com a lógica clássica sem tais
limitações.
O cálculo de sequentes é uma ferramenta fundamental que representa o processo
dedutivo como uma sequência de sequentes, onde cada sequente corresponde a um passo na
prova.
Na nossa abordagem, a construção de uma prova assume a forma de uma árvore de
derivação. Essa árvore de derivação é uma representação gráfica estruturada que simplifica a
derivação de sequentes. Ela possui elementos distintos, como uma raiz que representa o
sequente que estamos tentando provar, folhas que simbolizam os axiomas iniciais, linhas de
inferência horizontais que claramente separam premissas de conclusões e regras de inferência
posicionadas estrategicamente ao lado das linhas. Essas regras orientam a geração sistemática
de novas fórmulas a partir das existentes.
Essa abordagem organizada aprimora consideravelmente nossa capacidade de
compreender e analisar provas lógicas complexas. As árvores de derivação tornam-se, assim,
uma ferramenta poderosa para o desenvolvimento do raciocínio lógico e das técnicas de
prova. No contexto do cálculo de sequentes, as regras determinam como um sequente pode
ser metodicamente e sistematicamente transformado em outro, permitindo a construção de
provas sólidas e válidas.. Seus principais componentes incluem:

1. Axiomas: Um axioma é uma afirmação considerada verdadeira sem necessidade de

prova. Geralmente, trata-se de um princípio lógico ou matemático fundamental ou
auto evidente.

Neste exemplo, fica evidente que qualquer fórmula A pode ser derivada de si mesma,
sem a necessidade de premissas. É conhecido como a "regra do axioma," que é uma
regra de inferência que opera sem a presença de premissas. Ela também é referida
como a "sequente inicial," já que pode ser utilizada para dar início a uma derivação no
 cálculo de sequentes. Na nossa representação de árvore de derivação, essa regra
corresponde aos rótulos das folhas.

2. Regra do Corte: A Regra do Corte é uma regra de inferência fundamental que merece
destaque neste momento, devido à sua extrema importância e notável generalidade.
Ela se diferencia das outras regras, que em sua maioria estão voltadas para operações
lógicas específicas. Dada a centralidade da Regra do Corte, nossa intenção é abordá-la
de forma mais detalhada e abrangente nas seções subsequentes. Isso nos permitirá
explorar minuciosamente as diversas implicações que essa regra oferece.

3. Regras estruturais: As regras estruturais são um conjunto de regras que governam a

manipulação de sequentes sem afetar diretamente o conteúdo lógico das fórmulas
nesses sequentes. Essas regras concentram-se principalmente nos aspectos estruturais
das provas, permitindo a reorganização de fórmulas, a introdução de hipóteses
adicionais e a eliminação de informações redundantes. O propósito fundamental das
regras estruturais é garantir que o processo de inferência de conclusões a partir de
premissas no cálculo de sequentes permaneça válido e coerente. Destacam-se três
regras estruturais principais:

a. Weakening (ou Regra do enfraquecimento): A regra de enfraquecimento nos

permite adicionar pressupostos adicionais tanto à direita (W right) quanto à
esquerda (W left) do sequente sem afetar a sua validade. Isso significa que
podemos introduzir novas informações ou hipóteses antes ou depois das
premissas existentes em um sequente, mantendo sua validade intacta.

b. Contração: A regra da contração permite eliminar duplicatas de hipóteses tanto

no lado direito (C right) quanto no lado esquerdo (C left) de um sequente sem
afetar sua validade.

c. Exchange (ou Regra da Permutação): A regra da permutação no cálculo de

sequentes permite alterar a ordem das fórmulas na lista de premissas ou
conclusões sem afetar a validade de um argumento lógico. É uma ferramenta
básica para reorganizar informações em uma prova.
4. Regras lógicas: chamadas de regras "operacionais" por Gentzen, giram em torno da
manipulação de operadores lógicos. Essas regras também são emparelhadas: para cada
operador, existe uma ou duas regras à esquerda na qual o sequente de conclusão
contém uma fórmula com esse operador no antecedente e uma ou duas regras
correspondente à direita associada a ele. Esse emparelhamento inclui:

a. Conjunção: A conjunção lógica ou "e" de duas fórmulas significa que ambas as

fórmulas são verdadeiras. As regras para conjunção no cálculo de sequentes
nos permitem introduzir ou eliminar uma conjunção no antecedente ou no
consequente de um sequente.

b. Disjunção: A disjunção lógica ou "ou" de duas fórmulas significa que uma ou

ambas as fórmulas são verdadeiras. As regras para disjunção no cálculo de
sequentes nos permitem introduzir ou eliminar uma disjunção no antecedente
ou no consequente de um sequente.

c. Condicional: A condicional lógica ou "implicação" de duas fórmulas significa

que se a primeira fórmula for verdadeira, então a segunda fórmula também é
verdadeira. As regras para condicional no cálculo de sequentes nos permitem
introduzir ou eliminar uma condicional no antecedente ou no consequente de
um sequente.

d. Negação: A negação lógica, representada pelo "não," inverte o valor-verdade

de uma fórmula. Se a fórmula original for verdadeira, sua negação será falsa, e
se a fórmula original for falsa, sua negação será verdadeira. Nas regras de
negação no cálculo de sequentes, temos a capacidade de introduzir ou eliminar
uma negação no antecedente ou no consequente de um sequente.
Para ilustrar a aplicação dos conhecimentos recém-adquiridos, finalmente provaremos o
sequente apresentado na seção anterior P ∧ Q ⊢ P utilizando as ferramentas do cálculo de
sequentes:

1. P ∧ Q ⊢ P é o sequente final, o sequente que queremos provar. Para construir nossa

árvore, primeiro escrevemos esse sequente na parte inferior e começamos a derivá-lo
para cima, adicionando a linha de inferência entre cada derivação.

2. O primeiro passo seria usar a regra lógica da conjunção à esquerda, que foi a primeira
apresentada neste estudo. Essa regra traz 'P' do antecedente para o próximo sequente e
repete o consequente, que também é 'P'.

3. O novo sequente é "P ⊢ P," que é uma tautologia e nosso axioma. Sem a necessidade
de mais provas, chegamos à nossa folha e provamos o sequente "P ∧ Q ⊢ P."

Assim derivamos com sucesso o sequente P ∧ Q ⊢ P utilizando o cálculo de sequentes de

Gentzen.
Agora que dominamos os conceitos fundamentais, estamos prontos para abordar
demonstrações mais complexas e avaliar sua validade.
Para ilustrar isso, vamos analisar o seguinte sequente:

A ⊢ (A → B) ∧ (B → A)

Neste sequente, a afirmação é que se A for verdadeiro, então tanto A → B quanto B → A

devem ser verdadeiros. Em outras palavras, se A for verdadeiro, isso implica que B e A são
equivalentes. Vamos construir a demonstração e verificar se conseguimos provar a validade
desse sequente.
1. Começamos aplicando a regra da conjunção a direita, que nos permite separar o
consequente resultando em dois novos sequentes.
2. Focamos no ramo da direita, e aplicamos a regra da implicação a direita trazendo o B
para o lado esquerdo da catraca e mantendo o A no lado direito.

3. Ainda no ramo direito da árvore, utilizamos a regra do enfraquecimento a direita

retirando B sem modificar a validade do antecedente. Assim obtemos a tautologia A ⊢
A que não necessidade de prova, chegando assim a um axioma e folha da nossa árvore

4. Nos direcionamos agora ao ramo esquerdo de nossa prova aplicando a regra da

implicação a direita levando o A do consequente para o antecedente.

5. Continuamos com uso da regra da contração a esquerda omitindo a fórmula A repetida

no antecedente

6. Aqui nos deparamos com um impasse, pois não é possível estabelecer um axioma.
Isso fica evidente quando construímos a tabela verdade e percebemos que não é
sempre o caso que, quando A é verdadeiro, (A → B) ∧ (B → A) também seja
verdadeiro.
 A B A→B B→A (A→B) ∧ (B→A)

V V V V V

F V V F F

V F F V F

F F V V V

Assim, observando a construção de uma prova no cálculo de sequentes, percebemos

sua utilidade tanto na determinação da validade de um sequente quanto na identificação de
sua invalidade. Durante o processo de construção da prova, se encontrarmos uma contradição
ou inconsistência em algum ponto, isso nos indicará que o sequente é inválido. Isso ocorre
porque não é possível derivá-lo de suas premissas utilizando regras lógicas válidas. Portanto,
a construção de provas no cálculo de sequentes não apenas verifica a validade, mas também
nos alerta sobre a inviabilidade de um sequente.
5 A regra do corte

Uma regra de grande importância que deliberadamente deixamos de mencionar devido

à sua complexidade e à necessidade de uma explicação mais detalhada é a regra do corte.
Diferentemente das regras mais simples discutidas anteriormente, a regra do corte amplia
consideravelmente sua aplicabilidade na lógica proposicional ao generalizar o modus ponens.
Para compreender esse conceito, podemos considerar dois conjuntos de afirmações,
representados como Γ ⊢ Δ, A e Π, A ⊢ Σ. Aqui, 'A' é uma afirmação que aparece em ambas as
sequências Δ e Π. A regra do corte nos permite remover 'A' desses conjuntos enquanto íntegra
sem esforço as afirmações restantes em um único conjunto: Γ, Π ⊢ Δ, Σ.
A representação formal da regra do corte é a seguinte:

A versatilidade da regra do corte é evidente em sua aplicação extensiva em várias

provas, tanto na lógica quanto na matemática. Entre seus benefícios, a regra do corte nos
permite decompor teoremas complexos em partes mais gerenciáveis, facilitando o processo de
prova. No entanto, é importante observar que a regra do corte também possui um aspecto
negativo: ela pode levar a provas mais intrincadas, adicionando complexidade ao processo
analítico geral.
Para ilustrar esse conceito importante, consideremos um exemplo simples que
demonstra o uso da regra do corte. Imagine que temos os seguintes sequentes:

Sequente 1: A ⊢ B
Sequente 2: B, C ⊢ D

No Sequente 1, temos a afirmação 'A' levando a 'B'. No Sequente 2, as afirmações 'B' e 'C',
juntas, levam a 'D'. Note que ambos os sequentes envolvem 'B'. Agora, nosso objetivo é
combinar esses sequentes usando a regra do corte.
Ao utilizar a regra do corte, podemos eliminar 'B' de ambos os sequentes e consolidar as
afirmações restantes. Aplicando a regra do corte, obtemos:

No sequente resultante, 'A' e 'C', juntas, levam a 'D', que é a conclusão desejada. Isso
demonstra como a regra do corte nos permite decompor e combinar sequentes com fórmulas
compartilhadas para deduzir novas conclusões.
A regra do corte, como demonstrado neste exemplo, é uma ferramenta poderosa para
gerenciar as relações lógicas entre afirmações, permitindo simplificar provas complexas e
estabelecer conexões entre diferentes partes do nosso raciocínio.
5.1 Síntese de prova

No contexto do cálculo de sequentes, a síntese de prova envolve a fusão de provas

desenvolvidas de forma independente para produzir novas conclusões.
Quando duas pessoas trabalham separadamente para estabelecer a validade de
sequentes que envolvem a mesma fórmula lógica, surge a possibilidade de combinar suas
provas, resultando em uma dedução aprimorada. Esse processo é comumente conhecido como
"combinação de provas" ou "síntese de prova".
Para desdobrar esse conceito em termos práticos:

1. Provas Iniciais: Cada indivíduo embarca na construção de suas próprias provas com o
objetivo de demonstrar a validade de um sequente dado que contém uma fórmula
lógica compartilhada.

2. Fórmula Compartilhada: Vamos denotar a fórmula lógica compartilhada como 'A'.

3. Fusão de Provas: Se ambas as provas confirmarem efetivamente a legitimidade de

sequentes com a fórmula A, surge a oportunidade de mesclar as duas provas para
derivar uma nova conclusão. Isso normalmente envolve analisar os elementos
estruturais das provas individuais e identificar pontos de convergência ou raciocínio
análogo.

4. Nova Conclusão: Através da fusão das provas, torna-se viável deduzir uma nova
conclusão que vai além das realizações de cada prova individualmente. Essa nova
dedução se baseia no conhecimento coletivo e nas etapas lógicas presentes em ambas
as provas.

É crucial enfatizar que o processo de fusão de provas pode ser intricado e

frequentemente requer análise minuciosa para garantir que a conclusão resultante permaneça
logicamente coerente. Além disso, a viabilidade de mesclar provas depende das regras
específicas e axiomas que regem o sistema de cálculo de sequentes em uso.
A facilidade de fusão de provas pode variar; em alguns casos, é direta, enquanto em
outros, pode ser mais complexa ou até mesmo inatingível devido às características estruturais
específicas das provas e às interdependências que envolvem. No entanto, o conceito de
aproveitar múltiplas provas para derivar novos insights é um princípio fundamental nos
campos da lógica e da teoria da prova.
Para detalhar como a regra do corte funciona e seu papel na síntese de prova
suponhamos o seguinte exemplo:

Considere duas provas - Prova 1 e Prova 2 - que estabelecem a validade de dois sequentes:

Prova 1: Γ ⊢ A Isso representa a primeira prova, onde Γ é um conjunto de premissas e A é a

conclusão.
Prova 2: A, Δ ⊢ B Isso representa a segunda prova, onde A é uma fórmula compartilhada e Δ
é outro conjunto de premissas, levando à conclusão B.

Aplicação da Regra do Corte: A regra do corte nos permite eliminar a fórmula compartilhada
A. Aplicando a regra do corte, combinamos as duas provas em um todo coerente.

Novo Sequente: Γ, Δ ⊢ B Como resultado da aplicação da regra do corte, obtemos um novo

sequente em que as premissas de ambas as provas (Γ e Δ) levam à conclusão B.
Assim temos:

Um exemplo prático já visitado na seção anterior e que ilustra bem esse conceito é a aplicação
do corte na prova:

Onde A ⊢ B é a prova 1, B,C ⊢ D é a prova 2 e A,C ⊢ D é o novo sequente resultante.

A regra do corte permite a remoção ou "corte" da fórmula compartilhada A dos dois

sequentes, efetivamente fundindo as duas provas em um todo coerente, o que resulta em um
novo sequente. Isso implica que as premissas combinadas de ambas as provas agora levam
diretamente à conclusão B, eliminando a necessidade de uma prova separada de A como etapa
intermediária.
A fundamentação da regra do corte está baseada no raciocínio lógico e é normalmente
estabelecida como uma das regras de inferência dentro do cálculo de sequentes.
Essencialmente, a regra encapsula o conceito de que, se você pode estabelecer A a partir de Γ
e, em seguida, estabelecer B a partir de A e Δ, você pode deduzir diretamente B a partir de Γ e
Δ.
A regra do corte na lógica matemática é uma ferramenta poderosa que, quando
utilizada corretamente, simplifica consideravelmente as provas, permitindo a eliminação de
etapas intermediárias e estabelecendo conexões diretas entre diferentes partes da prova. Isso é
fundamental para analisar o raciocínio lógico, tornando mais acessível o manuseio de provas
intricadas, de forma semelhante à divisão de um problema complexo em subproblemas
menores e mais gerenciáveis. Essa flexibilidade na construção de provas é uma das vantagens
mais importantes da regra do corte, pois permite a inserção de fórmulas em diferentes pontos
das árvores de prova, sem restrições a fórmulas predefinidas ou iniciais. À medida que a
prova avança, novas fórmulas podem ser introduzidas conforme necessário, facilitando o
desenvolvimento do argumento e abordando uma variedade de problemas e argumentos na
lógica matemática.
 No entanto, o uso da regra de corte também apresenta desafios, sendo uma
preocupação importante seu potencial de ferir a propriedade de subformulas. A propriedade
de subformulas, definida formalmente como a exigência de que todas as fórmulas em uma
prova devem ser subformulas do sequente final, é crucial. Essa exigência garante a
manutenção da consistência lógica e a precisão da prova em relação à validade do sequente.
Portanto, seu uso deve ser cauteloso e cuidadoso para evitar conclusões errôneas ou
insustentáveis.
Além disso, essa propriedade possui importância significativa, particularmente no
contexto dos provadores automáticos de teoremas no cálculo de sequentes de Gentzen. Um
provador automático de teoremas é um programa de computador ou sistema projetado para
automatizar o processo de demonstração de teoremas matemáticos. Ele desempenha um papel
fundamental na restrição do espaço de busca para subformulas, permitindo que o provador de
teoremas se concentre exclusivamente nas partes relevantes da prova. Essa restrição reduz a
complexidade computacional e melhora significativamente o desempenho dos sistemas de
provação automática de teoremas, tornando-os ferramentas inestimáveis para matemáticos e
pesquisadores.
6 Teorema da eliminação do corte (“Hauptsatz” de Gentzen)

Ao usar a regra do corte, novas fórmulas podem ser introduzidas na prova que não são
subformulas do sequente final. Isso pode simplificar a prova, mas também torná-la mais
complexa e menos compreensível, afetando a consistência da prova e a validação.
O Teorema da Eliminação do Corte, formulado por Gerhard Gentzen em 1934, lida
com essas questões, demonstrando a possibilidade de obter uma prova "livre de corte",
alcançando a mesma conclusão que uma prova que a utiliza, simplificando o processo de
construção da prova e mantendo a coerência estrutural dos argumentos lógicos. Em uma
definição formal:

Seja S um cálculo de se quentes para um dado sistema lógico. O Teorema de

Eliminação do Corte declara que para qualquer sequente Γ ⊢ Δ derivável em S (ou seja, uma
prova válida usando as regras do cálculo de sequentes S), existe uma prova em S sem o uso
da regra do Corte que estabelece o mesmo sequente Γ ⊢ Δ.

Em outras palavras, uma prova válida no cálculo de sequentes de Gentzen S que

envolve a regra do Corte pode ser transformada sistematicamente em uma prova equivalente
em S sem que a regra do Corte seja usada, enquanto ainda se prova o mesmo sequente.
No entanto, demonstrar esse teorema é um desafio que requer atenção minuciosa.
Inicialmente, iremos identificar os casos-chave que nos proporcionam uma compreensão
sólida do panorama geral, para então nos concentrarmos nos detalhes mais intrincados.

6.1 Casos-chave

Os casos-chave são situações em que a regra de corte pode ser descartada porque as
regras lógicas que introduzem a mesma fórmula se alinham, demonstrando simetria profunda.
Esses casos-chave são explicados para os seguintes conjuntos de regras:

1. (∧ right) e (∧ left 1): Neste caso, antes de aplicar a regra do corte, as duas fórmulas
utilizadas originaram-se de uma conjunção à direita no lado esquerdo e uma conjunção
à esquerda no lado direito. Aqui (∧ left 1) representa a rega de conjunção onde a
fórmula mais a esquerda é trazida para cima.
 Torna-se uma derivação da seguinte forma:

Ou utiliza a notação de barra dupla para simbolizar múltiplas instâncias da aplicação

da regra do Enfraquecimento e da Permutação, temos:

2. (∧ right) e (∧ left 2): Neste caso, antes de aplicar a regra do corte, as duas fórmulas
utilizadas originaram-se de uma conjunção à direita no lado esquerdo e uma conjunção
à esquerda no lado direito. Aqui (∧ left 2) representa a rega de conjunção onde a
fórmula mais a direita é trazida para cima.

De maneira similar, pode ser substituído pela seguinte forma (mais uma vez nos
utilizando da barra dupla):

3. (∨ right 1) e (∨ left): Neste caso, antes de aplicar a regra do corte, as duas fórmulas
utilizadas originaram-se de uma disjunção à direita no lado esquerdo e uma disjunção
à esquerda no lado direito. Aqui (∨ right 1) representa a rega de disjunção onde a
fórmula mais a esquerda é trazida para cima.
 É substituído por:

4. (∨ right 2) e (∨ left): Neste caso, antes de aplicar a regra do corte, as duas fórmulas
utilizadas originaram-se de uma disjunção à direita no lado esquerdo e uma disjunção
à esquerda no lado direito. Aqui (∨ right 2) representa a rega de disjunção onde a
fórmula mais a direita é trazida para cima.

Equivale a:

5. ( ¬ right) e ( ¬ left): Neste caso, antes de aplicar a regra do corte, as duas fórmulas
utilizadas originaram-se de uma negação à direita no lado esquerdo e uma negação à
esquerda no lado direito.

Corresponde a forma:

6. ( → right) e ( → left): Neste caso, antes de aplicar a regra do corte, as duas fórmulas
utilizadas originaram-se de uma implicação à direita no lado esquerdo e uma
implicação à esquerda no lado direito.
 Traduz-se como:

Observe-se que, nesse último cenário, o problema foi resolvido através de dois cortes.

É relevante salientar que, apesar de a finalidade destas substituições ser a exclusão da

regra de corte, em todos os exemplos mencionados, o corte não foi de fato abolido da prova;
ao invés disso, ele foi deslocado ligeiramente para uma posição superior. Isso ilustra como,
mediante o uso repetitivo dessas transformações em uma prova, é viável progressivamente
eliminar a mencionada regra, deslocando continuamente as posições de corte para cima até
sua completa extinção. Outro ponto de extrema importância a enfatizar é que estamos fazendo
uso de uma versão da prova que exclui permutações e enfraquecimentos, o que pode criar
uma impressão enganosa de que as provas estão se tornando menores, quando, na verdade,
ocorre precisamente o contrário.
É crucial reconhecer que o teorema de eliminação de corte envolve conceitos
complexos que demandam uma compreensão aprofundada para sua aplicação ótima.

6.2 Lemas fundamentais

Para tanto, um conceito essencial na aplicação da eliminação de cortes é a ideia de

profundidade lógica. Essa ideia serve para quantificar a complexidade das fórmulas lógicas,
levando em consideração os conectores lógicos. Os principais elementos dessa noção
incluem:
1. A profundidade lógica dp(ϕ) de uma fórmula é definida indutivamente da seguinte
forma:
a. A profundidade lógica de uma variável proposicional ou ⊥ (contradição) é 0.

b. Para conectivos lógicos binários (denotados por □), a profundidade lógica de ϕ

ψ é o máximo entre dp(ϕ) e dp(ψ), incrementado em 1.

O símbolo □ usado na definição de profundidade lógica, pode ser substituído por

qualquer conectivo lógico. Isso significa que a definição é válida para uma ampla gama de
operadores lógicos.
 2. A classificação ou grau rk(ϕ) de uma fórmula ϕ é definida como dp(ϕ) + 1. Aqui,
dp(ϕ) representa a profundidade lógica da fórmula ϕ.

Para ilustrar, considere as seguintes fórmulas lógicas:

ϕ = P (onde P é uma variável proposicional)
ψ = Q (onde Q é outra variável proposicional)
φ = (ϕ ∨ ψ)

1. A profundidade lógica dp(ϕ) de uma variável proposicional é 0, então dp(ϕ) = 0.

2. Da mesma forma, a profundidade lógica dp(ψ) de outra variável proposicional também
é 0, então dp(ψ) = 0.
3. Agora, vamos calcular a profundidade lógica da fórmula composta φ = (ϕ ∨ ψ).
4. O operador lógico utilizado aqui é a disjunção (∨), que é um conector lógico binário.
Portanto, dp(φ) = max(dp(ϕ), dp(ψ)) + 1 = max(0, 0) + 1 = 1.

Agora, vamos calcular a classificação rk(ϕ) para cada fórmula:

rk(ϕ) = dp(ϕ) + 1 = 0 + 1 = 1.
rk(ψ) = dp(ψ) + 1 = 0 + 1 = 1.
rk(φ) = dp(φ) + 1 = 1 + 1 = 2.

Tendo já estudado os conceitos de profundidade lógica e classificação, podemos agora

avançar para o segundo passo em nosso estudo sobre eliminação de corte. Este passo envolve
abordar a tarefa específica de encontrar evidências sem utilizar a regra de corte, uma tarefa
facilitada pelos conceitos-chave conhecidos como 'Lema Chave', 'Lema de Enfraquecimento'
e 'Lema de Inversão'

Weakening:
Se Γ ⊢ ∆ é o sequente final de uma derivação π e Γ ⊆ Γ0 e ∆ ⊆ ∆0, então Γ0 ⊢ ∆0
também é derivável. Na verdade, o último tem uma derivação π0 com uma classificação não
maior do que a de π.

Este lema, também conhecido como "Lema de Enfraquecimento", afirma que se você
possui uma derivação π de um sequente Γ ⊢ ∆ e consegue identificar as subfórmulas
Γ0 e ∆0, de modo que Γ seja um subconjunto de Γ0 e ∆ seja um subconjunto de ∆0,
então é possível derivar o sequente Γ0 ⊢ ∆0. Além disso, este lema assegura que a
nova derivação π0 do sequente Γ0 ⊢ ∆0 terá uma classificação (que mensura a
complexidade da derivação) não superior à de π.

Lema de Inversão:
Cada uma das regras no cálculo de sequentes clássico é invertível: se existe uma
derivação π de um sequente σ e σ pode ser obtido a partir dos sequentes σ1, . . . , σn por uma
das regras, então existem derivações πi dos σi também, e a classificação de cada πi não
precisa ser maior do que a de π.
 O “Lema da inversão” define que dentro do cálculo de sequentes, uma regra serve
como guia para gerar um novo sequente a partir de um ou mais sequentes anteriores.
Uma regra é considerada invertível quando nos permite reverter esse procedimento;
em outras palavras, se possuímos conhecimento da verdade do novo sequente,
podemos deduzir que os sequentes anteriores também são verdadeiros.
Por exemplo, uma das regras no cálculo sequente é a regra de introdução da
conjunção (∧), que estipula que, se tivermos dois sequentes, A e B, podemos
estabelecer um novo sequente, A ∧ B, que denota a conjunção de "A e B são ambos
verdadeiros". Essa regra é invertível porque, quando verificamos a verdade de A ∧ B,
podemos inferir a verdade tanto de A quanto de B. A essência do lema da inversão
reside em sua afirmação de que, para regras específicas dentro do cálculo sequente,
esse processo reverso é consistentemente aplicável para construir uma prova. Para
ilustrar, ao tentar validar um sequente no formato de A ∧ B, podemos
sistematicamente esforçar-nos para provar tanto A quanto B individualmente, e depois
empregar a regra de introdução da conjunção (∧) para uni-los. Essa abordagem
simplifica nosso objetivo, permitindo-nos concentrar nos sequentes menores da prova.
O lema da inversão fornece insights sobre quais regras possuem essa característica e
como usá-las eficientemente.

Lema Chave:
Suponha que π é uma derivação que termina com uma aplicação da regra de corte
aplicada a uma fórmula de classificação d, enquanto a classificação de qualquer outra
fórmula de corte em π é estritamente menor do que d. Então π pode ser transformado em uma
derivação π0 com o mesmo sequente final que π e com classificação estritamente menor do
que d.

O "Lema Chave" lida com o conceito de "classificação" em derivações sequentes. Ele

afirma que se você tem uma derivação π que termina com a aplicação da regra de corte
a uma fórmula de classificação d, mas todas as outras fórmulas de corte na derivação
têm classificações estritamente menores do que d, então é possível transformar essa
derivação em uma nova derivação π0 que tem o mesmo antecedente (parte esquerda
do sequente) que π, mas a classificação é estritamente menor do que d. Isso é útil para
simplificar e otimizar derivações complexas.

Com base nesses conceitos, a aplicação da eliminação do corte começa encontrando a

classificação mais alta de qualquer fórmula de corte na derivação e, em seguida, aplicando
uma série de transformações, como já estudado em seções anteriores chamadas "casos-chave".
Esses casos-chave não são exaustivos, mas representam exemplos importantes usados para
compreender o conceito completo da eliminação do corte. Eles ajudam a eliminar todas as
fórmulas de corte com essa classificação. As transformações dependem da estrutura da
fórmula de corte e das últimas regras que foram aplicadas nos ramos da prova. Essas
transformações preservam o resultado final da derivação, mas reduzem sua classificação de
corte. Ao repetir esse processo para classificações mais baixas, é possível obter eventualmente
uma derivação sem cortes.
7 Conclusão

Neste estudo, exploramos os princípios da lógica proposicional e sua relação com os

sequentes de Gentzen. Iniciamos com uma introdução que enfatiza a importância da lógica
proposicional em campos como filosofia, matemática e ciência da computação. Em seguida,
apresentamos os sequentes de Gentzen como uma abordagem formal da lógica proposicional,
discutindo seu significado e introduzindo o cálculo de sequentes como uma ferramenta
fundamental.
Um aspecto crucial deste trabalho foi a análise da regra do corte, que desempenha um
papel central na dedução de teoremas a partir de sequentes. Exploramos sua relevância para a
estruturação de argumentos válidos e sua conexão com a síntese de prova.
Além disso, investigamos o teorema da eliminação do corte, evidenciando como
simplifica provas complexas e destaca a eficácia do cálculo de sequentes em demonstrações
formais.
No entanto, é importante reconhecer as limitações deste estudo, incluindo a exclusão
da lógica de predicados, uma extensão fundamental da lógica proposicional, bem como o fato
de que o teorema da eliminação do corte não foi estudado exaustivamente. Este estudo
fornece apenas uma introdução ao conceito, sem aprofundar em exemplos práticos. Assim, há
espaço suficiente para investigações adicionais na área da lógica de predicados e sua relação
com os sequentes de Gentzen, bem como a exploração de exemplos práticos e aplicações do
teorema da eliminação do corte.
As contribuições deste trabalho abrangem uma exploração aprofundada dos conceitos
básicos da lógica proposicional e dos sequentes de Gentzen, com ênfase na importância da
regra do corte e do teorema da eliminação do corte. Esperamos que este estudo tenha
fornecido uma base sólida para aqueles que desejam compreender e aplicar esses conceitos
em suas pesquisas e trabalhos acadêmicos.
Por fim, apontamos para várias áreas promissoras de pesquisa futura, como a
aplicação prática dos sequentes de Gentzen em domínios específicos, exploração de extensões
da lógica proposicional, como a lógica de predicados, e investigação de técnicas avançadas de
prova e simplificação de argumentos. O campo da lógica oferece vastas oportunidades de
exploração, e este trabalho pode servir como um ponto de partida sólido para pesquisas
futuras nessa direção.
Assim, concluímos esta pesquisa, esperando que tenha contribuído para uma
compreensão mais profunda da lógica proposicional e dos sequentes de Gentzen, bem como
para inspirar futuras investigações neste fascinante campo.
8 Bibliografia

[1] STANFORD ENCYCLOPEDIA OF PHILOSOPHY. The Development of Proof Theory.

Stanford, 2014. Disponível
em:https://plato.stanford.edu/entries/proof-theory-development/#PreNotPro . Acesso em:
24 set. 2023.
[2] GENTZEN, Gerhard. Investigations into logical deduction. American Philosophical
Quarterly, Urbana, v. 1, n. 4, p. 288-306, Oct. 1964.
[3] MANCOSU, P.; GALVAN, S.; ZACH, R. An Introduction to Proof Theory:
Normalization, Cut-Elimination, and Consistency Proofs. Oxford: Oxford University
Press, 2021. DOI: 10.1093/oso/9780192895936.001.0001.
[4] GIRARD, J.-Y. Proofs and types [Internet]. Translated and with appendices by Taylor, P.
and Lafont, Y. Cambridge: Cambridge University Press, 1989. Disponível em:
https://www.paultaylor.eu/stable/prot.pdf. Acesso em: 24 set. 2023.
[5] VAN BENTHEM, Johan. Cut elimination. Amsterdam: Institute for Logic, Language and
Computation, 2011. Disponível em:
https://staff.fnwi.uva.nl/j.vanbenthem/teaching/CutElimination.pdf. Acesso em: 10 jul.
2021.
[6] MARTINS, A. T.; OLIVEIRA, A. G. de; QUEIROZ, R. J. G. B. de. Uma introdução à
teoria da prova. In: SIMPÓSIO BRASILEIRO DE MÉTODOS FORMAIS, 1., 1998, Belo
Horizonte. Anais… Belo Horizonte: UFMG, 1998. p. 1-20.