Um estudo de Lógica Linear com Subexponenciais...Um estudo de lógica linear com subexponenciais / Laura Fernandes Dell Orto. Natal, 20 17 . 109 f. Orientador: Prof. Dr. Carlos Alberto

Universidade Federal do Rio Grande do NorteCentro de Ciências Exatas e da Terra

Programa de Pós-Graduação em Matemática Aplicadae Estatística

Mestrado em Matemática Aplicada e Estatística

Um estudo de Lógica Linear comSubexponenciais

Laura Fernandes Dell Orto

Natal-RN

Fevereiro de 2017

Laura Fernandes Dell Orto

Um estudo de Lógica Linear com Subexponenciais

Trabalho apresentado ao Programa de Pós-Graduação em Matemática Aplicada e Es-tatística da Universidade Federal do RioGrande do Norte, em cumprimento com asexigências legais para obtenção do título deMestre.Área de Concentração: Modelagem Matemá-tica.Linha de Pesquisa: Matemática Computaci-onal

Orientador(a)

Prof. Dr. Carlos Alberto Olarte Vega

Universidade Federal do Rio Grande do Norte – UFRNPrograma de Pós-Graduação em Matemática Aplicada e Estatística –

PPGMAE

Natal-RN

Fevereiro de 2017

Catalogação da Publicação na Fonte. UFRN / SISBI / Biblioteca Setorial Especializada do Centro de Ciências Exatas e da Terra – CCET.

Dell Orto, Laura Fernandes. Um estudo de lógica linear com subexponenciais / Laura Fernandes Dell Orto. – Natal, 2017. 109f.

Orientador: Prof. Dr. Carlos Alberto Olarte Vega. Dissertação (Mestrado) – Universidade Federal do Rio Grande do Norte. Centro

de Ciências Exatas e da Terra. Programa de Pós-Graduação em Matemática Aplicada e Estatística.

1. Lógica Matemática - Dissertação. 2. Teoria da prova - Dissertação. 3.

Eliminação do corte - Dissertação. 4. Lógica linear - Dissertação. 5. Lógica linear com subexponenciais - Dissertação. I. Vega, Carlos Alberto Olarte. II. Título.

RN/UF/BSE-CCET CDU: 510.6

Dissertação de Mestrado sob o título Um estudo de Lógica Linear com Subexponenciais

apresentada por Laura Fernandes Dell Orto e aceita pelo Programa de Pós-Graduação

em Matemática Aplicada e Estatística da Universidade Federal do Rio Grande do Norte,

sendo aprovada por todos os membros da banca examinadora abaixo especificada:

Professor Doutor Carlos Alberto Olarte VegaOrientador(a)

Escola de Ciência e TecnologiaUniversidade Federal do Rio Grande do Norte

Professora Doutora Elaine Gouvêa PimentelDepartamento de Matemática

Universidade Federal do Rio Grande do Norte

Professor Doutor Mário Sérgio AlvimDepartamento de Ciência da ComputaçãoUniversidade Federal de Minas Gerais

Natal-RN, 15 de Fevereiro de 2017.

Aos meus pais.

Agradecimentos

Seria impossível agradecer a todos aqui.

Primeiramente, gostaria de agradecer ao meu orientador Carlos Alberto Olarte Vega,

por toda a atenção e paciência ao longo desses dois anos. Ele foi uma das pessoas que

mais me motivou e inspirou para continuar estudando e escrevendo, sempre atencioso e

solícito com tudo que precisei. Gostaria de agradecer também à professora Elaine Gouvea

Pimentel, que também me orientou quando necessário e dispôs muito do seu tempo para

que esse trabalho pudesse ser concluído.

Agradeço muito à minha família: meus pais, Eloiza e Vinicius, e meu irmão, Bruno. A

paciência, compreensão e ajuda deles em vários momentos foi fundamental nessa jornada.

Não menos importante, agradeço também à minha família que não mora conosco: meus

avós, tios e primos, que tantas vezes deixei de visitar e estar com eles em momentos

importantes para poder me dedicar a este trabalho.

Sou imensamente grata também a todos meus amigos. Seria impossível citar todos

aqui. Agradeço principalmente aos meus amigos da Liga N-Blast, a quem devo muito apoio

ao longo desses dois anos. Agradeço também a todos os Sihings e Sijehs da Academia Tat

Wong de Kung Fu. Por muitas vezes, quando estamos desanimados mentalmente, a prática

do Kung Fu nos estimula e nos ensina a ter persistência e excelência em tudo que fazemos

na nossa vida.

Este trabalho teria sido impossível de ser realizado sem a ajuda de todas as minhas

colegas de trabalho do Núcleo de Estudos em Saúde Coletiva (NESC/UFRN), onde sou

técnica administrativa. Seria impossível finalizar esse trabalho sem ajuda e compreensão

delas em todas as minhas ausências para assistir aulas e estudar. Agradeço também às

minhas chefias e aos coordenadores e vice-coordenadores do NESC durante esses dois

anos.

E, por fim, agradeço à UFRN por me dar o direito de poder conciliar trabalho e estudo,

algo bastante difícil. Trabalho como técnica-admistrativa na UFRN desde 2014 e sem a

liberdade para estudar que a UFRN concede aos seus funcionários teria sido impossível

concluir este trabalho.

I’m not a linear logician.

Jean-Yves Girard

Um estudo de Lógica Linear com Subexponenciais

Autor: Laura Fernandes Dell Orto

Orientador(a): Prof. Dr. Carlos Alberto Olarte Vega

Resumo

Em Lógica Clássica, podemos utilizar as hipóteses um número indeterminado de vezes.

Por exemplo, a prova de um teorema pode fazer uso do mesmo lema várias vezes. Porém,

em sistemas físicos, químicos e computacionais a situação é diferente: um recurso não

pode ser reutilizado após ser consumido em uma ação. Em Lógica Linear, fórmulas são

vistas como recursos a serem utilizados durante a prova. É essa noção de recursos que

faz a Lógica Linear ser interessante para a modelagem de sistemas. Para tanto, a Lógica

Linear controla o uso da contração e do enfraquecimento através dos exponenciais ! e

?. Este trabalho tem como objetivo fazer um estudo sobre a Lógica Linear com Subex-

ponenciais (SELL), que é um refinamento da Lógica Linear. Em SELL, os exponenciais

da Lógica Linear possuem índices, isto é, ! e ? serão substituídos por !i e ?i, onde “i” é

um índice. Um dos pontos fundamentais de Teoria da Prova é a prova da Eliminação do

Corte, que neste trabalho é demonstrada tanto para Lógica Linear como para SELL, onde

apresentamos detalhes que normalmente são omitidos. A partir do teorema de Elimina-

ção do Corte, podemos concluir a consistência do sistema (para as lógicas que estamos

utilizando) e outros resultados como a propriedade de subfórmula. O trabalho inicia-se

com um capítulo de Teoria da Prova, e em seguida se faz uma exposição sobre a Lógica

Linear. Assim, com essas bases, apresenta-se a Lógica Linear com Subexponenciais. SELL

tem sido utilizada, por exemplo, na especificação e verificação de diferentes sistemas tais

como sistemas bioquímicos, sistemas de interação multimídia e, em geral, em sistemas

concorrentes com modalidades temporais, espaciais e epistêmicas. Com essa base teórica

bastante clara, apresenta-se a especificação de um sistema bioquímico utilizando SELL.

Além disso, apresentamos várias instâncias de SELL que tem interpretações interessantes

do ponto de vista computacional.

Palavras-chave: Lógica Matemática, Teoria da Prova, Eliminação do Corte, Lógica Linear,

Lógica Linear com Subexponenciais.

A study of Linear Logic with Subexponentials

Author: Laura Fernandes Dell Orto

Advisor: Prof. Dr. Carlos Alberto Olarte Vega

Abstract

In Classical Logic, we can use a given hypothesis an indefinite number of times. For

example, the proof of a theorem may use the same lemma several times. However, in

physical, chemical and computational systems, the situation is different: a resource can-

not be reused after being consumed in one action. In Linear Logic, formulas are seen

as resources to be used during a proof. This feature makes Linear Logic an interesting

formalism for the specification and verification of such systems. Linear Logic controls the

rules of contraction and weakening through the exponentials ! and ?. This work aims to

study Linear Logic with subexponentials (SELL), which is a refinement of Linear Logic.

In SELL, the exponentials of Linear Logic are decorated with indexes, i.e., ! and ? are

replaced with !i and ?i, where “i” is an index. One of the main results in Proof Theory is

the Cut-Elimination theorem. In this work we demonstrate that theorem for both Linear

Logic and SELL, where we present details that are usually omitted in the literature. From

the Cut-Elimination Theorem, we can show, as a corollary, the consistency of the system

(for the logics considered here) and other results as the subformula property. This work

begins with an introduction to Proof Theory and then, it presents Linear Logic. On these

bases, we present Linear Logic with subexponentials. SELL has been used, for example,

in the specification and verification of various systems such as biochemical systems, mul-

timedia interaction systems and, in general, concurrent systems with temporal, spatial

and epistemic modalities. Using the theory of SELL, we show the specification of a bi-

ochemical system. Moreover, we present several instances of SELL that have interesting

interpretations from a computational point of view.

Keywords : Mathematical Logic, Proof Theory, Cut-Elimination, Linear Logic, Linear Lo-

gic with Subexponenciais.

Lista de símbolos

⇒ “deduz” ou “prova”

⊃ Implicação

∧ Conjunção

∨ Disjunção

` Turnstile

∃ Existe

∀ Para todo

⊗ Times

⊕ Plus

& With

O Par

> Top

⊥ Bottom

! Bang ou Of course

? Why not ou Question mark

( Entails

e Cap

d Cup

Sumário

1 Introdução p. 11

2 Teoria da Prova p. 14

2.1 Cálculo de Sequentes para a Lógica Intuicionista . . . . . . . . . . . . . p. 14

2.2 Admissibilidade do Corte . . . . . . . . . . . . . . . . . . . . . . . . . . p. 23

2.3 Lógica de Primeira Ordem . . . . . . . . . . . . . . . . . . . . . . . . . p. 31

2.3.1 Os quantificadores no Cálculo de Sequentes . . . . . . . . . . . . p. 33

2.3.2 Admissibilidade do Corte . . . . . . . . . . . . . . . . . . . . . . p. 37

3 Lógica Linear p. 41

3.1 Lógica Linear Intuicionista . . . . . . . . . . . . . . . . . . . . . . . . . p. 48

3.2 Admissibilidade do Corte na Lógica Linear . . . . . . . . . . . . . . . . p. 50

4 Lógica Linear com Subexponenciais (SELL) p. 72

4.1 Sintaxe . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . p. 73

4.2 Estrutura Algébrica dos Subexponenciais . . . . . . . . . . . . . . . . . p. 74

4.3 Sistema SELLSΣ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . p. 77

4.4 Sistema SELLSe . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . p. 87

5 Especificação de sistemas bioquímicos em SELL p. 98

6 Considerações finais p. 106

Referências p. 108

11

1 Introdução

Lógica e Teoria da Prova tem sido excelentes ferramentas para estudar sistemas for-

mais. Sistemas naturais (físicos e químicos) são, em geral, modelados com base em expe-

rimentos e observações. Através de sistemas formais, podemos compreender melhor esses

sistemas reais por meio de um conjunto bem organizado de hipóteses, definições, teore-

mas, lemas, corolários, etc. Além disso, sistemas formais são bastante úteis no estudo de

modelos abstratos (matemáticos e computacionais) devido ao seu rigor na apresentação

dos conceitos e resultados.

A Lógica de Primeira Ordem é um dos principais ramos da lógica mais estudados hoje

por causa de suas aplicações nos fundamentos da matemática. Podemos afirmar que, por

volta de 1900, a lógica moderna foi concebida como uma teoria de sentenças, conjuntos

e relações e em torno de 1940–1950 o paradigma do sistema lógico se tornou a Lógica de

Predicados (ou Cálculo de Predicados)1.

A Lógica Intuicionista (também chamada de Lógica Construtivista) surgiu com o pro-

prósito de utilizar provas construtivistas nos sistemas formais: um prova só é válida em

Lógica Intuicionista se houver uma prova direta da sentença. Do ponto de vista compu-

tacional, esse é um bom sistema por utilizar somente provas diretas. Na Lógica Clássica,

toda proposição tem atribuído um valor verdadeiro ou falso independente de termos pro-

vas diretas em ambos os casos. Na Lógica Intuicionista, uma proposição só é considerada

verdadeira ou falsa caso haja uma prova direta para tal afirmação. Todos os sistemas

apresentados neste trabalho serão intuicionistas, salvo quando apresentamos brevemente

o sistema clássico para uma abordagem introdutória do assunto.

Já as Lógicas Subestruturais são lógicas não-clássicas construídas de forma a não pos-

suir uma ou mais regras estruturais da Lógica Clássica. Uma das Lógicas Subestruturais

mais utilizadas é a Lógica Linear (GIRARD, 1986), que não possui as regras de enfra-

quecimento e contração. Com isso, as informações não pode ser simplesmente copiadas1Lógica de Predicados (ou Cálculo de Predicados) é um termo genérico para a Lógica de Primeira

Ordem.

12

e utilizadas indefinidamente como acontece na Lógica Clássica. Isso faz com que a Ló-

gica Linear seja um bom formalismo para modelar sistemas reias, pois no mundo real

dificilmente se trabalha com recursos infinitos. Neste trabalho, apresentaremos a Lógica

Linear e um refinamento dela: a Lógica Linear com Subexponenciais (SELL) (OLARTE;

PIMENTEL; NIGAM, 2015). SELL se mostrará bastante útil para modelar outros aspectos

de sistemas, como modalidades espaciais e temporais.

A Lógica Matemática é tradicionalmente dividida em quatro partes: Teoria dos Con-

juntos, Teoria dos Modelos, Teoria da Recursão, Teoria da Prova e Matemática Constru-

tiva (BARWISE, 1977). Neste trabalho, iremos nos focar em Teoria da Prova. Dedicaremos

o capítulo 2 para expor os principais conceitos de Teoria de Prova necessários para o

objetivo desse trabalho.

Neste trabalho iremos realizar um estudo de Lógica Linear com Subexponenciais com

foco na admissibilidade do corte. A regra de corte é uma regra que introduz um lema para

podermos provar o sequente. Iremos provar a admissibilidade do corte em três sistemas:

G3ip (capítulo 2), Lógica Linear Intuicionista (capítulo 3) e Lógica Linear com Subex-

ponenciais (capítulo 4). Em muitos casos, a consistência do sistema é imediata quando a

admissibilidade do corte é demonstrada, daí vem a importância dessa prova neste trabalho.

E, por fim, no capítulo 5, especificaremos um sistema bioquímico utilizando o forma-

lismo de SELL. Devido aos índices nos exponenciais, SELL permite especificar modali-

dades espaciais e temporais. Isso se mostrará bastante útil na descrição de evolução do

sistema.

Dessa forma, o trabalho possui a seguinte estrutura:

1. Introdução

2. Teoria da Prova: neste capítulo apresentamos o sistema G3ip (que é um sistema

intuicionista) e provamos a admissibilidade do corte nesse sistema. Provaremos tam-

bém a admissibilidade das regras estruturais (contração e enfraquecimento).

3. Lógica Linear: capítulo fundamental para o trabalho. Apresenta-se uma breve intro-

dução de Lógica Linear Clássica e em seguida apresenta-se a Lógica Linear Intui-

cionista. Assim, prova-se a admissibilidade do corte na Lógica Linear Intuicionista,

apresentando com detalhes casos normalmente omitidos.

4. Lógica Linear com Subexponenciais: apresenta-se a Lógica Linear com Subexpo-

nenciais e demonstra-se a admissibilidade do corte nos sistemas SELLSΣ (sistema

13

SELLS com uma assinatura exponencial Σ) e SELLSe (sistema SELLS com os quan-

tificados e e d) (OLARTE; PIMENTEL; NIGAM, 2015) com detalhes normalmente omi-

tidos. Trabalharemos com o sistema SELL intuicionista, daí vem o motivo de nos

capítulos anteriores provarmos a admissibilidade do corte somente para sistemas

intuicionistas.

5. Especificação de sistemas bioquímicos em SELL: neste capítulo iremos especificar

um sistema bioquímico utilizando o formalismo de SELL.

6. Conclusões: conclusões sobre o trabalho e perspectivas futuras.

14

2 Teoria da Prova

Teoria da Prova é um dos ramos da Lógica Matemática que estuda a estrutura e as

propriedades das provas matemáticas. Em sua tese de doutorado, Gerhard Gentzen (1909

- 1945) introduziu o Cálculo de Sequentes no início da década de 1930. Em sua tese,

Gentzen propõe duas formulações principais para sistemas de regras lógica: a dedução

natural e o cálculo de sequentes.

Neste trabalho, não entramos em detalhes sobre dedução natural. Iremos utilizar

apenas o cálculo de sequentes, que será abordado na próxima seção. O sistema de dedução

natural pode ser visto com detalhes em (TROELSTRA; SCHWICHTENBERG, 2000).

2.1 Cálculo de Sequentes para a Lógica Intuicionista

O Cálculo de Sequentes que utilizaremos neste trabalho surgiu em 1934, por Gerhard

Gentzen, como uma forma de estudo mais prática da Dedução Natural. Isso se deve ao

fato de que no Cálculo de Sequentes possuímos um maior controle dos antecedentes e

sucedentes, pois, diferentemente da dedução natural, se trabalha com sequentes e não

com fórmulas.

Gentzen apresentou os sistemas LK e LJ (também chamados de G-systems) que tra-

tavam, respectivamente, da Lógica de Primeira Ordem Clássica e da Lógica de Primeira

Ordem Intuicionista (TROELSTRA; SCHWICHTENBERG, 2000). Os sistemas propostos ori-

ginalmente por Gentzen, chamados G1 e G2, não serão abordados aqui. Nesses sistemas,

as regras de enfraquecimento e contração são regras que fazem parte das regras lógicas do

sistema. Já no sistema G3 essas regras são admissíveis. Utilizaremos aqui o sistema G3 e

provaremos a admissibilidade da regra de corte:

Γ⇒ D D,∆⇒ CCut

Γ,∆⇒ C

15

Nesta dissertação iremos abordar somente o Cálculo de Sequentes para a Lógica In-

tuicionista. Portanto, nesse capítulo, descreveremos o sistema G3ip e iremos nos focar na

admissibilidade da regra de corte. Isso se faz necessário pois no Capítulo 4 iremos provar

o mesmo para a Lógica Linear com Subexponenciais. Abaixo, seguem as regras do sistema

G3ip1.

Sistema G3ip

Axioma Inicial

axiomA, Γ ⇒ A

Regras Lógicas

⊥L⊥, Γ ⇒ CA ⊃ B, Γ ⇒ A B, Γ ⇒ C

⊃LA ⊃ B, Γ ⇒ C

A, Γ ⇒ B⊃R

Γ ⇒ A ⊃ B

A, B, Γ ⇒ C∧L

A ∧ B, Γ ⇒ CΓ ⇒ A Γ ⇒ B ∧R

Γ ⇒ A ∧ B

A, Γ ⇒ C B, Γ ⇒ C∨L

A ∨ B, Γ ⇒ CΓ ⇒ A ∨R1

Γ ⇒ A ∨ BΓ ⇒ B ∨R2

Γ ⇒ A ∨ B

Observação 2.1. A fórmula principal é a fórmula da conclusão na qual a regra lógica é

aplicada.

No Cálculo de Sequentes proposto por Gentzen, o contexto das regras é um con-

texto compartilhado, ou seja, ao aplicar uma regra o contexto Γ permanece o mesmo

nas premissas esquerda e direita (exceto em Cut, porém isso será discutido mais a frente

no final da seção 2.2). Na regra de Cut, é introduzido um lema D, e mostraremos que

essa regra é admissível. A negação e a equivalência são definidas como ¬A = A ⊃ ⊥ e

A ≡ B = (A ⊃ B) ∧ (B ⊃ A).

Notação. Quando derivamos fórmulas e sequentes, devemos especificar em qual for-

malismo estamos derivando. Para o sequente Γ⇒ ∆ derivado no formalismo K, escreve-

mos

`K Γ⇒ ∆

Na próxima seção mostraremos que a regra de corte é admissível em G3ip. Para

provar a admissibilidade, utilizaremos indução na ordem lexicográfica do par ordenado

(W,H) (essa ordem será melhor explicada na próxima seção).1G3 se refere ao terceiro refinamento do sistema de Gentzen e ip significa “intuitionistic propositional”

16

Definição 2.1 (Admissibilidade). Dado um sistema de regras G, dizemos que uma regra

com premissas S1,...,Sn e conclusão S é admissível em G se, sempre que uma instância

de S1,...,Sn é derivável em G, a instância correspondente de S é derivável em G.

Em outras palavras, uma regra é admissível em um sistema de regras G quando o

conjunto de resultados desse sistema não se altera com a inclusão dessa nova regra. Ou

seja, a regra admissível é uma regra redundante: sempre que houver uma prova com uma

regra admissível, existe uma prova sem utilizar essa regra.

Definição 2.2 (Peso de uma fórmula). O peso w(A) de uma fórmula A é definido indu-

tivamente por

w(⊥) = 0

w(p) = 1, onde um átomo p é uma fórmula que não contém conectivos lógicos.

w(A ◦ B) = w(A) + w(B) + 1, onde ◦ = ∧,∨,⊃

Notação. `n Γ⇒ C significa: o sequente Γ⇒ C é derivável com uma altura máxima

de derivação n.

Definição 2.3 (Altura de uma derivação). Uma derivação em G3ip é ou um axioma, ou

uma instância de ⊥L, ou a aplicação de uma regra lógica a derivações cujas conclusões são

premissas da regra utilizada. A altura de uma derivação é o maior número de aplicações

sucessivas de regras na derivação , onde um axioma e ⊥L tem altura 0.

Podemos definir a altura de uma derivação indutivamente. O caso n = 0 são as regras

⊥L e axiom:

axiom`0 Γ, P ⇒ P⊥L`0 Γ,⊥ ⇒ C

Para regras que possuem uma premissa, temos:

`n Γ′ ⇒ C ′

`n+1 Γ⇒ C

Para regras que possuem duas premissa, temos:

`n Γ′ ⇒ C ′ `m Γ′′ ⇒ C ′′

`max(n,m)+1 Γ⇒ C

17

Além das regras apresentadas no sistema G3ip, existem ainda as Regras Estrutu-

rais. Estas são admissíveis no sistema. São elas enfraquecimento, contração e corte. A

admissibilidade do corte será detalhada na próxima sessão.

Regras Estruturais

Γ ⇒ CW

D, Γ ⇒ CD, D, Γ ⇒ C

CD, Γ ⇒ C

Γ ⇒ D D, ∆ ⇒ CCut

Γ, ∆ ⇒ C

Intuitivamente, o enfraquecimento nos diz que introduzir uma hipótese não altera a

nossa prova e a contração nos diz que repetir uma hipótese também não altera nossa prova.

Nos teoremas 2.1 e 2.2, provaremos a admissibilidade da contração e do enfraquecimento

(NEGRI; PLATO, 2001). Já a regra de corte introduz um lema D para provarmos o sequente

Γ,∆⇒ C. A admissibilidade do corte será demonstrada na próxima seção.

Lema 2.1 (Lema da Inversão). As seguintes afirmações são verdadeiras:

• Se `n A ∧B,Γ⇒ C, então `n A,B,Γ⇒ C;

• Se `n A ∨B,Γ⇒ C, então `n A,Γ⇒ C e `n B,Γ⇒ C;

• Se `n A ⊃ B,Γ⇒ C então `n B,Γ⇒ C.

Demonstração.

• Se `n A ∧B,Γ⇒ C, então `n A,B,Γ⇒ C

Caso base: se n = 0, então (i) C é um átomo e C ∈ Γ, logo o sequente A ∧B,Γ⇒ C

termina com a regra axiom, então A,B,Γ⇒ C também termina com a regra axiom. (ii)

Se ⊥ ∈ Γ, logo A ∧ B,Γ ⇒ C termina com a regra ⊥L, então A,B,Γ ⇒ C também

termina com a regra ⊥L.

Hipótese indutiva: assuma que o lema da inversão vale para uma altura ≤ n e seja

`n+1 A ∧B,Γ⇒ C. Temos dois casos:

(i) A ∧ B é a fórmula principal, então a premissa A,B,Γ ⇒ C tem uma derivação de

altura n

`n A,B,Γ⇒ C∧L`n+1 A ∧B,Γ⇒ C

18

(ii) A∧B não é a fórmula principal. Considere, por exemplo, o caso em que C = C1∨C2

`n A ∧B,Γ⇒ C1 ∨R`n+1 A ∧B,Γ⇒ C1 ∨ C2

Pela hipótese indutiva, temos `n A,B,Γ⇒ C1. Pela regra ∨R, temos

`n A,B,Γ⇒ C1 ∨R`n+1 A,B,Γ⇒ C1 ∨ C2

que é o sequente `n+1 A,B,Γ⇒ C1 ∨ C2 que queríamos provar.

No caso geral, quando A ∧B não é principal, se temos

`n A ∧B,Γ′ ⇒ C ′

`n+1 A ∧B,Γ⇒ C

então, pela hipótese indutiva, temos `n A,B,Γ′ ⇒ C ′. Qualquer regra que aplicar-

mos teremos `n+1 A,B,Γ⇒ C.

• Se `n A ∨B,Γ⇒ C, então `n A,Γ⇒ C e `n B,Γ⇒ C

Caso base: se n = 0, então (i) C é um átomo e C ∈ Γ, logo o sequente A ∨B,Γ⇒ C

termina com a regra axiom, então A,Γ⇒ C e B,Γ⇒ C também terminam com a regra

axiom. (ii) Se ⊥ ∈ Γ, logo A ∨ B,Γ ⇒ C termina com a regra ⊥L, então A,Γ ⇒ C e

B,Γ⇒ C também terminam com a regra ⊥L.


`n+1 A ∨B,Γ⇒ C. Temos dois casos:

(i) A ∨ B é a fórmula principal, então as premissas A,Γ ⇒ C e B,Γ ⇒ C tem uma

derivação de altura n

`n A,Γ⇒ C `n B,Γ⇒ C∨L`n+1 A ∨B,Γ⇒ C

(ii) A∨B não é a fórmula principal. Considere, por exemplo, o caso em que C = C1∨C2

`n A ∨B,Γ⇒ C1 ∨R`n+1 A ∨B,Γ⇒ C1 ∨ C2

Pela hipótese indutiva, temos `n A,Γ⇒ C1 e `n B,Γ⇒ C1. Pela regra ∨R, temos

19

`n A,Γ⇒ C1 ∨R`n+1 A,Γ⇒ C1 ∨ C2

`n B,Γ⇒ C1 ∨R`n+1 B,Γ⇒ C1 ∨ C2

que são os sequente `n+1 A,Γ ⇒ C1 ∨ C2 e `n+1 B,Γ ⇒ C1 ∨ C2 que queríamos

provar.

No caso geral, quando A ∨B não é principal, se temos

`n A ∨B,Γ′ ⇒ C ′

`n+1 A ∨B,Γ⇒ C

então, pela hipótese indutiva, temos `n A,Γ′ ⇒ C ′ e `n B,Γ′ ⇒ C ′. Qualquer regra

que aplicarmos teremos `n+1 A,Γ⇒ C e `n+1 B,Γ⇒ C.

• Se `n A ⊃ B,Γ⇒ C então `n B,Γ⇒ C

Caso base: se n = 0, então (i) C é um átomo e C ∈ Γ, logo o sequente A ⊃ B,Γ⇒ C

termina com a regra axiom, então B,Γ⇒ C também termina com a regra axiom. (ii) Se

⊥ ∈ Γ, logo A ⊃ B,Γ ⇒ C termina com a regra ⊥L, então B,Γ ⇒ C também termina

com a regra ⊥L.


`n+1 A ⊃ B,Γ⇒ C. Temos dois casos:

(i) A ⊃ B é a fórmula principal, então a premissa B,Γ ⇒ C tem uma derivação de

altura n

`n A ⊃ B,Γ⇒ A `n B,Γ⇒ C⊃L`n+1 A ⊃ B,Γ⇒ C

(ii) A ⊃ B não é a fórmula principal. Considere, por exemplo, o caso em que C = C1∨C2

`n A ⊃ B,Γ⇒ C1 ∨R`n+1 A ⊃ B,Γ⇒ C1 ∨ C2

Pela hipótese indutiva, temos `n B,Γ⇒ C1. Pela regra ∨R, temos

`n B,Γ⇒ C1 ∨R`n+1 B,Γ⇒ C1 ∨ C2

que é o sequente `n+1 B,Γ⇒ C1 ∨ C2 que queríamos provar.

No caso geral, quando A ⊃ B não é principal, se temos

20

`n A ⊃ B,Γ′ ⇒ C ′

`n+1 A ⊃ B,Γ⇒ C

então, pela hipótese indutiva, temos `n B,Γ′ ⇒ C ′. Qualquer regra que aplicarmos

teremos `n+1 B,Γ⇒ C.

QED.

Teorema 2.1 (Preservação da altura da Contração). Se `n D,D,Γ ⇒ C, então `nD,Γ⇒ C.

Demonstração. A prova é por indução na altura da derivação n.

Caso base: se n = 0, então (i) C é um átomo e C ∈ {D,D,Γ} e o sequenteD,D,Γ⇒ C

termina com a regra axiom, logo C ∈ {D,Γ} e D,Γ ⇒ C também termina com a regra

axiom. (ii) Se D,D,Γ⇒ C termina com ⊥L, então ⊥L ∈ {D,D,Γ}, logo ⊥L ∈ {D,Γ} eD,Γ⇒ C também termina com ⊥L.

Hipótese indutiva: assuma que a preservação da altura da contração é admissível para

derivações com altura ≤ n. Temos dois casos:

(i) D não é a fórmula principal. Considere, por exemplo, o caso em que C = C1 ∨ C2

`n D,D,Γ⇒ C1

`n+1 D,D,Γ⇒ C1 ∨ C2

Pela hipótese indutiva temos `n D,Γ⇒ C1. Pela regra ∨R, temos

`n D,Γ⇒ C1 ∨R`n+1 D,Γ⇒ C1 ∨ C2

que é o sequente `n+1 D,Γ⇒ C1 ∨ C2 que queríamos provar.

Em geral, quando D não é principal, se temos

`n D,D,Γ′ ⇒ C ′

`n+1 D,D,Γ⇒ C

então, pela hipótese indutiva, temos `n D,Γ′ ⇒ C ′. Qualquer regra que aplicarmos

teremos `n+1 D,Γ ⇒ C. O mesmo vale para regras que possuem duas premissas.

Suponha, por exemplo, Γ = Γ′, A ⊃ B

21

`n A ⊃ B,D,D,Γ′ ⇒ A `m D,D,Γ′, B ⇒ C⊃L`max(n,m)+1 D,D,Γ

′, A ⊃ B ⇒ C

Pela hipótese indutiva, temos `n A ⊃ B,D,Γ′ ⇒ A e `m D,Γ′, B ⇒ C. Pela regra

⊃L, temos

`n A ⊃ B,D,Γ′ ⇒ A `m D,Γ′, B ⇒ C⊃L`max(n,m)+1 D,Γ

′, A ⊃ B ⇒ C

(ii) D é principal na última regra que conclui as premissas de contração. Então temos

três subcasos:

• D = A ∧B

Temos o último passo da derivação:

`n A,B,A ∧B,Γ⇒ C∧L`n+1 A ∧B,A ∧B,Γ⇒ C

Pelo lema da inversão, sabemos que `n A,B,A,B,Γ ⇒ C. Por hipótese in-

dutiva (aplicada duas vezes), temos `n A,B,Γ ⇒ C. Aplicando a regra ∧L,temos

`n A,B,Γ⇒ C∧L`n+1 A ∧B,Γ⇒ C

• D = A ∨B


`n A,A ∨B,Γ⇒ C `n B,A ∨B,Γ⇒ C∨L`n+1 A ∨B,A ∨B,Γ⇒ C

Pelo lema da inversão, sabemos que `n A,A,Γ ⇒ C e `n B,B,Γ ⇒ C. Por

hipótese indutiva, temos `n A,Γ ⇒ C e `n B,Γ ⇒ C. Aplicando a regra ∨L,temos

`n A,Γ⇒ C `n B,Γ⇒ C∨L`n+1 A ∨B,Γ⇒ C

• D = A ⊃ B


`n A ⊃ B,A ⊃ B,Γ⇒ A `n B,A ⊃ B,Γ⇒ C⊃L`n+1 A ⊃ B,A ⊃ B,Γ⇒ C

Pela hipótese indutiva na primeira premissa, temos `n A ⊃ B,Γ ⇒ A. Pelo

lema da inversão na segunda premissa, temos `n B,B,Γ ⇒ C. Por hipótese

indutiva, temos `n B,Γ⇒ C. Aplicando a regra ⊃L, temos

22

`n A ⊃ B,Γ⇒ A `n B,Γ⇒ C⊃L`n+1 A ⊃ B,Γ⇒ C

QED.

Teorema 2.2 (Preservação da altura do Enfraquecimento). Se `n Γ ⇒ C, então `nD,Γ⇒ C para um D arbitrário.

Demonstração. A prova é por indução na altura da derivação n.

Caso base: se n = 0, então (i) C é um átomo e C ∈ Γ e o sequente Γ ⇒ C termina

com a regra axiom, logo C ∈ {D,Γ} e D,Γ ⇒ C também termina com a regra axiom.

(ii) Se Γ ⇒ C termina com ⊥L, então ⊥L ∈ Γ, logo ⊥L ∈ {D,Γ} e D,Γ ⇒ C também

termina com ⊥L.

Hipótese indutiva: assuma que a preservação da altura do enfraquecimento é admis-

sível para derivações com altura ≤ n.

Se a última regra aplicada foi ∧L, onde Γ = A ∧B,Γ′, temos o último passo:

`n A,B,Γ′ ⇒ C∧L`n+1 A ∧B,Γ′ ⇒ C

Pela hipótese indutiva, `n D,A,B,Γ′ ⇒ C. Então, aplicando de ∧L,

`n D,A,B,Γ′ ⇒ C∧L`n+1 D,A ∧B,Γ′ ⇒ C

que é o sequente `n+1 D,A ∧ B,Γ′ ⇒ C que queríamos provar. Qualquer regra que

aplicamos teremos `n+1 D,A ∧ B,Γ′ ⇒ C. O mesmo vale para regras que possuem duas

premissas. Suponha, por exemplo, Γ = Γ′, A ⊃ B

`n A ⊃ B,Γ′ ⇒ A `m Γ′, B ⇒ C⊃L`max(n,m)+1 Γ′, A ⊃ B ⇒ C

Pela hipótese indutiva, temos `n D,A ⊃ B,Γ′ ⇒ A e `m D,Γ′, B ⇒ C. Pela regra

⊃L, temos

`n D,A ⊃ B,Γ′ ⇒ A `m D,Γ′, B ⇒ C⊃L`max(n,m)+1 D,Γ

′, A ⊃ B ⇒ C

QED.

23

2.2 Admissibilidade do Corte

Agora, iremos apresentar o principal resultado desse capítulo: a admissibilidade do

corte em G3ip. A regra de corte nos diz que é possível provar o sequente Γ,∆ ⇒ C se

podemos “adivinhar” um lema D.

Γ⇒ D D,∆⇒ CCut

Γ,∆⇒ C

A prova utiliza indução na ordem lexicográfica do par ordenado (W,H), onde W é o

peso do corte (definição 2.5) e H é a altura do corte (definição 2.4).

Como dito no início do capítulo, uma regra admissível é uma regra redundante: os

resultados não se alteram com a inclusão dessa nova regra. Dessa forma, a regra de corte

facilita algumas provas. Mas se existe uma prova utilizando a regra do corte, então existe

também uma prova sem utilizar a regra do corte.

Definição 2.4 (Altura do Corte). A altura de uma regra de corte (altura do corte) em

uma derivação é a soma das alturas de derivação das duas premissas do corte.

Notação. A notação

π1

...Γ ⇒ D

π2

...D, ∆ ⇒ C

CutΓ, ∆ ⇒ C

significa que o sequente Γ ⇒ D possui uma derivação π1 de altura n e o sequente

D,∆ ⇒ C possui uma derivação π2 de altura m. Logo, esse corte possui uma altura

n+m. Da mesma forma, uma derivação π3 possui uma altura k.

Definição 2.5 (Peso do corte). O peso do corte é o peso w(D) da fórmula de corte D.

Teorema 2.3 (Eliminação do Corte). A regra de corte

Γ ⇒ D D, ∆ ⇒ CCut

Γ, ∆ ⇒ C

é admissível em G3ip.

24

Demonstração.

A prova procede por indução na ordem lexicográfica do par ordenado (W,H), onde

W é o peso (ou complexidade) da fórmula de corte e H é a altura do corte. Como W

e H são bem-fundados, podemos mostrar que a ordem lexicográfica definida como “se

(w1, h1) > (w2, h2), então ou w1 > w2, ou w1 = w2 e h1 > h2” também é uma ordem bem

fundada.

Mostraremos que o corte é admissível para o caso base (0, 0), ou seja, quando W = 0

e H = 0. Esse é o nosso caso base para indução. Depois utilizamos indução na ordem

lexicográfica do par ordenado (W,H).

Caso base: (W,H) = (0, 0)

Para W = 0, temos que D = ⊥. Temos a derivação com altura de corte zero, onde

⊥ ∈ Γ para que H = 0

⊥L⊥,Γ′ ⇒ ⊥⊥L⊥,∆⇒ CCut

Γ,∆⇒ C

Transformamos então em uma derivação sem corte

⊥L⊥,Γ′,∆⇒ C

Casos indutivos: a demonstração será dividida nos seguintes casos:

O corte possui pelo menos um axioma ou conclusão de ⊥L como premissa

1. A premissa esquerda Γ⇒ D do corte é um axioma ou conclusão de ⊥L.

2. A premissa direita D,∆⇒ C é um axioma ou conclusão de ⊥L.

O corte não possui nem axioma nem conclusão de ⊥L como premissas

3. A fórmula D no corte não é principal na premissa esquerda.

4. A fórmula D no corte não é principal na premissa direita.

5. A fórmula D no corte é principal em ambas as premissas.

25

Para provar o caso (w, h) com w 6= 0 e/ou h 6= 0, vamos assumir, por indução, que

todo corte com peso w′ e altura h′ pode ser eliminado, onde (w′, h′) < (w, h). Ou seja,

usaremos indução na ordem lexicográfica do par ordenado (W,H).

Segue a demonstração para cada caso com seus respectivos subcasos:

1. A premissa esquerda Γ⇒ D do corte é um axioma ou conclusão de ⊥L.

1.1. A fórmula D no corte está em Γ

Γ = Γ′, D

AxiomΓ′, D ⇒ D D,∆⇒ C

CutΓ′, D,∆⇒ C

Neste caso, Γ,∆⇒ C deriva de D,∆⇒ C por enfraquecimento.

1.2. ⊥ é uma fórmula em Γ

Temos uma derivação com altura de corte n, onde Γ = Γ′,⊥

⊥L

Γ′,⊥ ⇒ D

π1

...∆, D ⇒ C

CutΓ′,⊥,∆⇒ C

Transformamos em uma derivação sem corte

⊥L

Γ′,⊥,∆⇒ C

2. A premissa direita D,∆⇒ C é um axioma ou conclusão de ⊥L.

2.1. C está em ∆

Temos uma derivação com altura de corte n, onde ∆ = ∆′, C

π1

...Γ⇒ D

axiom∆′, C,D ⇒ C

CutΓ,∆′, C ⇒ C


axiomΓ,∆′, C ⇒ C

2.2. C = D

26

Γ⇒ CAxiom

C,∆⇒ CCut

Γ,∆⇒ C

Neste caso, Γ,∆⇒ C deriva de Γ⇒ C por enfraquecimento

2.3. ⊥ é uma fórmula em ∆

Temos uma derivação com altura de corte n, onde ∆ = ∆′,⊥π1

...Γ⇒ D

⊥L

∆′,⊥, D ⇒ CCut

Γ,∆′,⊥ ⇒ C


⊥L

Γ,∆′,⊥ ⇒ C


3.1. ∧L, com Γ = A ∧B,Γ′

A derivação com uma altura de corte n+ 1 +m é

π1

...A,B,Γ′ ⇒ D

∧LA ∧B,Γ′ ⇒ D

π2

...D,∆⇒ C

CutA ∧B,Γ′,∆⇒ C

Permutando o corte, temos uma derivação com altura de corte n+m

π1

...A,B,Γ′ ⇒ D

π2

...D,∆⇒ C

CutA,B,Γ′,∆⇒ C

∧LA ∧B,Γ′,∆⇒ C

3.2. ∨L, com Γ = A ∨B,Γ′

A derivação com uma altura de corte max(n,m) + 1 + k é

π1

...A,Γ′ ⇒ D

π2

...B,Γ′ ⇒ D

∨LA ∨B,Γ′ ⇒ D

π3

...D,∆⇒ C

CutA ∨B,Γ′,∆⇒ C

27

Permutando o corte, temos duas derivações com alturas de corte n+ k e m+ k

π1

...A,Γ′ ⇒ D

π3

...D,∆⇒ C

CutA,Γ′,∆⇒ C

π2

...B,Γ′ ⇒ D

π3

...D,∆⇒ C

CutB,Γ′,∆⇒ C

∨LA ∨B,Γ′,∆⇒ C

3.3. ⊃L, com Γ = A ⊃ B,Γ′


π1

...A ⊃ B,Γ′ ⇒ A

π2

...B,Γ′ ⇒ D

⊃L

A ⊃ B,Γ′ ⇒ D

π3

...D,∆⇒ C

CutA ⊃ B,Γ′,∆⇒ C

Permutando o corte, temos uma derivação com altura de corte m+ k

π1

...A ⊃ B,Γ′ ⇒ A

WA ⊃ B,Γ′,∆⇒ A

π2

...B,Γ′ ⇒ D

π3

...D,∆⇒ C

CutB,Γ′,∆⇒ C

⊃L

A ⊃ B,Γ′,∆⇒ C


4.1. ∧L, com ∆ = A ∧B,∆′

A derivação com uma altura de corte n+m+ 1 é

π1

...Γ⇒ D

π2

...D,A,B,∆′ ⇒ C

∧LD,A ∧B,∆′ ⇒ C

CutΓ, A ∧B,∆′ ⇒ C


π1

...Γ⇒ D

π2

...D,A,B,∆′ ⇒ C

CutΓ, A,B,∆′ ⇒ C

∧LΓ, A ∧B,∆′ ⇒ C

4.2. ∨L, com ∆ = A ∨B,∆′

A derivação com uma altura de corte n+max(m, k) + 1 é

28

π1

...Γ⇒ D

π2

...D,A,∆′ ⇒ C

π3

...D,B,∆′ ⇒ C

∨LD,A ∨B,∆′ ⇒ C

CutΓ, A ∨B,∆′ ⇒ C

Permutando o corte, temos duas derivações com alturas de corte n+m e n+k

π1

...Γ⇒ D

π2

...D,A,∆′ ⇒ C

CutΓ, A,∆′ ⇒ C

π1

...Γ⇒ D

π3

...D,B,∆′ ⇒ C

CutΓ, B,∆′ ⇒ C

∨LΓ, A ∨B,∆′ ⇒ C

4.3. ⊃L, com ∆ = A ⊃ B,∆′


π1

...Γ⇒ D

π2

...D,A ⊃ B,∆′ ⇒ A

π3

...D,B,∆′ ⇒ C

⊃L

D,A ⊃ B,∆′ ⇒ CCut

Γ, A ⊃ B,∆′ ⇒ C


π1

...Γ⇒ D

π2

...D,A ⊃ B,∆′ ⇒ A

CutΓ, A ⊃ B,∆′ ⇒ A

π1

...Γ⇒ D

π3

...D,B,∆′ ⇒ C

CutΓ, B,∆′ ⇒ C

⊃L

Γ, A ⊃ B,∆′ ⇒ C

4.4. ∧R, com C = A ∧B


π1

...Γ⇒ D

π2

...D,∆⇒ A

π3

...D,∆⇒ B

∧RD,∆⇒ A ∧B

CutΓ,∆⇒ A ∧B


π1

...Γ⇒ D

π2

...D,∆⇒ A

CutΓ,∆⇒ A

π1

...Γ⇒ D

π3

...D,∆⇒ B

CutΓ,∆⇒ B

∧RΓ,∆⇒ A ∧B

29

4.5. ∨R, com C = A ∨B

As derivações com alturas de corte n+m+ 1 e n+ k + 1 são

π1

...Γ⇒ D

π2

...D,∆⇒ A

∨R1

D,∆⇒ A ∨BCut

Γ,∆⇒ A ∨B

π1

...Γ⇒ D

π3

...D,∆⇒ B

∨R2

D,∆⇒ A ∨BCut

Γ,∆⇒ A ∨B

Permutando os cortes, temos as derivações com alturas de corte n+m e n+ k

π1

...Γ⇒ D

π2

...D,∆⇒ A

CutΓ,∆⇒ A

∨R1

Γ,∆⇒ A ∨B

π1

...Γ⇒ D

π3

...D,∆⇒ B

CutΓ,∆⇒ B

∨R2

Γ,∆⇒ A ∨B

4.6. ⊃R, com C = A ⊃ B


π1

...Γ⇒ D

π2

...D,A,∆⇒ B

⊃RD,∆⇒ A ⊃ B

CutΓ,∆⇒ A ⊃ B


π1

...Γ⇒ D

π2

...D,A,∆⇒ B

CutΓ, A,∆⇒ B

⊃RΓ,∆⇒ A ⊃ B


5.1. D = A ∧B

A derivação com peso de corte w(A ∧B) é

π1

...Γ⇒ A

π2

...Γ⇒ B ∧R

Γ⇒ A ∧B

π3

...A,B,∆⇒ C

∧LA ∧B,∆⇒ C

CutΓ,∆⇒ C

Obtemos então dois cortes com complexidades (pesos) w(B) e w(A)

30

π2

...Γ⇒ B

π1

...Γ⇒ A

π3

...A,B,∆⇒ C

CutΓ, B,∆⇒ C

CutΓ,Γ,∆⇒ C

CΓ,∆⇒ C

5.2. D = A ∨B

A derivação com peso de corte w(A ∨B) é

π1

...Γ⇒ A ∨R1

Γ⇒ A ∨B

π2

...A,∆⇒ C

π3

...B,∆⇒ C

∨LA ∨B,∆⇒ C

CutΓ,∆⇒ C

Obtemos então um corte com complexidade (peso) menor w(A)

π1

...Γ⇒ A

π2

...A,∆⇒ C

CutΓ,∆⇒ C

O caso onde onde escolhemos B em ∨R2 é similar.

5.3. D = A ⊃ B

A derivação com uma altura de corte n+ 1 +max(m, k) + 1 e peso w(A ⊃ B)

é

π1

...A,Γ⇒ B

⊃RΓ⇒ A ⊃ B

π2

...A ⊃ B,∆⇒ A

π3

...B,∆⇒ C

⊃LA ⊃ B,∆⇒ C

CutΓ,∆⇒ C

Obtemos então uma derivação com três cortes. No primeiro e no segundo corte,

os pesos foram reduzidos para w(A) e w(B). No terceiro corte, o peso perma-

neceu o mesmo e a altura foi reduzida para n+ 1 +m

π1

...A,Γ⇒ B

⊃RΓ⇒ A ⊃ B

π2

...A ⊃ B,∆⇒ A

CutΓ,∆⇒ A

π1

...A,Γ⇒ B

π3

...B,∆⇒ C

CutA,Γ,∆⇒ C

CutΓ,∆⇒ C

5.4. D = ⊥

Temos

31

Γ⇒ ⊥⊥L⊥,∆⇒ CCut

Γ,∆⇒ C

Existem duas possibilidades para este caso:

(i) Γ⇒ ⊥ termina em zero passos e Γ,∆⇒ C segue como no caso 1

(ii) Γ⇒ ⊥ é derivado por uma regra da esquerda (casos 3.1-3.3)

QED.

2.3 Lógica de Primeira Ordem

Nesta seção, estenderemos a Lógica Proposicional apresentada anteriormente. Na se-

ção anterior, as fórmulas representavam proposições sem argumentos. Agora, vamos es-

tender nossa abordagem para a Lógica de Primeira Ordem, também chamada de Lógica

de Predicados. Em Lógica de Primeira Ordem os átomos tem o formato P (t1, ..., tn), ou

seja, os predicados possuem argumentos. Isso nos trás um dos principais pontos desta

seção: os quantificadores ∃ e ∀ . Nas próximas seções trataremos esses quantificadores

com mais detalhes.

Definição 2.6 (Alfabeto da Lógica de Primeira Ordem).

• a, b, ... ou a1, a2, ... ou a, a′, ... são constantes;

• x, y, ... ou x1, x2, ... ou x, x′, ... são variáveis;

• f(x1, ..., xn), g(x1, ..., xn), ... são funções com aridade n, para n ≥ 0;

• P (x1, ..., xn), Q(x1, ..., xn), ... são predicados com aridade n, para n ≥ 0;

• ⊥ é o conectivo com aridade zero;

• Os conectivos com aridade n=1 são os quantificadores ∃ e ∀;

• Os conectivos com aridade n=2 são ∧,∨ e ⊃.

Termos são representados por t1, t2, ... ou t, t′, ... Definimos os termos indutivamente:

• Constantes são termos;

• Variáveis são termos;

32

• Aplicação de uma função f aos termos t1, ..., tn nos fornece o termo f(t1, ...tn).

Fórmulas são representadas indutivamente por:

• ⊥ é uma fórmula;

• A aplicação de um predicado P aos termos t1, ..., tn nos dá a fórmula P (t1, ..., tn);

• Se A e B são fórmulas, então A ∧B, A ∨B e A ⊃ B são fórmulas;

• Se A é uma fórmula, então ∀xA e ∃xA são fórmulas.

O conjunto de variáveis livres FV (t) em um termo t é definido indutivamente por: 2

• Para t = a, FV (a) = ∅;

• Para t = x, FV (t) = {x};

• Para t = f(t1, ..., tn), FV (f(t1, ..., tn)) = FV (t1) ∪ ... ∪ FV (tn).

O conjunto de variáveis livres FV (A) em uma fórmula A é definido indutivamente

por:

• FV (⊥) = ∅;

• FV (P (t1, ..., tn)) = FV (t1) ∪ ... ∪ FV (tn);

• FV (A ∧B) = FV (A ∨B) = FV (A ⊃ B) = FV (A) ∪ FV (B);

• FV (∀xA) = FV (∃xA) = FV (A)− {x}.

Dizemos que um termo t é livre para x ∈ A se, quando substituímos x por t em A,

nenhum termo t torna-se ligado em A.

Em Lógica de Primeira Ordem vale também o princípio da α-equivalência (ou α-

conversão): as variáveis ligadas podem ser renomeadas, isto é, modificamos o símbolo

que as representa, desde que esse novo símbolo já não esteja presente na expressão. Por

exemplo, se y não ocorre em A(x), então ∀xA(x) ≡ ∀yA(y) e ∃xA(x) ≡ ∃yA(y) são

exemplos de α-equivalências.2F.V. é a abreviação de “Free Variables”

33

Considere uma fórmula A e um termo t. A variável livre x em A pode ser substituída

por um termo t. Utilizamos a notação [t/x] para indicar que a variável x foi substituída

pelo termo t. A seguir, definimos a substituição indutivamente em fórmulas e termos.

Substituição [t/x] em um termo:

• a(t/x) = a;

• y(t/x) = y se y 6= x e y(t/x) = t se y = x;

• f(t1, ..., tn)(t/x) = f(t1(t/x), ..., tn(t/x)).

Substituição [t/x] em uma fórmula:

• ⊥(t/x) = ⊥;

• (P (t1, ..., tn))(t/x) = P (t1(t/x), ..., tn(t/x));

• (A ◦B)(t/x) = A(t/x) ◦B(t/x), para ◦ = ∧,∨,⊃;

• (∀yA)(t/x) = ∀yA(t/x) se y 6= x e (∀yA)(t/x) = ∀yA se y = x;

• (∃yA)(t/x) = ∃yA(t/x) se y 6= x e (∃yA)(t/x) = ∃yA se y = x;

2.3.1 Os quantificadores no Cálculo de Sequentes

Quando escrevemos A(y/x), significa que estamos substituindo x por um y arbitrário.

Já quando escrevemos A(t/x), significa que estamos substituindo x por um t particu-

lar. O cálculo de sequentes para a Lógica de Primeira Ordem é obtido adicionando os

quantificados nas regras G3ip:

Sistema G3i

A(t/x),∀xA,Γ⇒ C∀L∀xA,Γ⇒ C

Γ⇒ A(y/x)∀R

Γ⇒ ∀xA

A(y/x),Γ⇒ C∃L∃xA,Γ⇒ C

Γ⇒ A(t/x)∃R

Γ⇒ ∃xA

34

onde y é uma variável fresca.

Será mostrado que os teoremas, definições e lemas da Lógica Proposicional continuam

válidos para os quantificadores.

Observe que na regra ∀R está implícito que y não pode ocorrer livre em A. Podemos

então dar o seguinte significado a essas regras:

• Uma prova direta de ∀xA consiste de uma prova de A(y/x) para um y arbitrário;

• Uma prova direta de ∃xA consiste de uma prova de A(t/x) para um t particular.

Estendemos a Definição 2.2 e o peso das fórmulas com quantificadores é dado por

w(∀xA) = w(A) + 1

w(∃xA) = w(A) + 1

A altura da derivação é definida da mesma forma mostrada para G3ip.

Lema 2.2 (Preservação da altura da α-conversão). Dado uma derivação D de Γ⇒ C em

G3i, essa derivação pode ser transformada em uma derivação D′ de Γ′ ⇒ C ′ onde Γ′, C ′

e D′ diferem de Γ, C e D apenas pela substituição dos símbolos das variáveis ligadas por

símbolos de variáveis frescas.

Demonstração. A prova procede por indução na altura da derivação.

Caso base: se n = 0, então Γ⇒ C é um axioma ou conclusão de ⊥L. Assim, o mesmo

ocorre com Γ′ ⇒ C ′, onde os símbolos das variáveis ligadas ligadas foram trocados por

símbolos das variáveis frescas.

Caso indutivo: suponha que Γ⇒ C possui uma derivação de altura ≤ n. Se aplicarmos

regras proposicionais (∧,∨,⊃), a renomeação das variáveis da conclusão é obtida através

das premissas. Considere, por exemplo, o caso ∨R onde C = A ∨B

`n Γ⇒ A∨R`n+1 Γ⇒ A ∨B

`n Γ′ ⇒ A′∨R

`n+1 Γ′ ⇒ (A ∨B)′

Para os quantificadores, os casos são mais interessantes. Considere, por exemplo, a

regra ∀L

`n A(t/x), ∀xA,Γ′ ⇒ C ′∀L`n+1 ∀xA,Γ′ ⇒ C ′

35

Trocando x pela variável fresca y, pela hipótese indutiva, temos a premissa com mesma

altura

`n A(y/x)(t/y), (∀yA)(y/x),Γ′ ⇒ C ′

Aplicando ∀L, temos a derivação

`n A(y/x)(t/y), (∀yA)(y/x),Γ′ ⇒ C ′∀L`n+1 (∀yA)(y/x),Γ′ ⇒ C ′

onde `n+1 (∀yA)(y/x),Γ′ ⇒ C ′ é o sequente que queríamos provar. Os casos ∃L e ∃Rsão obtidos de forma similar. QED.

Lema 2.3 (Lema da Substituição). Se Γ ⇒ C é derivável em G3i e t é livre para

x ∈ {Γ, C} então Γ(t/x)⇒ C(t/x) é derivável em G3i com a mesma altura de derivação.

Demonstração. A demonstração é por indução na altura da derivação.

Caso base: se Γ ⇒ C é um axioma ou conclusão de ⊥L então Γ(t/x) ⇒ C(t/x)

também é um axioma ou conclusão de ⊥L, pois (i) se C ∈ Γ então C(t/x) ∈ Γ(t/x) (ii)

se ⊥ ∈ Γ então ⊥ ∈ Γ(t/x).

Caso indutivo: suponha que o lema vale para altura ≤ n.

Considere, por exemplo, que a última regra aplicada foi ∨R, onde C = A ∨B

`n Γ⇒ A∨R

`n+1 Γ⇒ (A ∨B)

Por hipótese indutiva, temos

`n Γ(t/x)⇒ A(t/x)

Aplicando ∨R

`n Γ(t/x)⇒ A(t/x)∨R

`n+1 Γ(t/x)⇒ (A ∨B)(t/x)

Se t é livre para x ∈ {A∨B} então t é livre para x ∈ A (pois a regra ∨R não altera o

conjunto de variáveis livres e ligadas). Então Γ⇒ C possui a mesma altura de derivação

que Γ(t/x) ⇒ C(t/x). O mesmo vale para as demais regras dos operadores ∧,∨,⊃. Os

casos mais interessantes são quando aplicamos as regras ∀ e ∃.

(i) Se Γ⇒ C é derivado por ∀L, temos

36

`n A(t/x),∀xA,Γ⇒ C∀L`n+1 ∀xA,Γ⇒ C

Se y 6= x, então, pelo lema da α-conversão, temos

`n A(t′/y),∀yA,Γ′ ⇒ C∀L`n+1 ∀yA,Γ′ ⇒ C

Se t é livre para x ∈ A(t′/x), então, por hipótese indutiva, temos

`n (A(t′/y))(t/x), (∀yA)(t/x),Γ′(t/x)⇒ C(t/x)

As duas substituições (A(t′/y))(t/x) podem ser dadas por uma substituição única:

(A(t′/y))(t/x) = A(t′(t/x)/y, t/x)

Se t é livre para x ∈ {∀yA}, então o termo t não contém a variável y:

(A(t′/y))(t/x) = A(t′(t/x)/y, t/x) = (A(t/x))(t′(t/x)/y)

Então, substituindo no sequente da hipótese indutiva, temos

`n (A(t/x))(t′′/y), (∀yA)(t/x),Γ′(t/x)⇒ C(t/x)

onde t′′ = t′(t/x)

Aplicando ∀L

`n (A(t/x))(t′′/y), (∀yA)(t/x),Γ′(t/x)⇒ C(t/x)∀L`n+1 (∀yA)(t/x),Γ′(t/x)⇒ C(t/x)

onde `n+1 (∀yA)(t/x),Γ′(t/x)⇒ C(t/x) é o sequente que queríamos demonstrar.

(ii) Se Γ⇒ C é derivado por ∀R, temos

`n Γ⇒ A(z/y)∀R`n+1 Γ⇒ ∀yA

onde y 6= x. Por hipótese indutiva, temos

37

`n Γ(t/x)⇒ A(z/y)(t/x)∀R`n+1 Γ(t/x)⇒ (∀yA)(t/x)

Como t é livre para x ∈ {∀yA}, podemos trocar a ordem das substituições e obter

uma derivação de altura ≤ n como queríamos provar

`n Γ(t/x)⇒ A(t/x)(z/y)∀R`n+1 Γ(t/x)⇒ (∀yA)(t/x)

Os casos ∃L e ∃R são similares a ∀R e ∀L.

QED.

2.3.2 Admissibilidade do Corte

Teorema 2.4 (Eliminação do Corte para G3i). A regra de corte é admissível em G3i.

Demonstração. Continuando a prova de admissibilidade de G3ip com a mesma nu-

meração, iremos adicionar os casos em que aparecem os quantificadores.


3.4. ∀L, com Γ = ∀xA,Γ′


π1

...A(t/x), ∀xA,Γ′ ⇒ D

∀L∀xA,Γ′ ⇒ D

π2

...D,∆⇒ C

Cut∀xA,Γ′,∆⇒ C


π1

...A(t/x),∀xA,Γ′ ⇒ D

π2

...D,∆⇒ C

CutA(t/x),∀xA,Γ′,∆⇒ C

∀L∀xA,Γ′,∆⇒ C

3.5. ∃L, com Γ = ∃xA,Γ′


38

π1

...A(y/x),Γ′ ⇒ D

∃L∃xA,Γ′ ⇒ D

π2

...D,∆⇒ C

Cut∃xA,Γ′,∆⇒ C

Neste caso, não podemos simplesmente permutar o corte e obter uma altura

de corte menor, pois a variável fresca de ∃L será outra

π′1...

A(z/x),Γ′ ⇒ D

π2

...D,∆⇒ C

CutA(z/x),Γ′,∆⇒ C

∃L∃xA,Γ′,∆⇒ C

Porém, o lema da substituição nos garante que Γ ⇒ C e Γ(t/x) ⇒ C(t/x)

possuem a mesma altura de derivação, onde t é livre para x em Γ e C. Então

A(y/x),Γ′ ⇒ D e A(z/x),Γ′ ⇒ D possuem a mesma altura de derivação n.

Logo, a permutação do corte nos fornece uma prova de altura n+m.


4.7. ∀L, com ∆ = ∀xA,∆′


π1

...Γ⇒ D

π2

...D,A(t/x),∀xA,∆′ ⇒ C

∀LD, ∀xA,∆′ ⇒ C

Cut∀xA,Γ,∆′ ⇒ C


π1

...Γ⇒ D

π2

...D,A(t/x),∀xA,∆′ ⇒ C

CutA(t/x),∀xA,Γ,∆′ ⇒ C

∀L∀xA,Γ,∆′ ⇒ C

4.8. ∃L, com ∆ = ∃xA,∆′


π1

...Γ⇒ D

π2

...D,A(y/x),∆′ ⇒ C

∃LD, ∃xA,∆′ ⇒ C

Cut∃xA,Γ,∆′ ⇒ C

39

Permutando o corte e pelo lema da substituição (da mesma forma que no caso

3.5), temos uma derivação com altura de corte n+m

π1

...Γ⇒ D

π2′

...D,A(z/x),∆′ ⇒ C

CutA(z/x),Γ,∆′ ⇒ C

∃L∃xA,Γ,∆′ ⇒ C

4.9. ∀R, com C = ∀xA


π1

...Γ⇒ D

π2

...D,∆⇒ A(y/x)

∀RD,∆⇒ ∀xA

CutΓ,∆⇒ ∀xA

Permutando o corte e pelo lema da substituição (da mesma forma que no caso

3.5 e 4.8), temos uma derivação com altura de corte n+m

π1

...Γ⇒ D

π2′

...D,∆⇒ A(z/x)

CutΓ,∆⇒ A(z/x)

∀RΓ,∆⇒ ∀xA

4.10. ∃R, com C = ∃xA


π1

...Γ⇒ D

π2

...D,∆⇒ A(t/x)

∃RD,∆⇒ ∃xA

CutΓ,∆⇒ ∃xA


π1

...Γ⇒ D

π2

...D,∆⇒ A(t/x)

CutΓ,∆⇒ A(t/x)

∃LΓ,∆⇒ ∃xA


40

5.4. D = ∀xA

A derivação com uma altura de corte n+ 1 +m+ 1 e peso w(∀xA) é

π1

...Γ⇒ A(y/x)

∀RΓ⇒ ∀xA

π2

...A(t/x),∀xA,∆⇒ C

∀L∀xA,∆⇒ CCut

Γ,∆⇒ C

Obtemos então dois cortes

π1[t/y]

...Γ⇒ A(t/x)

π1′

...Γ⇒ A(z/x)

∀RΓ⇒ ∀xA

π2

...A(t/x),∀xA,∆⇒ C

CutA(t/x),Γ,∆⇒ C

CutΓ,Γ,∆⇒ C

CΓ,∆⇒ C

No primeiro corte reduzimos o peso para w(A(t/x)). No segundo corte, pelo

lema da substituição, π′1 tem a mesma altura que π1. E então reduzimos a

altura para n+ 1 +m.

5.5. D = ∃xA

A derivação com peso de corte w(∃xA) é

π1

...Γ⇒ A(t/x)

∃RΓ⇒ ∃xA

π2

...A(y/x),∆⇒ C

∃L∃xA,∆⇒ CCut

Γ,∆⇒ C

Obtemos uma derivação com peso de corte w(A(t/x)), onde, pelo lema da

substituição, π′2 tem a mesma altura que π2

π1

...Γ⇒ A(t/x)

π2′

...A(t/x),∆⇒ C

CutΓ,∆⇒ C

QED.

41

3 Lógica Linear

A Lógica Linear é uma Lógica Subestrutural que foi proposta por Jean-Yves Girard

(GIRARD, 1986). A motivação para a criação da Lógica Linear veio da necessidade de

haver mais controle nos recursos utilizados durante a prova. Em lógica clássica temos a

implicação

A ⊃ B

significando, intuitivamente, que podemos utilizar um A para produzir um número in-

determinado de Bs. Em problemas reais, não possuímos infinitos recursos para serem

utilizamos. Por exemplo, suponha uma máquina de café onde inserimos uma moeda A e

em seguida recebemos um café B. Ao receber o café, não recebemos de volta a moeda.

Ou seja, a moeda é um recurso que foi consumido durante a prova.

A implicação A ( B da Lógica Linear consome A para produzir B. Para recuperar

o comportamento clássico, utilizamos !

!A( B

Já a máquina de café, que pode ser utilizada um número indeterminado de vezes e,

em cada uso, uma moeda é consumida para produzir um café, pode ser representada na

Lógica Linear como

!(A( B)

As lógicas subestruturais são caracterizadas por rejeitarem uma ou mais regras es-

truturais. Nesse sentido, em Lógica Linear não é permitido livremente o uso das regras

estruturais de enfraquecimento e contração. As fórmulas representam recursos e recursos

não podem ser usados livremente sem especificar o que foi consumido durante a prova.

42

A Lógica Linear às vezes precisa que algumas fórmulas tenham comportamento “clás-

sico”, ou seja, é preciso se aplicar as regras de enfraquecimento e contração. Diferentemente

de outras lógicas subestruturais, as regras estruturais aparecem em Lógica Linear de forma

controlada através dos operadores ! e ?, como exemplificado anteriormente. Dessa forma,

os exponenciais ! e ? dão às fórmulas um comportamento clássico enquanto que as outras

fórmulas que não possuem os exponenciais têm um comportamento linear: são recursos

finitos durante a prova.

Uma das consequências de não poder utilizar enfraquecimento e contração é o surgi-

mento de mais conectivos lógicos além dos utilizados na Lógica Clássica usual. Por exem-

plo, em Cálculo de Sequentes, podemos introduzir o operador lógico ∧ de duas formas,

como mostrado abaixo para os sistemas S1 e S2:

• introdução da conjunção no sistema S1

Γ1 ⇒ A,∆1 Γ2 ⇒ B,∆2 ∧RΓ1,Γ2 ⇒ A ∧B,∆1,∆2

Γ, A,B ⇒ ∆∧L

Γ, A ∧B ⇒ ∆

• introdução da conjunção no sistema S2

Γ⇒ A,∆ Γ⇒ B,∆∧R

Γ⇒ A ∧B,∆

Γ, A⇒ ∆∧L1

Γ, A ∧B ⇒ ∆Γ, B ⇒ ∆

∧L2

Γ, A ∧B ⇒ ∆

Observe que no sistema S1 os contextos são divididos enquanto que no sistema S2 os

contextos são compartilhados.

Podemos mostrar que, na presença das regras de enfraquecimento e contração, os

sistemas S1 e S2 são equivalentes. Mostrando para o caso ∧R:

Γ1 ⇒ A,∆1W

Γ1,Γ2 ⇒ A,∆1,∆2

Γ2 ⇒ B,∆2W

Γ1,Γ2 ⇒ B,∆1,∆2 ∧RΓ1,Γ2 ⇒ A ∧B,∆1,∆2

Note que o sistema S2 segue de S1 quando utilizamos enfraquecimento e contração:

Γ⇒ A,∆ Γ⇒ B,∆∧R

Γ,Γ⇒ A ∧B,∆,∆C

Γ⇒ A ∧B,∆

43

Para provar a equivalência entre S1 e S2, controlamos o enfraquecimento e a contração

na prova. Como em Lógica Linear não existem essas regras, as regras de introdução da

conjunção dos sistemas S1 e S2 correspondem a dois operadores diferentes. O mesmo

vale para os outros operadores ∨,>,⊥, que correspondem a dois operadores diferentes na

Lógica Linear.

Na sintaxe da Lógica Linear Clássica, existem três tipos de conectivos: Multiplicativos

(⊗, O, 1, ⊥), Aditivos (⊕, &, 0, >) e Exponenciais (!, ?). Definimos a linguagem da Lógica

Linear através da notação BNF1:

Definição 3.1 (Sintaxe da Lógica Linear Clássica).

A ::= p | p⊥ | A ⊗ A | A ⊕ A | A & A | A O A | 1 | 0 | > | ⊥ | !A | ?A

| ∃x.A | ∀x.A

onde p é um átomo e A é uma fórmula.

Dessa forma, apresentamos as regras da Lógica Linear Clássica:

Sistema cLL

Regras de identidade

Axiomp⇒ pΓ1 ⇒ B,∆1 Γ2, B ⇒ ∆2

CutΓ1,Γ2 ⇒ ∆1,∆2

Regras de negação

Γ⇒ A,∆(.)⊥L

Γ, A⊥ ⇒ ∆

Γ, A⇒ ∆(.)⊥R

Γ⇒ A⊥,∆

Regras multiplicativas

Γ⇒ ∆1L

Γ, 1⇒ ∆1R⇒ 1

⊥L⊥ ⇒Γ⇒ ∆ ⊥R

Γ⇒ ⊥,∆

Γ1 ⇒ A, ∆1 Γ2 ⇒ B, ∆2 ⊗RΓ1, Γ2 ⇒ A ⊗ B, ∆1, ∆2

Γ, A, B ⇒ ∆⊗L

Γ, A ⊗ B ⇒ ∆

1BNF (Backus-Naur Form ou Backus Normal Form) é uma sintaxe usada para descrever linguagensformais.

44

Γ ⇒ A, B, ∆OR

Γ ⇒ A O B, ∆Γ1, A⇒ ∆1 Γ2, B ⇒ ∆2 OL

Γ1,Γ2, AOB ⇒ ∆1,∆2

Regras aditivas

0LΓ, 0⇒ ∆

>RΓ⇒ >,∆

Γ ⇒ A, ∆ Γ ⇒ B, ∆&R

Γ ⇒ A & B, ∆

Γ, A ⇒ ∆&L1

Γ, A & B ⇒ ∆

Γ, B ⇒ ∆&L2

Γ, A & B ⇒ ∆

Γ ⇒ A,∆⊕R1

Γ ⇒ A ⊕ B, ∆Γ ⇒ B,∆

⊕R2Γ ⇒ A ⊕ B, ∆

Γ, A ⇒ ∆ Γ, B ⇒ ∆⊕L

Γ, A ⊕ B ⇒ ∆

Regras exponenciais

! Γ ⇒ A, ?∆!R

! Γ ⇒ !A, ?∆

! Γ, A ⇒ ?∆?L

! Γ, ?A ⇒ ?∆

Γ, A ⇒ ∆!L

Γ, !A ⇒ ∆

Γ ⇒ A,∆?R

Γ ⇒ ?A,∆

Γ ⇒ ∆!W

Γ, !A ⇒ ∆Γ⇒ ∆

?WΓ⇒?A,∆

Γ, !A, !A ⇒ ∆!C

Γ, !A ⇒ ∆

Γ⇒?A, ?A,∆?C

Γ⇒?A,∆

Regras dos quantificadores

Γ, A(t/x) ⇒ ∆∀L

Γ, ∀xA ⇒ ∆

Γ ⇒ A(y/x), ∆∀R

Γ⇒ ∀xA, ∆

Γ, A(y/x) ⇒ ∆∃L

Γ, ∃xA ⇒ ∆

Γ⇒ A(t/x), ∆∃R

Γ ⇒ ∃xA, ∆

Observe que as fórmulas !A, ?A em !W, !C, ?W, ?C tem comportamento clássico. As

regras !L e ?R transformam uma fórmula clássica em uma fórmula linear, ou seja, a fórmula

A após consumida não poderá mais ser utilizada. Já as regras !R e ?L só permitem que se

introduza os exponenciais se todas as outras fórmulas tiverem comportamento clássico.

45

Dividimos os operadores da Lógica Linear em dois grupos: os multiplicativos e os adi-

tivos. Enquanto os operadores multiplicativos dividem o contexto, os operadores aditivos

possuem contextos compartilhados. Isto é, os operadores multiplicativos utilizam a pre-

missa apenas uma vez e os operadores aditivos utilizam a premissa várias vezes. (REIS,

2010)

Do ponto de vista lógico, podemos ver a Lógica Linear como um refinamento das Ló-

gicas Clássica e Intuicionista. O objetivo da Lógica Linear é conciliar a simetria da Lógica

Clássica com as provas construtivas da Lógica Intuicionista. Enquanto a Lógica Clássica

enfatiza a “verdade” e a Lógica Intuicionista enfatiza a prova, a Lógica Linear enfatiza a

função das fórmulas como recurso, ou seja, ela possui um controle mais preciso sobre as

regras estruturais. A vantagem desse fato é que a dedução lógica não é simplesmente uma

aplicação de regras, e sim uma forma de manipular recursos que nem sempre podem ser

duplicados ou perdidos durante a prova.

Em Lógica Linear, temos duas possíveis leituras para o Princípio do Terceiro Excluído:

A⊕ A⊥ (aditivo)

AOA⊥ (multiplicativo)

A disjunção aditiva é a disjunção da Lógica Intuicionista: não é provável. Ao tentarmos

provar A⊕ A⊥ na Lógica Linear, teremos o mesmo problema que a Lógica Intuicionista:

?...⇒ A ⊕R1

⇒ A⊕ A⊥

?...

⇒ A⊥ ⊕R2

⇒ A⊕ A⊥

Porém, ao se utilizar o exponencial ? para que a fórmula tenha um comportamento

clássico, podemos utilizar a contração e A⊕ A⊥ é facilmente demonstrável:

A⇒ A(.)⊥L⇒ A,A⊥⊕R

⇒ A,A⊕ A⊥⊕R

⇒ A⊕ A⊥, A⊕ A⊥?R

⇒?(A⊕ A⊥), ?(A⊕ A⊥)?C

⇒?(A⊕ A⊥)

Já a disjunção multiplicativa é trivialmente demonstrável, pois corresponde à tauto-

logia A ⊃ A (que é aceitável na Lógica Intuicionista):

46

A⇒ A(.)⊥L⇒ A,A⊥OR

⇒ AOA⊥

Note que na Lógica Linear Clássica não há a implicação linear (. Isso ocorre pois a

implicação pode ser reescrita como

A ( B ≡ A⊥OB

onde a equivalência A˛ B é definida como A˛ B = (A( B)&(B ( A).

Isso é facilmente demonstrável. Basta provar que (A ( B) ˛ (A⊥OB). Primeiro

provemos o sequente ⇒ (A( B) ( (A⊥OB)

A⇒ A B ⇒ B (L

A( B,A⇒ B(.)⊥R

A( B ⇒ A⊥, BOR

A( B ⇒ A⊥OB(R

⇒ (A( B) ( (A⊥OB)

Agora, provemos ⇒ (A⊥OB) ( (A( B)

A⇒ A(.)⊥L

A⊥, A⇒ B ⇒ BOL

A⊥OB,A⇒ B(R

A⊥OB ⇒ A( B(R

⇒ (A⊥OB) ( (A( B)

Como já dito anteriormente, em Lógica Linear existem duas conjunções (⊗ e &) e

duas disjunções (⊕ e O). Enquanto A⊗B nos diz que tanto A quanto B serão realizados,

A&B nos diz que apenas uma das ações será realizada, mas deveremos decidir qual. Já

A ⊕ B nos diz que apenas uma ação será realizada, mas não poderemos decidir qual.

(LINCOLN et al., 1992)

A proposição AOB significa “se não A, então B”. Esse significado torna-se mais claro

quando vemos que A ( B é equivalente a A⊥OB. A fórmula A ( B pode ser pensada

como “podemos obter B consumindo A apenas uma vez”. (LINCOLN, 1992)

Para cada um desses conectivos, existe a sua unidade (ou elemento neutro): 1 é a

unidade de ⊗, > é a unidade de &, ⊥ é a unidade de O e 0 é a unidade de ⊕. Assim,

podemos escrever:

47

⊥OA ≡ A

>&A ≡ A

1⊗ A ≡ A

0⊕ A ≡ A

E, por fim, temos a dualidade dos exponenciais ! e ?. Como dito no início do capítulo,

os operadores exponenciais controlam o enfraquecimento e a contração. Intuitivamente,

podemos enxergar ! como o operador que controla o enfraquecimento e a contração no lado

esquerdo do sequente: !A significa que “temos várias cópias de A” ou que “podemos usar

A zero, uma ou mais vezes”. Enquanto que ?A controla o enfraquecimento e a contração

do lado direito do sequente: ?A significa que “eu posso produzir quantas cópias de A eu

queira” ou que “A pode ser obtido zero, uma ou mais vezes”.

A Lógica Linear possui a negação linear, escrita na forma (.)⊥. Ela nos mostra clara-

mente a dualidade da Lógica Linear. A negação linear se comporta da mesma forma que

a transposição na Álgebra Linear, expressando a mudança de ponto de vista: (GIRARD,

1995)

A negação A⊥ é o inverso da proposição A

Ação do tipo A = Reação do tipo A⊥

A( B ≡ B⊥ ( A⊥

Uma das principais propriedades da negação linear é a dupla negação:

A ≡ A⊥⊥

Isso é facilmente demonstrável, basta provar o sequente ⇒ (A( A⊥⊥)&(A⊥⊥ ( A)

A⇒ A ⊥L

A,A⊥ ⇒⊥R

A⇒ A⊥⊥ (R

⇒ A( A⊥⊥

A⇒ A ⊥R

⇒ A⊥, A⊥L

A⊥⊥ ⇒ A (R

⇒ A⊥⊥ ( A&R

⇒ (A( A⊥⊥)&(A⊥⊥ ( A)

As fórmulas de De Morgan podem ser escritas nessa notação:

48

(p)⊥ = p⊥ (p⊥)⊥

= p

(A⊗B)⊥ = A⊥OB⊥ (AOB)⊥ = A⊥ ⊗B⊥

(A⊕B)⊥ = A⊥&B⊥ (A&B)⊥ = A⊥ ⊕B⊥

(1)⊥ = ⊥ (⊥)⊥ = 1

(0)⊥ = > (>)⊥ = 0

(!A)⊥ =?(A⊥) (?A)⊥ =!(A⊥)

(∀xA)⊥ = ∃xA⊥ (∃xA)⊥ = ∀xA⊥

3.1 Lógica Linear Intuicionista

Na sintaxe da Lógica Linear Intuicionista, existem três tipos de conectivos: Multipli-

cativos (⊗, (, 1), Aditivos (⊕, &, 0, >) e Exponenciais (!). Definimos a linguagem da

Lógica Linear através da notação BNF:

Definição 3.2 (Sintaxe da Lógica Linear Intuicionista).

A ::= p | A⊗ A | A⊕ A | A&A | A( A | 1 | 0 | > |!A |?A | ∃x.A | ∀x.A

onde p é um átomo e A é uma fórmula.

Na Lógica Linear Intuicionista, o conectivo ( agora faz parte da sintaxe. A regras são

as mesmas da Lógica Linear Clássica, porém o lado direito do sequente contém exatamente

uma fórmula. Por esse motivo, os conectivos ⊥ e O foram omitidos. (ROCCA; ROVERSI,

1997) (BENTON et al., 1993) (NIGAM; OLARTE; PIMENTEL, 2016)

Sistema iLL

Regras de identidade

Axiomp ⇒ pΓ ⇒ B ∆, B ⇒ A

CutΓ, ∆ ⇒ A

Regras multiplicativas

Γ⇒ A1L

Γ, 1⇒ A1R⇒ 1

Γ1 ⇒ A Γ2 ⇒ B⊗R

Γ1, Γ2 ⇒ A ⊗ BΓ, A, B ⇒ C

⊗LΓ, A ⊗ B ⇒ C

49

Γ, A ⇒ B(R

Γ ⇒ A ( BΓ1 ⇒ A Γ2, B ⇒ C

(L

Γ1,Γ2, A( B ⇒ C

Regras aditivas

0LΓ, 0⇒ A

>RΓ⇒ >

Γ ⇒ A Γ ⇒ B&R

Γ ⇒ A & B

Γ, A ⇒ C&L1

Γ, A & B ⇒ C

Γ, B ⇒ C&L2

Γ, A & B ⇒ C

Γ ⇒ A ⊕R1Γ ⇒ A ⊕ B

Γ ⇒ B ⊕R2Γ ⇒ A ⊕ B

Γ, A ⇒ C Γ, B ⇒ C⊕L

Γ, A ⊕ B ⇒ C

Regras exponenciais

!Γ ⇒ A!R

!Γ ⇒ !A!Γ, A⇒?B

?L!Γ, ?A⇒?B

Γ, A ⇒ B!L

Γ, !A ⇒ BΓ⇒ A

?RΓ⇒?A

Γ⇒ BW

Γ, !A⇒ BΓ, !A, !A⇒ B

CΓ, !A⇒ B

Regras dos quantificadores

Γ⇒ A(y/x)∀R

Γ⇒ ∀xAΓ, A(t/x)⇒ B

∀LΓ,∀xA⇒ B

onde y não é livre em Γ

Γ⇒ A(t/x)∃R

Γ⇒ ∃xAΓ, A(y/x)⇒ B

∃LΓ,∃xA⇒ B

onde y não é livre nem em Γ nem em B

50

3.2 Admissibilidade do Corte na Lógica Linear

A admissibilidade do corte na Lógica Linear é demonstrada utilizando a mesma ideia

da admissibilidade do corte em G3ip: indução na ordem lexicográfica do par ordenado

(W,H), onde W é o peso do corte e H é a altura do corte.

Definição 3.3 (Peso de uma fórmula). O peso w(A) de uma fórmula A é definido indu-

tivamente por

w(>) = 0, w(1) = 0, w(0) = 0

w(p) = 1, onde um átomo p é uma fórmula que não contém conectivos lógicos.

w(A ◦ B) = w(A) + w(B) + 1, onde ◦ = &,⊗,⊕,(

w(∀xA) = w(A) + 1

w(∃xA) = w(A) + 1

w(!A) = w(A) + 1

w(?A) = w(A) + 1

Além disso, para um dos casos apresentados (ver caso 5.5), será necessário utilizar a

regra Cut!. A regra Cut! é uma generalização derivável da regra de corte:

Lema 3.1. A regra Cut!

Γ⇒!A ∆, (!A)r ⇒ CCut! (r > 1)

Γ,∆⇒ C

é admissível na Lógica Linear Intuicionista, onde (!A)r (r > 1) significa r cópias de !A.

Demonstração. A prova da eliminação de Cut! é similar à prova de eliminação do

corte. Assim como na eliminação do corte, a prova de Cut! procede por indução na ordem

lexicográfica do par ordenado (W,H), e os casos indutivos se subdividem em vários casos.

A grande maioria dos casos é similar a prova do corte que mostraremos a seguir, mas

alguns casos são mais interessantes. Considere por exemplo o caso em que C = F ⊗G.

Temos a derivação com altura de Cut! igual a n+ 1 +max(m, k) + 1

π1

...!Γ⇒ A

!R!Γ⇒!A

π2

...∆1, (!A)r

′ ⇒ F

π3

...∆2, (!A)r

′′ ⇒ G⊗R

∆, (!A)r ⇒ F ⊗GCut!

!Γ,∆⇒ F ⊗G

51

onde r = r′ + r′′ e ∆ = ∆1,∆2.

Transformamos então em duas derivações com alturas de Cut! igual a n + 1 + k e

n+ 1 +m

π1

...!Γ⇒ A

!R!Γ⇒!A

π3

...∆2, (!A)r

′′ ⇒ GCut!

∆2, !Γ⇒ G

π1

...!Γ⇒ A

!R!Γ⇒!A

π2

...(!A)r

′,∆1 ⇒ F

Cut!!Γ,∆1 ⇒ F

⊗R!Γ, !Γ,∆⇒ F ⊗G

!C!Γ,∆⇒ F ⊗G

onde r = r′ + r′′ e ∆ = ∆1,∆2.

QED.

Lema 3.2 (Preservação da altura da α-conversão para a Lógica Linear Intuicionista).

Dado uma derivação D de Γ ⇒ C na Lógica Linear Intuicionista, essa derivação pode

ser transformada em uma derivação D′ de Γ′ ⇒ C ′ onde Γ′, C ′ e D′ diferem de Γ, C e

D apenas pela substituição dos símbolos das variáveis ligadas por símbolos de variáveis

frescas.

Demonstração. A demonstração da Preservação da altura da α-conversão para a Ló-

gica Linear Intuicionista é similar à demonstração em G3i (ver lema 2.2). Vamos consi-

derar, por exemplo, o caso em que a última regra aplicada foi !R

`n!Γ⇒ A!R`n+1!Γ⇒!A


`n!Γ′ ⇒ A′

Aplicando !R

`n!Γ′ ⇒ A′!R`n+1!Γ′ ⇒!A′

QED.

52

Lema 3.3 (Lema da Substituição para a Lógica Linear Intuicionista). Se Γ ⇒ C é

derivável na Lógica Linear Intuicionista e t é livre para x ∈ {Γ, C} então Γ(t/x)⇒ C(t/x)

é derivável na Lógica Linear Intuicionista com a mesma altura de derivação.

Demonstração. A demonstração do Lema da Substituição para a Lógica Linear Intui-

cionista é similar a demonstração em G3i (ver lema 2.3). Vamos considerar, por exemplo,

o caso em que a última regra aplicada foi !R

`n!Γ⇒ A!R`n+1!Γ⇒!A


`n!Γ(t/x)⇒ A(t/x)

Aplicando !R

`n!Γ(t/x)⇒ A(t/x)!R`n+1!Γ(t/x)⇒!A(t/x)

QED.

Teorema 3.1 (Eliminação do corte na Lógica Linear Intuicionista). A regra de corte

Γ⇒ D ∆, D ⇒ CCut

Γ,∆⇒ C

é admissível na Lógica Linear Intuicionista.

Demonstração. A prova procede por indução na ordem lexicográfica do par ordenado

(W,H), onde W é o peso (ou a complexidade) da fórmula de corte e H é a altura da

fórmula de corte (da mesma forma como feito no capítulo 2 para demonstrar o teorema

2.3).

Casos base: (W,H) = (0, 0)

Para W = 0, temos três casos:

(i) D = 0

Temos a derivação com altura de corte zero, onde 0 ∈ Γ para que H = 0

53

0L0,Γ′ ⇒ 0

0L0,∆⇒ C

CutΓ,∆⇒ C


0L0,Γ′,∆⇒ C

(ii) D = >

Temos a derivação com altura de corte zero, onde 0 ∈ ∆ para que H = 0

>RΓ⇒ >

0L>, 0,∆′ ⇒ CCut

Γ, 0,∆′ ⇒ C


0LΓ, 0,∆′ ⇒ C

(iii) D = 1

Temos a derivação com altura de corte zero, onde 0 ∈ Γ para que H = 0

1R⇒ 10L

1, 0,Γ′,∆⇒ CCut

0,Γ′,∆⇒ C


0L0,Γ′,∆⇒ C

Se 0 ∈ ∆, o caso é similar. Outra possibilidade seria C = >, nesse caso os sequentes

terminam com >R.

Casos indutivos: a demonstração será dividida nos seguintes casos

O corte possui pelo menos um axioma ou conclusão de 0L,>R como pre-

missa

1. A premissa esquerda Γ⇒ D do corte é um axioma ou conclusão de 0L,>R.

2. A premissa direita D,∆⇒ C é um axioma ou conclusão de 0L,>R.

54

O corte não possui nem axioma nem conclusão de 0L,>R como premissas





1. A premissa esquerda Γ⇒ D do corte é um axioma ou conclusão de 0L,>R.

1.1. 0 é uma fórmula em Γ

Temos uma derivação com altura de corte n, onde Γ = Γ′, 0

0LΓ′, 0⇒ D

π1

...∆, D ⇒ C

CutΓ′, 0,∆⇒ C


0LΓ′, 0,∆⇒ C

1.2. D = >

Neste caso, temos

>RΓ⇒ > ∆,> ⇒ C

CutΓ,∆⇒ C

Como não existe regra de > à esquerda, o sequente ∆,> ⇒ C corresponde aos

casos em que D não é principal na premissa direita (casos 4.1 a 4.18) e aos

casos 2.1 e 2.2.

2. A premissa direita D,∆⇒ C é um axioma ou conclusão de 0L,>R.

2.1. 0 é uma fórmula em ∆

Temos uma derivação com altura de corte n, onde ∆ = ∆′, 0

π1

...Γ⇒ D

0L∆′, 0, D ⇒ C

CutΓ,∆′, 0⇒ C

55


0LΓ,∆′, 0⇒ C

2.2. C = >

Temos uma derivação com altura de corte n, onde C = >

π1

...Γ⇒ D

>R∆, D ⇒ >

CutΓ,∆⇒ >


>RΓ,∆⇒ >


3.1. &L, com Γ = A&B,Γ′


π1

...A,Γ′ ⇒ D

&L

A&B,Γ′ ⇒ D

π2

...∆, D ⇒ C

CutA&B,Γ′,∆⇒ C


π1

...A,Γ′ ⇒ D

π2

...∆, D ⇒ C

CutA,Γ′,∆⇒ C

&L

A&B,Γ′,∆⇒ C

O caso de &L escolhendo B é similar.

3.2. ⊕L, com Γ = A⊕B,Γ′


π1

...Γ′, A⇒ D

π2

...Γ′, B ⇒ D

⊕L

A⊕B,Γ′ ⇒ D

π3

...∆, D ⇒ C

CutA⊕B,Γ′,∆⇒ C

56

Permutando o corte, temos duas derivações com alturas de corte n+ k e m+ k

π1

...A,Γ′ ⇒ D

π3

...∆, D ⇒ C

CutA,Γ′,∆⇒ C

π2

...B,Γ′ ⇒ D

π3

...∆, D ⇒ C

CutB,Γ′,∆⇒ C

⊕L

A⊕B,Γ′,∆⇒ C

3.3. ⊗L, com Γ = A⊗B,Γ′


π1

...A,B,Γ′ ⇒ D

⊗L

A⊗B,Γ′ ⇒ D

π2

...∆, D ⇒ C

CutA⊗B,Γ′,∆⇒ C


π1

...A,B,Γ′ ⇒ D

π2

...∆, D ⇒ C

CutA,B,Γ′,∆⇒ C

⊗L

A⊗B,Γ′,∆⇒ C

3.4. (L, com Γ = A( B,Γ′ onde Γ′ = Γ′1,Γ′2


π1

...Γ′1 ⇒ A

π2

...Γ′2, B ⇒ D

(L

A( B,Γ′ ⇒ D

π3

...∆, D ⇒ C

CutA( B,Γ′,∆⇒ C

Permutando o corte, temos uma derivação com altura de corte m+ k

π1

...Γ′1 ⇒ A

π2

...Γ′2, B ⇒ D

π3

...∆, D ⇒ C

CutΓ′2,∆, B ⇒ C

(L

A( B,Γ′,∆⇒ C

3.5. !L, com Γ =!A,Γ′

Neste caso, é possível aplicar três regras distintas quando temos ! à esquerda:

dereliction2, contração e enfraquecimento2Uma tradução literal para “Dereliction” é “Abandono”, mas preferimos manter o nome original da

regra.

57

• Dereliction

A derivação com uma altura de corte n+m+ 1 éπ1

...A,Γ′ ⇒ D

!L!A,Γ′ ⇒ D

π2

...∆, D ⇒ C

Cut!A,Γ′,∆⇒ C


π1

...A,Γ′ ⇒ D

π2

...∆, D ⇒ C

CutA,Γ′,∆⇒ C

!L!A,Γ′,∆⇒ C

• Contração

A derivação com uma altura de corte n+ 1 +m éπ1

...!A, !A,Γ′ ⇒ D

C!A,Γ′ ⇒ D

π2

...∆, D ⇒ C



π1

...!A, !A,Γ′ ⇒ D

π2

...∆, D ⇒ C

Cut!A, !A,Γ′,∆⇒ C

C!A,Γ′,∆⇒ C

• Enfraquecimento


...Γ′ ⇒ D

W!A,Γ′ ⇒ D

π2

...∆, D ⇒ C



π1

...Γ′ ⇒ D

π2

...∆, D ⇒ C

CutΓ′,∆⇒ C

W!A,Γ′,∆⇒ C

3.6. ?L, com Γ =?A,Γ′

Temos a derivação

58

π1

...!Γ′, A⇒?D

?L!Γ′, ?A⇒?D

π2

...∆, ?D ⇒ C

Cut!Γ′, ?A,∆⇒ C

Vamos considerar a premissa direita do corte e fazer uma análise dos casos

possíveis para a derivação π2:

• ?D não é principal à direita e aplicamos uma L-rule

Esses casos correspondem aos casos 4.1 a 4.9 e ao caso 2.1

• ?D não é principal à direita e aplicamos uma R-rule


• ?D é principal à direita

A derivação com uma altura de corte n+ 1 +m+ 1 éπ1

...!Γ′, A⇒?D

?L!Γ′, ?A⇒?D

π2

...!∆, D ⇒?C

?L!∆, ?D ⇒?C

Cut!Γ′, ?A, !∆⇒?C

Permutando o corte, temos uma derivação com altura de corte n+m+ 1

π1

...!Γ′, A⇒?D

π2

...!∆, D ⇒?C

?L!∆, ?D ⇒?C

Cut!Γ′, A, !∆⇒?C

?L!Γ′, ?A, !∆⇒?C

3.7. 1 é uma fórmula em Γ

Temos que Γ = 1,Γ′. A derivação com uma altura de corte n+ 1 +m é

π1

...Γ′ ⇒ D

1L1,Γ′ ⇒ D

π2

...D,∆⇒ C

Cut1,Γ′,∆⇒ C


π1

...Γ′ ⇒ D

π2

...∆, D ⇒ C

CutΓ′,∆⇒ C

1L1,Γ′,∆⇒ C

59

3.8. ∀L, com Γ = ∀xA,Γ′


π1

...A(t/x),Γ′ ⇒ D

∀L∀xA,Γ′ ⇒ D

π2

...∆, D ⇒ C

Cut∀xA,Γ′,∆⇒ C


π1

...A(t/x),Γ′ ⇒ D

π2

...∆, D ⇒ C

CutA(t/x),Γ′,∆⇒ C

∀L∀xA,Γ′,∆⇒ C

3.9. ∃L, com Γ = ∃xA,Γ′


π1

...A(y/x),Γ′ ⇒ D

∃L∃xA,Γ′ ⇒ D

π2

...∆, D ⇒ C

Cut∃xA,Γ′,∆⇒ C

Permutando o corte e pelo lema da substituição, temos uma derivação com

altura de corte n+m

π1′

...A(z/x),Γ′ ⇒ D

π2

...∆, D ⇒ C

CutA(z/x),Γ′,∆⇒ C

∃L∃xA,Γ′,∆⇒ C


4.1. &L, com ∆ = A&B,∆′


π1

...Γ⇒ D

π2

...A,∆′, D ⇒ C

&L

A&B,∆′, D ⇒ CCut

Γ, A&B,∆′ ⇒ C


60

π1

...Γ⇒ D

π2

...A,∆′, D ⇒ C


&L

Γ, A&B,∆′ ⇒ C

O caso de &L escolhendo B é similar.

4.2. ⊕L, com ∆ = A⊕B,∆′


π1

...Γ⇒ D

π2

...∆′, D,A⇒ C

π3

...∆′, D,B ⇒ C

⊕L

A⊕B,∆′, D ⇒ CCut

Γ, A⊕B,∆′ ⇒ C


π1

...Γ⇒ D

π2

...∆′, A,D ⇒ C

CutΓ,∆′, A⇒ C

π1

...Γ⇒ D

π3

...∆′, B,D ⇒ C

CutΓ,∆′, B ⇒ C

⊕L

Γ, A⊕B,∆′ ⇒ C

4.3. ⊗L, com ∆ = A⊗B,∆′


π1

...Γ⇒ D

π2

...A,B,∆′, D ⇒ C

⊗L

A⊗B,∆′, D ⇒ CCut

Γ, A⊗B,∆′ ⇒ C


π1

...Γ⇒ D

π2

...A,B,∆′, D ⇒ C

Γ, A,B,∆′ ⇒ C⊗L

Γ, A⊗B,∆′ ⇒ C

4.4. (L, com ∆ = A( B,∆′ onde ∆′ = ∆′1,∆′2


61

π1

...Γ⇒ D

π2

...∆′1 ⇒ A

π3

...∆′2, D,B ⇒ C

(L

A( B,∆′, D ⇒ CCut

Γ, A( B,∆′ ⇒ C

Permutando o corte, temos uma derivação com altura de corte n+ k

π2

...∆′1 ⇒ A

π1

...Γ⇒ D

π3

...∆′2, B,D ⇒ C

Cut∆′2,Γ, B ⇒ C

(L

Γ, A( B,∆′ ⇒ C

4.5. !L, com ∆ =!A,∆′


dereliction, contração e enfraquecimento

• Dereliction


π1

...Γ⇒ D

π2

...D,A,∆′ ⇒ C

!LD, !A,∆′ ⇒ C

CutΓ, !A,∆′ ⇒ C


π1

...Γ⇒ D

π2

...D,A,∆′ ⇒ C


!LΓ, !A,∆′ ⇒ C

• Contração


π1

...Γ⇒ D

π2

...D, !A, !A,∆′ ⇒ C

CD, !A,∆′ ⇒ C



π1

...Γ⇒ D

π2

...D, !A, !A,∆′ ⇒ C

CutΓ, !A, !A,∆′ ⇒ C

CΓ, !A,∆′ ⇒ C

62

• Enfraquecimento


π1

...Γ⇒ D

π2

...D,∆′ ⇒ C

WD, !A,∆′ ⇒ C



π1

...Γ⇒ D

π2

...∆′, D ⇒ C

CutΓ,∆′ ⇒ C

WΓ, !A,∆′ ⇒ C

4.6. ?L, com ∆ =?A,∆′

Temos a derivação

π1

...Γ⇒!D

π2

...A, !∆′, !D ⇒?C

?L?A, !∆′, !D ⇒?C

CutΓ, ?A, !∆′ ⇒?C

Vamos considerar a premissa esquerda do corte e fazer uma análise dos casos


• !D não é principal à esquerda


• !D é principal à esquerda


...!Γ⇒ D

!R!Γ⇒!D

π2

...A, !∆′, !D ⇒?C

?L?A, !∆′, !D ⇒?C

Cut!Γ, ?A, !∆′ ⇒?C

Permutando o corte, temos uma derivação com altura de corte n+ 1 +m

π1

...!Γ⇒ D

!R!Γ⇒!D

π2

...A, !∆′, !D ⇒?C

Cut!Γ, A, !∆′ ⇒?C

?L!Γ, ?A, !∆′ ⇒?C

4.7. 1 é uma fórmula em ∆

Temos que ∆ = 1,∆′. A derivação com uma altura de corte n+m+ 1 é

63

π1

...Γ⇒ D

π2

...D,∆′ ⇒ C

1LD, 1,∆′ ⇒ C

CutΓ,∆⇒ C


π1

...Γ⇒ D

π2

...∆′, D ⇒ C

CutΓ,∆′ ⇒ C

1LΓ, 1,∆′ ⇒ C

4.8. ∀L, com ∆ = ∀xA,∆′


π1

...Γ⇒ D

π2

...A(t/x),∆′, D ⇒ C

∀L∀xA,∆′, D ⇒ CCut

Γ,∀xA,∆′ ⇒ C


π1

...Γ⇒ D

π2

...A(t/x),∆′, D ⇒ C

CutΓ, A(t/x),∆′ ⇒ C

∀LΓ,∀xA,∆′ ⇒ C

4.9. ∃L, com ∆ = ∃xA,∆′


π1

...Γ⇒ D

π2

...A(y/x),∆′, D ⇒ C

∃L∃xA,∆′, D ⇒ CCut

Γ,∃xA,∆′ ⇒ C

Permutando o corte e pelo lema da α-conversão, temos uma derivação com

altura de corte n+m

64

π1

...Γ⇒ D

π2′

...A(z/x),∆′, D ⇒ C

CutΓ, A(z/x),∆′ ⇒ C

∃LΓ,∃xA,∆′ ⇒ C

Como y pode estar livre em Γ, podemos substituí-lo por z assumindo que z

não ocorre livre em D, ∆′ e Γ.

4.10. &R, com C = A&B


π1

...Γ⇒ D

π2

...∆, D ⇒ A

π3

...∆, D ⇒ B

&R∆, D ⇒ A&B

CutΓ,∆⇒ A&B


π1

...Γ⇒ D

π2

...∆, D ⇒ A

CutΓ,∆⇒ A

π1

...Γ⇒ D

π3

...∆, D ⇒ B

CutΓ,∆⇒ B

&RΓ,∆⇒ A&B

4.11. ⊕R, com C = A⊕B


π1

...Γ⇒ D

π2

...∆, D ⇒ A

⊕R∆, D ⇒ A⊕B

CutΓ,∆⇒ A⊕B


π1

...Γ⇒ D

π2

...∆, D ⇒ A

CutΓ,∆⇒ A

⊕RΓ,∆⇒ A⊕B

4.12. ⊗R, com C = A⊗B onde ∆ = ∆1,∆2


65

π1

...Γ⇒ D

π2

...∆1 ⇒ A

π3

...∆2, D ⇒ B

⊗R∆, D ⇒ A⊗B

CutΓ,∆⇒ A⊗B

Observe que foi feito uma escolha ao aplicar ⊗R, porém o caso em que temos

∆1, D na derivação π2 é similar.

Permutando o corte, temos uma derivação com altura de corte n+ k

π1

...Γ⇒ D

π3

...∆2, D ⇒ B

Cut∆2,Γ⇒ B

π2

...∆1 ⇒ A

⊗RΓ,∆⇒ A⊗B

4.13. (R, com C = A( B


π1

...Γ⇒ D

π2

...∆, D,A⇒ B

(R

∆, D ⇒ A( BCut

Γ,∆⇒ A( B


π1

...Γ⇒ D

π2

...∆, A,D ⇒ B

CutΓ,∆, A⇒ B

(R

Γ,∆⇒ A( B

4.14. !R, com C =!A

Temos a derivação

π1

...Γ⇒!D

π2

...!D, !∆⇒ A

!R!D, !∆⇒!A

CutΓ, !∆⇒!A



• !D não é principal à esquerda


66

• !D é principal à esquerda


...!Γ⇒ D

!R!Γ⇒!D

π2

...!D, !∆⇒ A

!R!D, !∆⇒!A

Cut!Γ, !∆⇒!A


π1

...!Γ⇒ D

!R!Γ⇒!D

π2

...!D, !∆⇒ A

Cut!Γ, !∆⇒ A

!R!Γ, !∆⇒!A

4.15. ?R, com C =?A


π1

...Γ⇒ D

π2

...∆, D ⇒ A

?R∆, D ⇒?A

CutΓ,∆⇒?A


π1

...Γ⇒ D

π2

...∆, D ⇒ A

CutΓ,∆⇒ A

?RΓ,∆⇒?A

4.16. C = 1

Temos que C = 1. Nesse caso, temos a derivação

Γ,∆⇒ D D ⇒ 1Cut

Γ,∆⇒ 1

Para a prova terminar, D deve ser vazio. Mas como D é a fórmula de corte, ela

não pode ser vazia. Não existe o caso no qual, na premissa direita, aplicamos

a regra 1R imediatamente depois de cut.

4.17. ∀R, com C = ∀xA


67

π1

...Γ⇒ D

π2

...∆, D ⇒ A(y/x)

∀R∆, D ⇒ ∀xA

CutΓ,∆⇒ ∀xA

Permutando o corte e pelo lema da α-conversão, temos uma derivação com

altura de corte n+m

π1

...Γ⇒ D

π2′

...∆, D ⇒ A(z/x)

CutΓ,∆⇒ A(z/x)

∀RΓ,∆⇒ ∀xA

Como y pode estar livre em Γ, podemos substituí-lo por z assumindo que z

não ocorre livre em D, ∆ e Γ.

4.18. C = ∃xA


π1

...Γ⇒ D

π2

...∆, D ⇒ A(t/x)

∃R∆, D ⇒ ∃xA

CutΓ,∆⇒ ∃xA


π1

...Γ⇒ D

π2

...∆, D ⇒ A(t/x)

CutΓ,∆⇒ A(t/x)

∃RΓ,∆⇒ ∃xA


5.1. D = A&B

A derivação com um peso de corte w(A&B) é

π1

...Γ⇒ A

π2

...Γ⇒ B

&RΓ⇒ A&B

π3

...∆, A⇒ C

&L∆, A&B ⇒ C

CutΓ,∆⇒ C

68

Neste caso, selecionamosA na premissa direita. O caso selecionandoB é similar.

Temos então a derivação com um peso de corte menor w(A)

π1

...Γ⇒ A

π3

...A,∆⇒ C

CutΓ,∆⇒ C

5.2. D = A⊕B

A derivação com um peso de corte w(A⊕B) é

π1

...Γ⇒ A ⊕R

Γ⇒ A⊕B

π2

...∆, A⇒ C

π3

...∆, B ⇒ C

⊕L∆, A⊕B ⇒ C

CutΓ,∆⇒ C

Neste caso, selecionamos A na premissa esquerda. O caso selecionando B é

similar. Temos então a derivação com um peso de corte menor w(A)

π1

...Γ⇒ A

π2

...A,∆⇒ C

CutΓ,∆⇒ C

5.3. D = A⊗B onde Γ = Γ1,Γ2

A derivação com um peso de corte w(A⊗B) é

π1

...Γ1 ⇒ A

π2

...Γ2 ⇒ B

⊗RΓ1,Γ2 ⇒ A⊗B

π3

...∆, A,B ⇒ C

⊗L∆, A⊗B ⇒ C

CutΓ,∆⇒ C

Temos então duas derivações com um peso de corte menor w(A) e w(B)

π1

...Γ1 ⇒ A

π2

...Γ2 ⇒ B

π3

...∆, A,B ⇒ C

Cut∆,Γ2, A⇒ C

CutΓ,∆⇒ C

5.4. D = A( B onde ∆ = ∆1,∆2

A derivação com um peso de corte w(A( B) é

69

π1

...Γ, A⇒ B

(R

Γ⇒ A( B

π2

...∆1 ⇒ A

π3

...∆2, B ⇒ C

(L

∆, A( B ⇒ CCut

Γ,∆⇒ C

Temos então duas derivações com um peso de corte menor w(A) e w(B)

π2

...∆1 ⇒ A

π1

...Γ, A⇒ B

π3

...∆2, B ⇒ C

CutΓ,∆2, A⇒ C

CutΓ,∆⇒ C

5.5. D =!A

Neste caso, é possível aplicar três regras distintas quando temos !D: dereliction,

contração e enfraquecimento

• Dereliction

A derivação com um peso de corte w(!A) éπ1

...!Γ⇒ A

!R!Γ⇒!A

π2

...∆, A⇒ C

!L∆, !A⇒ C

Cut!Γ,∆⇒ C


π1

...!Γ⇒ A

π2

...A,∆⇒ C

Cut!Γ,∆⇒ C

• Enfraquecimento


...!Γ⇒ A

!R!Γ⇒!A

π2

...∆⇒ C

W!A,∆⇒ C

Cut!Γ,∆⇒ C

Podemos então encontrar uma derivação sem corteπ2

...∆⇒ C

W!Γ,∆⇒ C

• Contração

Para o caso de contração podemos tentar permutar o corte. A derivação

com uma altura de corte n+ 1 +m+ 1

70

π1

...!Γ⇒ A !R!Γ⇒!A

π2

...!A, !A,∆⇒ C

C!A,∆⇒ C

Cut!Γ,∆⇒ C

se torna a derivação com alturas de corte n + 1 + max(n + 1,m) + 1 e

n+ 1 +m

π1

...!Γ⇒ A

!R!Γ⇒!A

π1

...!Γ⇒ A

!R!Γ⇒!A

π2

...!A, !A,∆⇒ C

Cut!A, !Γ,∆⇒ C

Cut!Γ, !Γ,∆⇒ C

C!Γ,∆⇒ C

Ou seja, a permutação aumentou a altura do primeiro corte. Nesse caso,

a solução é utilizar a regra de multicut. Podemos transformar a derivação

com uma altura de corte n+ 1 +m+ 1

π1

...!Γ⇒ A !R!Γ⇒!A

π2

...!A, !A,∆⇒ C

C!A,∆⇒ C

Cut!Γ,∆⇒ C

na derivação com uma altura de corte n+ 1 +m, onde r = 2π1

...!Γ⇒ A

!R!Γ⇒!A

π2

...∆, !A, !A⇒ C

Cut!!Γ,∆⇒ C

5.6. D =?A

A derivação com um peso de corte w(?A) é

π1

...Γ⇒ A

?RΓ⇒?A

π2

...!∆, A⇒?C

?L!∆, ?A⇒?C

CutΓ, !∆⇒?C


π1

...Γ⇒ A

π2

...!∆, A⇒?C

CutΓ, !∆⇒?C

5.7. D = 1

Temos a derivação

71

1R⇒ 1

π1

...Γ,∆⇒ C

1LΓ,∆, 1⇒ C

CutΓ,∆⇒ C

E a derivação sem corte é

π1

...Γ,∆⇒ C

5.8. D = ∀xA

A derivação com uma altura de corte n+ 1 +m+ 1 é

π1

...Γ⇒ A(y/x)

∀RΓ⇒ ∀xA

π2

...∆, A(t/x)⇒ C

∀L∆,∀xA⇒ C

CutΓ,∆⇒ C

Pelo lema da substituição, temos então uma derivação com altura de corte

n+m

π1[t/y]

...Γ⇒ A(t/x)

π2

...∆, A(t/x)⇒ C

CutΓ,∆⇒ C

5.9. D = ∃xA


π1

...Γ⇒ A(t/x)

∃RΓ⇒ ∃xA

π2

...∆, A(y/x)⇒ C

∃L∆,∃xA⇒ C

CutΓ,∆⇒ C

Pelo lema da substituição, temos então uma derivação com altura de corte

n+m

π1

...Γ⇒ A(t/x)

π2[t/y]

...∆, A(t/x)⇒ C

CutΓ,∆⇒ C

QED.

72

4 Lógica Linear comSubexponenciais (SELL)

Nós podemos mostrar que os conectivos (com exceção dos exponenciais) dos capítulos

anteriores são canônicos, isto é, se existem dois conectivos diferentes para a mesma regra,

eles são iguais. Suponha que tenhamos duas conjunções diferentes (∧a e ∧b) para as regras

clássicas do cálculo de sequentes: (NIGAM; PIMENTEL; REIS, 2011)

Γ, A,B ⇒ ∆∧aL

Γ, A ∧a B ⇒ ∆Γ⇒ ∆, A Γ⇒ ∆, B

∧aRΓ⇒ ∆, A ∧a B

Γ, A,B ⇒ ∆∧bL

Γ, A ∧b B ⇒ ∆

Γ⇒ ∆, A Γ⇒ ∆, B∧bR

Γ⇒ ∆, A ∧b B

É fácil mostrar que, para quaisquer fórmulas A e B, A ∧a B ≡ A ∧b B:

A,B ⇒ A∧aL

A ∧a B ⇒ AA,B ⇒ B

∧aLA ∧a B ⇒ B ∧bR

A ∧a B ⇒ A ∧b B

Isso significa que todos os símbolos para a conjunção clássica pertencem à mesma

classe de equivalência. Dessa forma, qualquer conectivo que escolhamos usar (∧a,∧b,∧c, ...)não irá interferir na derivabilidade do sequente.

O mesmo não vale para os conectivos exponenciais da Lógica Linear. Suponha que

temos !a, !b e ?a, ?b com as regras da Lógica Linear Intuicionista:

!a Γ ⇒ A!aR

!a Γ ⇒ !aA!aΓ, A ⇒ ?aB

?aL!aΓ, ?aA ⇒ ?aB

!b Γ ⇒ A!bR

!b Γ ⇒ !bA

!bΓ, A ⇒ ?bB?bL

!bΓ, ?bA ⇒ ?bB

Γ, A ⇒ B!aL

Γ, !aA ⇒ BΓ ⇒ A

?aRΓ ⇒ ?aA

73

Γ, A ⇒ B!bL

Γ, !bA ⇒ B

Γ ⇒ A?bR

Γ ⇒ ?bA

Em geral, não é possível mostrar as equivalências !aA ≡!bA e ?aA ≡?bA:

?...

!a,bR!aA⇒!bA

?...

A⇒!bA!aL

!aA⇒!bA

?...

?a,bL?aA⇒?bA

?...

?aA⇒ A?bD

?aA⇒?bA

No sequente A⇒!bA, em geral, não podemos introduzir !. Por exemplo, seja A = >

?...

> ⇒!b>A⇒!bA

Nesse sentido, podemos definir uma classe de exponenciais, que chamaremos de subex-

ponenciais. A Lógica Linear com Subexponenciais (SELL1) é um refinamento da Lógica

Linear, onde adicionamos os novos operadores subexponenciais !i,?i e o índice i indica a

classe do exponencial.

Formalmente, o sistema SELL foi apresentado por Vincent Danos (DANOS; JOINET;

SCHELLINX, 1993). Vivek Nigam (NIGAM; MILLER, 2009) apresentou um sistema onde os

subexponenciais têm uma estrutura de pré-ordem para garantir a eliminação do corte.

Posteriormente, apresentou-se o sistema SELLe (NIGAM; OLARTE; PIMENTEL, 2013) (sis-

tema SELL com quantificadores) e o sistema SELLS2 (OLARTE; PIMENTEL; NIGAM, 2015).

SELLS, diferente de SELL, possui uma estrutura de ×-poset.

4.1 Sintaxe

SELL possui as mesmas regras da Lógica Linear, exceto as regras dos exponenciais.

Enquanto a Lógica Linear possui apenas os exponenciais ! e ?, SELL possui quantos1A abreviatura vem do inglês “Linear Logic with Subexponential”.2A abreviatura SELLS vem do inglês “Linear Logic with Soft Subexponential”.

74

exponenciais se queira. Assim, substituiremos os exponenciais da Lógica Linear por um

conjunto (finito ou não) de exponenciais rotulados chamados subexponenciais (OLARTE;

PIMENTEL; NIGAM, 2015).

Definimos a linguagem de SELL no sistema intuicionista através da notação BNF:

Definição 4.1 (Sintaxe do sistema SELL intuicionista).

F ::= p | F ⊗ F | F ⊕ F | F&F | F ( F | 1 | 0 | > |!iF |?iF | ∃x.F | ∀x.F

onde p é um átomo e F é uma fórmula.

Dessa forma, os subexponenciais são a divisão de ! e ? em classes diferentes. Cada

subexponencial é caracterizado pelo seu índice i e o conjunto de fórmulas definido por

esse índice é chamado de location. Os índices possuem uma ordem que será definida mais

à frente, onde a ordem dos subexponenciais define em quais fórmulas aplicaremos as regras

!i e ?i.

Através dessa sintaxe, cada sistema é especificado por uma assinatura exponencial

Σ = (A,�, U) onde A é o conjunto de índices, � é a relação de ordem entre esses índices

e U é o conjunto dos índices que podem sofrer enfraquecimento e contração.

Além disso, iremos provar que a Eliminação do Corte também é válida para SELLS.

Uma estrutura de pré-ordem é suficiente para provar a Eliminação do Corte, porém, em

aplicações mais interessantes, utilizamos um ×-poset. Os quantificadores em SELLS são

consideravelmente mais expressivos do que em SELL. Veremos adiante que SELLe permite

somente a quantificação de subexponenciais que estão no ideal de um único subexponen-

cial, enquanto SELLSe permite a quantificação de subexponenciais que estão no ideal de

qualquer subexponencial de um dado conjunto não vazio de subexponenciais.

4.2 Estrutura Algébrica dos Subexponenciais

Definição 4.2 (Conjuntos Parcialmente Ordenados). Um conjunto parcialmente orde-

nado (poset) 3 é representado pelo par (D,v), onde D é um conjunto e v é uma relação

binária sobre D, tal que

• v é reflexiva: ∀d ∈ D, d v d;3A abreviatura “poset” vem do inglês “partially ordered set”

75

• v é antisimétrica: ∀d1, d2 ∈ D, se d1 v d2 e d2 v d1, então d1 = d2;

• v é transitiva: ∀d1, d2, d3 ∈ D, se d1 v d2 e d2 v d3, então d1 v d3.

Observação 4.1. Se, ∀d1, d2 ∈ D, ou d1 v d2 ou d2 v d1 ocorre, então dizemos que

(D,v) é um conjunto totalmente ordenado.

Definição 4.3 (Menor Limite Superior e Maior Limite Inferior). Seja (D,v) um conjunto

parcialmente ordenado, e seja X ⊆ D.

• ∀x ∈ X, d ∈ D é um limite superior de X se somente se x v d.

• d ∈ D é o menor limite superior de X (notação tX) se somente se d é um limite

superior de X e d v d′, para todo limite superior d′ ∈ D.4

• ∀x ∈ X, d ∈ D é um limite inferior de X se somente se d v x.

• d ∈ D é o maior limite inferior de X (notação uX) se somente se d é um limite

inferior de X e d′ v d, para todo limite inferior d′ ∈ D.5

Definição 4.4 (Reticulado Completo). Um conjunto parcialmente ordenado (D,v) é um

reticulado completo se somente se tX e uX existem ∀X ⊆ D

Observação 4.2. Um reticulado completo (D,v) possui um menor elemento ⊥ = uD e

um maior elemento > = tD.

Definição 4.5 (×-poset). Um ×-poset é representado pela tripla (D,v,×), onde essa

tripla representa um conjunto parcialmente ordenado unido com a operação binária ×(chamada produto), tal que:

• × é associativa: ∀d1, d2, d3 ∈ D, (d1 × d2)× d3 = d1 × (d2 × d3);

• × é comutativa: ∀d1, d2 ∈ D, d1 × d2 = d2 × d1;

• > é o elemento neutro de ×: ∀d ∈ D, d×> = d;

• × é monótona: ∀d1, d2, d3, d4 ∈ D, se d1 v d4 e d2 v d1 × d3, então d2 v d4 × d3;

• × é intensiva: ∀d1, d2 ∈ D, d1 × d2 v d1.

• ⊥ é o elemento nulo de ×: ∀d ∈ D, d×⊥ = ⊥4Abreviaremos “menor limite superior” como “lub”, do inglês “least upper bound”.5Abreviaremos “maior limite inferior” como “glb”, do inglês “greatest lower bound”.

76

Observação 4.3. Se, ∀d1, d2 ∈ D, glb(d1, d2) existe e d1 × d2 = glb(d1, d2), então o

×-poset é chamado idempotente.

Exemplo 4.1. Todo reticulado distributivo limitado (L,∨,∧, 0, 1) é um ×-poset idempo-

tente, onde d1 v d2 se e somente se d1 ∨ d2 = d2 e × = ∧.

Se d1 v d4, então d1 ∨ d4 = d4. Assim, d4 ∧ d3 = (d1 ∨ d4)∧ d3 = (d1 ∧ d3)∨ (d4 ∧ d3).

Logo, d1 ∧ d3 v d4 ∧ d3.

Temos que d2 ∨ 1 = 1 e d1 ∧ 1 = d1. Assim, d1 = d1 ∧ (d2 ∨ 1) = (d1 ∧ d2)∨ (d1 ∧ 1) =

(d1 ∧ d2) ∨ d1. Logo, d1 ∧ d2 v d1.

Exemplo 4.2 (C-semiring). Um c-semiring é uma tupla (A,+,×,⊥,>) que satisfaz as

seguintes condições:

(i) A é um conjunto e ⊥,> ∈ A;

(ii) + é um operador binário, comutativo, associativo e idempotente em A, onde ⊥ é

seu elemento neutro e > é seu elemento nulo;

(iii) × é um operador binário, associativo e comutativo em A, onde > é seu elemento

neutro e ⊥ é seu elemento nulo. Além disso, × é distributivo sobre +.

Seja v definido como a1 v a2 se e somente se a1 + a2 = a2. Assim, (A,v) é um

reticulado completo onde

(iv) + e × são monótonas em v;

(v) × é intensiva em v;

(vi) ⊥ (respectivamente, >) é o menor elemento (respectivamente, o maior elemento) de

A;

(vii) + é o operador lub.

Se × é idempotente, então

(viii) + é distributivo sobre ×;

(ix) (A,v) é um reticulado distributivo completo e × é seu glb. Um c-semiring é idem-

potente se seu operador × é idempotente. De outra maneira, o c-semiring é não-

idempotente.

77

Assim, (A,v,×) é um ×-poset e, se × é idempotente, (A,v,×) é um ×-poset idem-

potente.

Exemplo 4.3. Seja (D,v) um poset limitado e defina × como d1 × d2 = (↓ d1) ∩ (↓ d2)

onde ↓ d1 está no ideal de d1, isto é, ↓ d1 = {x ∈ D | x v d1}. Observe que a interseção de

ideais é um ideal e é não vazia pois ∀d1 ∈ D,⊥ ∈ (↓ d1). Além disso, d1 v d2 se e somente

se (↓ d1) ⊆ (↓ d2). Assim, a monotonicidade e a intensividade se mantém trivialmente e

(D,v,×) é um ×-poset.

4.3 Sistema SELLSΣ

A Lógica Linear com Subexponenciais (SELLSΣ) é especificada por uma assinatura

exponencial Σ = (A,�,×Σ, U), tal que

• A é um conjunto de rótulos;

• (A,�,×Σ) é um ×-poset que possui o produto ×Σ;

• (A,�,×Σ) possui um mínimo e um máximo (⊥,> ∈ A);

• U ⊆ A especifica quais subexponenciais permitem tanto o enfraquecimento quanto

a contração;

• � é ascendentemente fechado em relação a U : se a1 ∈ U e a1 � a2, então a2 ∈ U .

Dada uma assinatura exponencial, o sistema SELLSΣ é um sistema obtido pela subs-

tituição do exponencial ! da Lógica Linear pelo subexponencial !a, ∀a ∈ A, tal que as

regras da Lógica Linear permanecem válidas e adicionamos as seguintes regras:

Sistema SELLSΣ

• ∀a ∈ A (regras de dereliction e promotion)

Γ, F ⇒ G!aL

Γ, !aF ⇒ G

!a1F1,..., !anFn ⇒ F!aR

!a1F1,..., !anFn ⇒ !aF

tal que a � a1 ×Σ ...×Σ an.

Γ ⇒ G?aR

Γ ⇒ ?aG!a1F1,..., !anFn, F ⇒ ?an+1G

?aL!a1F1,..., !anFn, ?aF ⇒ ?an+1G

78

tal que a � a1 ×Σ ...×Σ an+1

• ∀u ∈ U (regras estruturais)

Γ ⇒ GW

Γ, !uF ⇒ GΓ, !uF , !uF ⇒ G

CΓ, !uF ⇒ G

Teorema 4.1. A regra F ⇒ F é admissível, onde F é uma fórmula.

Demonstração.

A prova procede por indução no peso de F . Primeiramente, vamos demonstrar os

casos bases onde w(F ) = 0

(i) F = 1

1R⇒ 11L

1⇒ 1

(ii) F = 0

0L0⇒ 0

(iii) F = >

>R> ⇒ >

Por hipótese indutiva, os sequentes A ⇒ A e B ⇒ B são demonstráveis. Temos

então os casos indutivos:

(iv) F = A&B

A⇒ A&L

A&B ⇒ AB ⇒ B

&LA&B ⇒ B

&RA&B ⇒ A&B

(v) F = A⊗B

A⇒ A B ⇒ B ⊗RA,B ⇒ A⊗B

⊗LA⊗B ⇒ A⊗B

(vi) F = A⊕B

79

A⇒ A ⊕RA⇒ A⊕B

B ⇒ B ⊕RB ⇒ A⊕B ⊕L

A⊕B ⇒ A⊕B

(vii) F = A( B

A⇒ A B ⇒ B (L

A( B,A⇒ B(R

A( B ⇒ A( B

(viii) F =!aA

A⇒ A!aL

!aA⇒ A!aR

!aA⇒!aA

(ix) F =?aA

A⇒ A?aR

A⇒?aA?aL

?aA⇒?aA

QED.

Teorema 4.2. Se o sequente Γ ⇒!aF é demonstrável em SELLSΣ, então o sequente

Γ⇒!bF , ∀b � a, também é demonstrável.

Demonstração. Suponha que temos uma prova de Γ ⇒!aF . Vamos tentar provar o

sequente Γ⇒!bF

Γ⇒!aF

F ⇒ F!aL

!aF ⇒ F!bR

!aF ⇒!bF CutΓ⇒!bF

onde Γ⇒!aF possui uma prova por hipótese e F ⇒ F é admissível pelo teorema 4.1.

QED.

Lema 4.1. A regra Cut!

Γ⇒!aF ∆, (!aF )r ⇒ CCut! (r > 1)

Γ,∆⇒ C

é admissível em SELLSΣ, onde (!aF )r (r > 1) significa r cópias de !aF e a ∈ U .

80

Demonstração. A prova da eliminação de Cut! em SELLSΣ é similar à prova de eli-

minação do corte em SELLSΣ. Assim como na eliminação do corte, a prova de Cut!

procede por indução na ordem lexicográfica do par ordenado (W,H), e os casos indutivos

se subdividem em vários casos. A grande maioria dos casos é similar a prova do corte que

mostraremos a seguir, mas alguns casos são mais interessantes. Considere, por exemplo,

o caso em que a fórmula de corte é principal à esquerda e temos que C =!bG.

Temos a derivação com altura de Cut! igual a n+ 1 +m+ 1

π1

...!a1Γ1, ..., !

anΓn ⇒ F!aR

!a1Γ1, ..., !anΓn ⇒!aF

π2

...!b1∆1, ..., !

bn∆n, (!aF )r ⇒ G

!bR!b1∆1, ..., !

bn∆n, (!aF )r ⇒!bG

Cut!a1Γ1, ..., !

anΓn, !b1∆1, ..., !

bn∆n ⇒!bG

onde

Γ =!a1Γ1, ..., !anΓn

∆ =!b1∆1, ..., !bn∆n

a � a1 ×Σ ...×Σ an

b � b1 ×Σ ...×Σ bn ×Σ a×Σ ...×Σ a︸︷︷︸r vezes

Transformamos então em uma derivação com altura de Cut! igual a n+ 1 +m

π1

...!a1Γ1, ..., !

anΓn ⇒ F!aR

!a1Γ1, ..., !anΓn ⇒!aF

π2

...!b1∆1, ..., !

bn∆n, (!aF )r ⇒ G

Cut!a1Γ1, ..., !

anΓn, !b1∆1, ..., !

bn∆n ⇒ G!bR

!a1Γ1, ..., !anΓn, !

b1∆1, ..., !bn∆n ⇒!bG

onde b � a1 ×Σ ...×Σ an ×Σ b1 ×Σ ...×Σ bn é válido por monotonicidade.

QED.

Teorema 4.3 (Eliminação do corte em SELLSΣ). A regra de corte


Γ,∆⇒ C

é admissível em SELLSΣ.

81

Demonstração. A prova procede por indução na ordem lexicográfica do par ordenado

(W,H), de mesma forma que no teorema 3.1. Para provar a eliminação do corte em

SELLSΣ, devemos reduzir a ordem lexicográfica do par ordenado (W,H) nas regras dos

exponenciais. Estes correspondem aos casos 3.5, 3.6, 4.5, 4.6, 4.14, 4.15, 5.5, 5.6 do capítulo

3. Os casos bases são os mesmos da Lógica Linear mostrados no capítulo anterior.

3.5. !L, com Γ =!aF,Γ′


dereliction, contração e enfraquecimento.

• Dereliction


...F,Γ′ ⇒ D

!aL

!aF,Γ′ ⇒ D

π2

...∆, D ⇒ C

Cut!aF,Γ′,∆⇒ C

Permutando o corte, temos uma derivação com altura de corte n+mπ1

...F,Γ′ ⇒ D

π2

...∆, D ⇒ C

CutF,Γ′,∆⇒ C

!aL

!aF,Γ′,∆⇒ C• Contração


...!aF, !aF,Γ′ ⇒ D

C!aF,Γ′ ⇒ D

π2

...∆, D ⇒ C



...!aF, !aF,Γ′ ⇒ D

π2

...∆, D ⇒ C

Cut!aF, !aF,Γ′,∆⇒ C

C!aF,Γ′,∆⇒ C

• Enfraquecimento


...Γ′ ⇒ D

W!aF,Γ′ ⇒ D

π2

...∆, D ⇒ C


82


π1

...Γ′ ⇒ D

π2

...∆, D ⇒ C

CutΓ′,∆⇒ C

W!aF,Γ′,∆⇒ C

3.6. ?L, com Γ =?aF,Γ′

Temos a derivação

π1

...F, !a1Γ′1, ..., !

anΓ′n ⇒?an+1D?aL

?aF, !a1Γ′1, ..., !anΓ′n ⇒?an+1D

π2

...∆, ?an+1D ⇒ C

Cut?aF, !a1Γ′1, ..., !

anΓ′n,∆⇒ C

onde Γ′ =!a1Γ′1, !a2Γ′2, ..., !

anΓ′n e a � a1 ×Σ ...×Σ an+1

Vamos considerar a premissa direita do corte e fazer uma análise dos casos


• ?an+1D não é principal à direita e aplicamos uma L-rule

Esses casos correspondem aos casos 4.1 a 4.8

• ?an+1D não é principal à direita e aplicamos uma R-rule


• ?an+1D é principal à direita


π1

...!a1Γ′1, ..., !

anΓ′n, F ⇒?an+1D?aL

!a1Γ′1, ..., !anΓ′n, ?

aF ⇒?an+1D

π2

...!b1∆1, ..., !

bn∆n, D ⇒?bn+1C?an+1

L

!b1∆1, ..., !bn∆n, ?

an+1D ⇒?bn+1CCut

!a1Γ′1, ..., !anΓ′n, ?

aF, !b1∆1, ..., !bn∆n ⇒?bn+1C

onde a � a1 ×Σ ...×Σ an+1 e an+1 � b1 ×Σ ...×Σ bn+1

Permutando o corte, temos uma derivação com altura de corte n+m+ 1

π1

...!a1Γ′1, ..., !

anΓ′n, F ⇒?an+1D

π2

...!b1∆1, ..., !

bn∆n, D ⇒?bn+1C?an+1

L!b1∆1, ..., !

bn∆n, ?an+1D ⇒?bn+1C

Cut!a1Γ′1, ..., !

anΓ′n, F, !b1∆1, ..., !

bn∆n ⇒?bn+1C?aL

!a1Γ′1, ..., !anΓ′n, ?

aF, !b1∆1, ..., !bn∆n ⇒?bn+1C

onde a � a1×Σ ...×Σan×Σb1×Σ ...×Σbn+1 e an+1 � b1×Σ ...×Σbn+1. Temos

que a � a1 ×Σ ...×Σ an ×Σ b1 ×Σ ...×Σ bn+1 é válido por monotonicidade.

83

4.5. !L, com ∆ =!aF,∆′


dereliction, contração e enfraquecimento.

• Dereliction


π1

...Γ⇒ D

π2

...D,F,∆′ ⇒ C

!aL

D, !aF,∆′ ⇒ CCut

Γ, !aF,∆′ ⇒ CPermutando o corte, temos uma derivação com altura de corte n+m

π1

...Γ⇒ D

π2

...D,F,∆′ ⇒ C

CutΓ, F,∆′ ⇒ C

!aL

Γ, !aF,∆′ ⇒ C• Contração


π1

...Γ⇒ D

π2

...D, !aF, !aF,∆′ ⇒ C

CD, !aF,∆′ ⇒ C

CutΓ, !aF,∆′ ⇒ C


...Γ⇒ D

π2

...D, !aF, !aF,∆′ ⇒ C

CutΓ, !aF, !aF,∆′ ⇒ C

CΓ, !aF,∆′ ⇒ C

• Enfraquecimento


π1

...Γ⇒ D

π2

...D,∆′ ⇒ C

WD, !aF,∆′ ⇒ C

CutΓ, !aF,∆′ ⇒ C


...Γ⇒ D

π2

...D,∆′ ⇒ C

CutΓ,∆′ ⇒ C

WΓ, !aF,∆′ ⇒ C

84

4.6. ?L, com ∆ =?aF,∆′

Temos a derivação

π1

...Γ⇒!bD

π2

...F, !a1∆′1, ..., !

an∆′n, !bD ⇒?an+1C

?aL

?aF, !a1∆′1, ..., !an∆′n, !

bD ⇒?an+1CCut

Γ, ?aF, !a1∆′1, ..., !an∆′n ⇒?an+1C

onde ∆′ =!a1∆′1, ..., !an∆′n e a � a1 ×Σ ...×Σ an+1 ×Σ b


possíveis para a derivação π1

• !bD não é principal à esquerda

Esses correspondem aos casos 3.1 a 3.8

• !bD é principal à esquerda


...!b1Γ1, ..., !

bmΓm ⇒ D!bR

!b1Γ1, ..., !bmΓm ⇒!bD

π2

...F, !a1∆′1, ..., !

an∆′n, !bD ⇒?an+1C

?aL

?aF, !a1∆′1, ..., !an∆′n, !

bD ⇒?an+1CCut

!b1Γ1, ..., !bmΓm, ?

aF, !a1∆′1, ..., !an∆′n ⇒?an+1C

onde b � b1 ×Σ ...×Σ bm e a � a1 ×Σ ...×Σ an+1 ×Σ b


π1

...!b1Γ1, ..., !

bmΓm ⇒ D!bR

!b1Γ1, ..., !bmΓm ⇒!bD

π2

...!a1∆′1, ..., !

an∆′n, !bD,F ⇒?an+1C

Cut!b1Γ1, ..., !

bmΓm, F, !a1∆′1, ..., !

an∆′n ⇒?an+1C?aL

!b1Γ1, ..., !bmΓm, ?

aF, !a1∆′1, ..., !an∆′n ⇒?an+1C

onde a � b1×Σ ...×Σ bm×Σ a1×Σ ...×Σ an+1 é válido por monotonicidade.

4.14. !R, com C =!aF

Temos a derivação

π1

...Γ⇒!bD

π2

...!b1∆1, ..., !

bn∆n, !bD ⇒ F

!aR

!b1∆1, ..., !bn∆n, !

bD ⇒!aFCut

Γ, !b1∆1, ..., !bn∆n ⇒!aF

85

onde a � b1 ×Σ ...×Σ bn ×Σ b


possíveis para a derivação π1

• !bD não é principal à esquerda


• !bD é principal à esquerda


...!a1Γ1, ..., !

amΓm ⇒ D!bR

!a1Γ1, ..., !amΓm ⇒!bD

π2

...!b1∆1, ..., !

bn∆n, !bD ⇒ F

!aR

!b1∆1, ..., !bn∆n, !

bD ⇒!aFCut

!a1Γ1, ..., !amΓm, !

b1∆1, ..., !bn∆n ⇒!aF

onde b � a1 ×Σ ...×Σ am e a � b1 ×Σ ...×Σ bn ×Σ b


π1

...!a1Γ1, ..., !

amΓm ⇒ D!bR

!a1Γ1, ..., !amΓm ⇒!bD

π2

...!b1∆1, ..., !

bn∆n, !bD ⇒ F

Cut!a1Γ1, ..., !

amΓm, !b1∆1, ..., !

bn∆n ⇒ F!aR

!a1Γ1, ..., !amΓm, !

b1∆1, ..., !bn∆n ⇒!aF

onde a � a1 ×Σ ...×Σ am ×Σ b1 ×Σ ...×Σ bn é válido por monotonicidade.

4.15. ?R, com C =?aF


π1

...Γ⇒ D

π2

...∆, D ⇒ F

?aR∆, D ⇒?aF

CutΓ,∆⇒?aF


π1

...Γ⇒ D

π2

...∆, D ⇒ F

CutΓ,∆⇒ F

?aRΓ,∆⇒?aF

Consideramos agora os casos em que a fórmula de corte é principal em ambas as

premissas:

86

5.5. D =!aF

Neste caso, é possível aplicar três regras distintas quando temos !D: dereliction,

contração e enfraquecimento

• Dereliction

A derivação com um peso de corte w(!aF ) éπ1

...!a1Γ1, ..., !

amΓm ⇒ F!aR

!a1Γ1, ..., !amΓm ⇒!aF

π2

...∆, F ⇒ C

!aL∆, !aF ⇒ C

Cut!a1Γ1, ..., !

amΓm,∆⇒ C

onde a � a1 ×Σ ...×Σ am

Temos então a derivação com um peso de corte menor w(F )

π1

...!a1Γ1, ..., !

amΓm ⇒ F

π2

...F,∆⇒ C

Cut!a1Γ1, ..., !

amΓm,∆⇒ C

• Enfraquecimento


...!a1Γ1, ..., !

amΓm ⇒ F!aR

!a1Γ1, ..., !amΓm ⇒!aF

π2

...∆⇒ C

W!aF,∆⇒ C

Cut!a1Γ1, ..., !

amΓm,∆⇒ C


Podemos então encontrar uma derivação sem corteπ2

...∆⇒ C

W!a1Γ1, ..., !

amΓm,∆⇒ C

Note que podemos aplicar enfraquecimento em !a1Γ1, ..., !amΓm. Temos que

a ∈ U e a � a1 ×Σ ... ×Σ am, então ∀i, ai ∈ U , pois � é ascendentemente

fechado em relação a U: se a1 ∈ U e a1 � a2, então a2 ∈ U , logo a1 ×Σ

... ×Σ am ∈ U . Como ×Σ é intensiva, temos que a � a1, a � a2, ..., a �am, logo a1 ∈ U, a2 ∈ U, ..., am ∈ U . Dessa forma, podemos aplicar o

enfraquecimento em Γ1, ...,Γm.

• Contração

Para o caso de contração iremos usar a regra Cut!. Temos a derivação com

uma altura de corte n+ 1 +m+ 1

87

π1

...!a1Γ1, ..., !

amΓm ⇒ F!aR

!a1Γ1, ..., !amΓm ⇒!aF

π2

...!aF, !aF,∆⇒ C

C!aF,∆⇒ C

Cut!a1Γ1, ..., !

amΓm,∆⇒ C


Utilizando a regra Cut!, temos uma derivação com altura de corte n+1+m

π1

...!a1Γ1, ..., !

amΓm ⇒ F!aR

!a1Γ1, ..., !amΓm ⇒!aF

π2

...!aF, !aF,∆⇒ C

Cut!a1Γ1, ..., !

amΓm,∆⇒ C


5.6. D =?aF

A derivação com um peso de corte w(?aF ) é

π1

...Γ⇒ F

?aRΓ⇒?aF

π2

...!b1∆1, ..., !

bn∆n, F ⇒?bn+1C?aL

!b1∆1, ..., !bn∆n, ?

aF ⇒?bn+1CCut

Γ, !b1∆1, ..., !bn∆n ⇒?bn+1C

onde a � b1 ×Σ ...×Σ bn+1

Temos então a derivação com um peso de corte menor w(F )

π1

...Γ⇒ F

π2

...!b1∆1, ..., !

bn∆n, F ⇒?bn+1CCut

Γ, !b1∆1, ..., !bn∆n ⇒?bn+1C

QED.

4.4 Sistema SELLSe

A assinatura exponencial de SELLSe é a mesma de SELLSΣ com algumas modifica-

ções: SELLSe possui variáveis subexponenciais. As variáveis exponenciais serão introdu-

zidas através dos quantificadores subexponenciais. Definimos a linguagem de SELLSe no

sistema clássico através da notação BNF:

Definição 4.6 (Sintaxe do sistema SELLSe intuicionista).

88

F ::= p | F ⊗ F | F ⊕ F | F&F | F ( F | 1 | 0 | > |!sF |?sF | ∃x.F | ∀x.F | el : τ.F |dl : τ.F

onde p é um átomo e F é uma fórmula.

Os operadores e e d são quantificadores que atuam nos índices dos exponenciais

(e não em variáveis). São utilizados para criar novos exponenciais de uma mesma classe.

Existem três tipos de tipagem nos quantificadores: uma para as constantes subexponen-

ciais e duas para as variáveis exponenciais. Assim, em SELLSe temos uma assinatura

(A,�, U), tal que:

• Os elementos de A, isto é, a, a1, a2, ... são chamados de constantes subexponenciais;

• s, s1, s2, ... e d, d1, d2, ... representam tanto as variáveis subexponenciais quanto as

constantes subexponenciais;

• i ∈ {b, u} indica se o subexponencial é limitado ou não-limitado6;

• l, l1, l2, ... são variáveis subexponenciais: l /∈ A;

l : {s1, ..., sn}il : {s1/s2}i

onde n ≥ 1 e s1 ≺ s2;

A tipagem l : {s1, ..., sn}i especifica que ⊥ ≺ l e o subexponencial l está no ideal de

todos os subexponenciais {s1, ..., sn}, isto é, l � sj para todo 1 ≤ j ≤ n.

A tipagem l : {s1/s2}i especifica que s2 � l � s1. Observe que se ambos s1 e s2

são não-limitados (respectivamente, limitados), então l também será, assim i = u

(respectivamente, i = b);

• a é uma constante subexponencial: a ∈ A

a : {a}i

onde a está no seu próprio ideal. Temos que i = u se a ∈ U e i = b caso contrário;

• τ especifica qualquer uma das três tipagens: a, s, d, l.

Os sequentes em SELLSe tem a forma S; Γ⇒ G, onde6b e u vem do inglês “bounded” (limitado) e “unbounded” (não-limitado)

89

• S = AΣ ∪ {l1 : τ, ..., ln : τ};

• {l1, ..., ln} é um conjunto de variáveis subexponenciais distintas;

• AΣ = {a : {a}i | a ∈ A}.

Seja S = {l | (l : τ) ∈ S}. A relação de pré-ordem �S é definida em S como um

conjunto fechado sobre as propriedades transitiva e reflexiva:7

� ∪{(l,>), (⊥, l) | l ∈ S}

∪{(l, s) | (l : {s1, ..., sn}); (s : τ) ∈ S; (sj, s) para todo 1 ≤ j ≤ n}

∪{(l, s1), (s2, l) | (l : {s1/s2}) ∈ S}

onde ⊥ e > são, respectivamente, os elementos mínimo e máximo em �S.

Note que (l,>), (⊥, l) diz que l é menor que o elemento máximo > e que l é maior

que o elemento mínimo (⊥).

Note (l, s). Como l : {s1, ..., sn} especifica que l � sj e (sj, s) nos diz que sj � s, então

temos que l � s. Da mesma forma, veja (l, s1), (s2, l) e note que l : {s1/s2} especifica que

s2 � l � s1.

Dessa forma, o sistema SELLSe estende o sistema SELLSΣ adicionando as regras dos

quantificadores subexponenciais:

Sistema SELLSe

S; Γ, F [s/l]⇒ GeL1(?1)

S; Γ,el : {s1, ..., sn}i.F ⇒ G

S; Γ, F [s/l]⇒ GeL2(?2)

S; Γ,el : {s1/s2}i.F ⇒ G

S; Γ⇒ G[s/l]dR1(?1)

S; Γ⇒ dl : {s1, ..., sn}i.GS; Γ⇒ G[s/l]

dR2(?2)S; Γ⇒ dl : {s1/s2}i.G

S, le : τ ; Γ, F [le/l]⇒ GdL(?3)

S; Γ,dl : τ.F ⇒ G

S, le : τ ; Γ⇒ G[le/l]eR(?3)

S; Γ⇒ el : τ.G

onde le é uma variável fresca, isto é, não está presente em S nas regras dL e eR. As

condições (?1), (?2) e (?3) são definidas abaixo:

(?1) s : τ ∈ S é tal que s �S sj para todo 1 ≤ j ≤ n e se i = b então s é limitado,

caso contrário s é não-limitado.7Uma relação parcial de ordem, como já definido anteriormente, é transitiva, reflexiva e anti-simétrica.

Já a relação de pré-ordem é apenas transitiva e reflexiva. Toda ordem parcial também é uma pré-ordem.

90

(?2) s : τ ∈ S é tal que s1 �S s �S s2 e se i = b então s é limitado, caso contrário s é

não-limitado.

(?3) �S′ é uma pré-ordem, ascendentemente fechada com relação ao conjunto US′ ,

onde S ′ = S, le : τ e US′ = {s | (s : {τ}u) ∈ S ′}.

Note que as regras dos quantificadores tem condições diferentes, então s, l e le não são

necessariamente do mesmo tipo. Porém as observações (?1), (?2) e (?3) fazem com que os

tipos sejam compatíveis.

Antes de demonstrar a eliminação do corte em SELLSe, precisaremos do lema da

substituição para o sistema SELLSe.

Lema 4.2 (Lema da Substituição para SELLSe). Assuma que S; Γ ⇒ G é derivável em

SELLSe com altura n e considere os subexponenciais s : τ e l : τ ′ tal que s ∈ S é livre

para l ∈ {Γ, G}. Temos que

(i) Se l : τ ′ é do tipo l : {s1, ..., sn} então s : τ é tal que s ≤ sj para todo 1 ≤ j ≤ n;

(ii) Se l : τ ′ é do tipo l : {s1/s2} então s : τ é tal que s1 ≤ s ≤ s2;

então S; Γ[s/l]⇒ G[s/l] é derivável em SELLSe com altura n.

Demonstração. A demonstração procede por indução na altura da derivação.

Casos bases: o sequente tem altura zero

0L`n S; Γ, 0⇒ G>R`n S; Γ,⇒ >

1R`n⇒ 1

Como o sequente termina com a regra 0L,>R, 1R, então

0L`n S; Γ[s/l], 0⇒ G[s/l]>R`n S; Γ[s/l],⇒ >

1R`n⇒ 1

Casos indutivos: considere, por exemplo, que a última regra aplicada foi ⊕R, onde

G = A⊕B

`n S; Γ⇒ A[s/l]⊕R`n+1 S; Γ⇒ (A⊕B)[s/l]

91

Como s é livre para l ∈ {A⊕B} então s é livre para algum l ∈ A (pois a regra ⊕R não

altera o conjunto de variáveis livres e ligadas). Então, por hipótese indutiva, S; Γ ⇒ G

possui a mesma altura que S; Γ[s/l] ⇒ G[s/l]. O mesmo vale para os demais operadores

⊗,(,&.

Agora, vamos considerar um caso mais interessante. Se S; Γ⇒ G é derivado por eL:

`n S; Γ, F [t/m]⇒ GeL`n+1 S; Γ,em : τ ′.F ⇒ G

Por hipótese indutiva, temos:

`n S; Γ[s/l], F [t/m][s/l]⇒ G[s/l]

Podemos assumir que m 6= s,m 6= l,m 6= t. Então

F [t/m][s/l] = F [s/l][t/m]

Substituindo na hipótese indutiva

`n S; Γ[s/l], F [s/l][t/m]⇒ G[s/l]

Pela regra eL

`n S; Γ[s/l], F [s/l][t/m]⇒ G[s/l]eL

`n+1 S; Γ[s/l],em : τ ′.F [s/l]⇒ G[s/l]

onde `n+1 S; Γ[s/l],em : τ ′.F [s/l]⇒ G[s/l] é o sequente que queríamos provar.

Argumento similar se utiliza nas demais regras de e,d.

Vamos considerar agora que S; Γ⇒ G é derivado por !aR:

`n!a1F1, ..., !amFm ⇒ F

!aR`n+1!a1F1, ..., !amFm ⇒!aF

onde a � a1 ×Σ ...×Σ am.


`n!a1F1[s/l], ..., !amFm[s/l]⇒ F [s/l]

92

Aplicando !aR

`n!a1F1[s/l], ..., !amFm[s/l]⇒ F [s/l]!aR`n+1!a1F1[s/l], ..., !amFm[s/l]⇒!aF [s/l]

onde a[s/l] � a1[s/l]×Σ ...×Σam[s/l] é válido pois, apesar de l : τ ′ e s : τ não serem do

mesmo tipo, as observações (?1), (?2) e (?3) fazem os tipos serem compatíveis. Suponha,

por exemplo, que s : τ e l : {s1, ..., sn}, isto é, l � sj. Então (?1) nos garante que s � sj.

Da mesma forma, suponha que s : τ e l : {s1/s2}, isto é, s1 � l � s2. Então (?2) nos

garante que s1 � s � s2. Argumento similar se utiliza na regra ?aL.

QED.

Teorema 4.4 (Eliminação do corte em SELLSe). A regra de corte

S; Γ⇒ D S; ∆, D ⇒ CS; Γ,∆⇒ C

é admissível em SELLSe.

Demonstração. Para provar a eliminação do corte em SELLSe, devemos utilizar in-

dução na ordem lexicográfica do par ordenado (W,H) nas regras dos quantificadores

exponenciais. Os casos bases são os mesmos da Lógica Linear mostrados no capítulo an-

terior. Continuando a numeração do sistema SELLSΣ, a demonstração será dividida nos

seguintes casos:






3.10. eL1, com Γ = Γ′,el : {s1, ..., sn}i.F


93

π1

...S; Γ′, F [s/l]⇒ D

eL1

S; Γ′,el : {s1, ..., sn}i.F ⇒ D

π2

...S; ∆, D ⇒ C

CutS; Γ′,el : {s1, ..., sn}i.F,∆⇒ C


π1

...S; Γ′, F [s/l]⇒ D

π2

...S; ∆, D ⇒ C

CutS; Γ′, F [s/l],∆⇒ C

eL1

S; Γ′,el : {s1, ..., sn}i.F,∆⇒ C

3.11. eL2, com Γ = Γ′,el : {s1/s2}i.F


π1

...S; Γ′, F [s/l]⇒ D

eL2

S; Γ′,el : {s1/s2}i.F ⇒ D

π2

...S; ∆, D ⇒ C

CutS; Γ′,el : {s1/s2}i.F,∆⇒ C


π1

...S; Γ′, F [s/l]⇒ D

π2

...S; ∆, D ⇒ C

CutS; Γ′, F [s/l],∆⇒ C

eL2

S; Γ′,el : {s1/s2}i.F,∆⇒ C

3.12. dL, com Γ = Γ′,dl : τ.F


π1

...S, le : τ ; Γ′, F [le/l]⇒ D

dL

S; Γ′,dl : τ.F ⇒ D

π2

...S; ∆, D ⇒ C

CutS; Γ′,dl : τ.F,∆⇒ C


π1

...S, le : τ ; Γ′, F [le/l]⇒ D

π2

...S, le : τ ; ∆, D ⇒ C

CutS, le : τ ; Γ′, F [le/l],∆⇒ C

dL

S; Γ′,dl : τ.F,∆⇒ C

94


4.19. eL1, com ∆ = ∆′,el : {s1, ..., sn}i.F


π1

...S; Γ⇒ D

π2

...S;D,∆′, F [s/l]⇒ C

eL1

S;D,∆′,el : {s1, ..., sn}i.F ⇒ CCut

S; Γ,∆′,el : {s1, ..., sn}i.F ⇒ C


π1

...S; Γ⇒ D

π2

...S;D,∆′, F [s/l]⇒ C

CutS; Γ,∆′, F [s/l]⇒ C

eL1

S; Γ,∆′,el : {s1, ..., sn}i.F ⇒ C

4.20. eL2, com ∆ = ∆′,el : {s1/s2}i.F


π1

...S; Γ⇒ D

π2

...S;D,∆′, F [s/l]⇒ C

eL2

S;D,∆′,el : {s1/s2}i.F ⇒ CCut

S; Γ,∆′,el : {s1/s2}i.F ⇒ C


π1

...S; Γ⇒ D

π2

...S;D,∆′, F [s/l]⇒ C

CutS; Γ,∆′, F [s/l]⇒ C

eL2

S; Γ,∆′,el : {s1/s2}i.F ⇒ C

4.21. dL, com ∆ = ∆′,dl : τ.F


π1

...S; Γ⇒ D

π2

...S, le : τ ;D,∆′, F [le/l]⇒ C

dL

S;D,∆′,dl : τ.F ⇒ CCut

S; Γ,∆′,dl : τ.F ⇒ C


95

π1

...S, le : τ ; Γ⇒ D

π2

...S, le : τ ;D,∆′, F [le/l]⇒ C

CutS, le : τ ; Γ,∆′, F [le/l]⇒ C

dL

S; Γ,∆′,dl : τ.F ⇒ C

4.22. dR1, com C = dl : {s1, ..., sn}i.G


π1

...S; Γ⇒ D

π2

...S; ∆, D ⇒ G[s/l]

dR1

S; ∆, D ⇒ dl : {s1, ..., sn}i.GCut

S; Γ,∆⇒ dl : {s1, ..., sn}i.G


π1

...S; Γ⇒ D

π2

...S; ∆, D ⇒ G[s/l]

CutS; Γ,∆⇒ G[s/l]

dR1

S; Γ,∆⇒ dl : {s1, ..., sn}i.G

4.23. dR2, com C = dl : {s1/s2}i.G


π1

...S; Γ⇒ D

π2

...S; ∆, D ⇒ G[s/l]

dR2

S; ∆, D ⇒ dl : {s1/s2}i.GCut

S; Γ,∆⇒ dl : {s1/s2}i.G


π1

...S; Γ⇒ D

π2

...S; ∆, D ⇒ G[s/l]

CutS; Γ,∆⇒ G[s/l]

dR2

S; Γ,∆⇒ dl : {s1/s2}i.G

4.24. eR, com C = el : τ.G


π1

...S; Γ⇒ D

π2

...S, le : τ ; ∆, D ⇒ G[le/l]

eR

S; ∆, D ⇒ el : τ.GCut

S; Γ,∆⇒ el : τ.G

96


π1

...S, le : τ ; Γ⇒ D

π2

...S, le : τ ; ∆, D ⇒ G[le/l]

CutS, le : τ ; Γ,∆⇒ G[le/l]

eR

S; Γ,∆⇒ el : τ.G


5.10. D = el : {s1, ..., sn}i.F


π1

...S, le : {s1, ..., sn}; Γ⇒ F [le/l]

eR

S; Γ⇒ el : {s1, ..., sn}i.F

π2

...S; ∆, F [s/l]⇒ C

eL1

S; ∆,el : {s1, ..., sn}i.F ⇒ CCut

S; Γ,∆⇒ C


π1[s/le]

...S; Γ⇒ F [s/l]

π2

...S; ∆, F [s/l]⇒ C

CutS; Γ,∆⇒ C

onde, pelo lema da substituição, π1[s/le] possui a mesma altura de derivação

de π1.

5.11. D = el : {s1/s2}i.F


π1

...S, le : {s1/s2}; Γ⇒ F [le/l]

eR

S; Γ⇒ el : {s1/s2}i.F

π2

...S; ∆, F [s/l]⇒ C

eL2

S; ∆,el : {s1/s2}i.F ⇒ CCut

S; Γ,∆⇒ C


π1[s/le]

...S; Γ⇒ F [s/l]

π2

...S; ∆, F [s/l]⇒ C

CutS; Γ,∆⇒ C


de π1.

97

5.12. D = dl : {s1, ..., sn}i.F


π1

...S; Γ⇒ F [s/l]

dR1

S; Γ⇒ dl : {s1, ..., sn}i.F

π2

...S, le : {s1, ..., sn}; ∆, F [le/l]⇒ C

dL

S; ∆,dl : {s1, ..., sn}i.F ⇒ CCut

S; Γ,∆⇒ C


π1

...S; Γ⇒ F [s/l]

π2[s/le]

...S; ∆, F [s/l]⇒ C

CutS; Γ,∆⇒ C


de π2.

5.13. D = dl : {s1/s2}i.F


π1

...S; Γ⇒ F [s/l]

dR2

S; Γ⇒ dl : {s1/s2}i.F

π2

...S, le : {s1/s2}; ∆, F [le/l]⇒ C

dL

S; ∆,dl : {s1/s2}i.F ⇒ CCut

S; Γ,∆⇒ C


π1

...S; Γ⇒ F [s/l]

π2[s/le]

...S; ∆, F [s/l]⇒ C

CutS; Γ,∆⇒ C


de π2.

QED.

98

5 Especificação de sistemasbioquímicos em SELL

Neste capítulo iremos descrever um formalismo para especificar e verificar proprieda-

des de sistemas bioquímicos onde consideramos modalidades espaciais e temporais. Como

a Lógica Linear trata as fórmulas como recursos, este é um formalismo ideal para repre-

sentar equações bioquímicas onde a cada interação temos o controle dos recursos sendo

consumidos e produzidos. Para tanto, utilizaremos SELL, que oferece um controle muito

mais refinado que a Lógica Linear Intuicionista. Cada interação dependerá das localiza-

ções dos componentes e do tempo, onde utilizaremos os subexponenciais de SELL para

representar cada interação por um location espacial e temporal.

Vamos especificar uma reação química em SELL e veremos como SELL pode nos

ajudar a verificar propriedades do sistema. Suponha, primeiramente, uma reação química

do tipo

F −→ G

em que consumimos F para produzir G. Em Lógica Linear, podemos representar essa

reação como

F ( G

Se quisermos considerar a localização espacial l dos componentes da reação, marcamos

ambos F e G com o índice l:

!lF (!lG

Se quisermos considerar que essa reação pode ocorrer em qualquer espaço, utilizamos

o quantificador e:

99

!ω e l : ω.(!lF (!lG)

Suponha que, na localização espacial a, podemos encontrar uma cópia de F e que, na

localização espacial b, podemos encontrar uma cópia de F e H. Então representamos:

!ω e l : ω.(!lF (!lG)⊗!aF⊗!bF⊗!bH

Assim, utilizamos SELL para descrever a especificação do sistema bioquímico. Con-

sidere um subexponencial não-limitado ω (isto é, ω ∈ U) e dois subexponenciais a, b tal

que a, b � ω e a � b. Seja F,G,H átomos e considere a seguinte fórmula

system =!ω e l : ω.(!lF (!lG)⊗!aF⊗!bF⊗!bH (5.1)

Os subexponenciais a, b podem ser interpretados como duas diferentes locations (ou

domínios espaciais) em uma célula. Assim, !aF (respectivamente !bF e !bH) significa que

em a (respectivamente b) podemos encontrar uma cópia de algum reagente F (respecti-

vamente F e H). A fórmula el : ω.(!lF (!lG) representa uma reação que, em um dado

location l � ω, consumimos F para produzir G. Portanto o sistema pode evoluir a um

estado onde o location a contém uma cópia de G e o location b contém uma cópia de G e

H como mostrado na derivação abaixo: (OLARTE et al., 2016).

F ⇒ F!aL

!aF ⇒ F!aR

!aF ⇒!aF

G⇒ G!aL

!aG⇒ G!aR

!aG⇒!aG (L

!aF (!aG, !aF ⇒!aGeL

el : ω.(!lF (!lG), !aF ⇒!aG!L

!ω e l : ω.(!lF (!lG), !aF ⇒!aG

F ⇒ F!bL

!bF ⇒ F!bR

!bF ⇒!bF

G⇒ G!bL

!bG⇒ G!bR

!bG⇒!bG (L

!bF (!bG, !bF ⇒!bGeL

el : ω.(!lF (!lG), !bF ⇒!bG!L

!ω e l : ω.(!lF (!lG), !bF ⇒!bG⊗R

!ω e l : ω.(!lF (!lG), !ω e l : ω.(!lF (!lG), !aF, !bF ⇒!aG⊗!bGC

!ω e l : ω.(!lF (!lG), !aF, !bF ⇒!aG⊗!bG

H ⇒ H!bL

!bH ⇒ H!bR

!bH ⇒!bH⊗R

!ω e l : ω.(!lF (!lG), !aF, !bF, !bH ⇒!aG⊗!bG⊗!bH⊗L

!ω e l : ω.(!lF (!lG)⊗!aF⊗!bF⊗!bH ⇒!aG⊗!bG⊗!bH

Neste capítulo mostraremos como dependências espaciais e temporais em sistemas bi-

oquímicos podem ser caracterizados como fórmulas em SELLSe. Utilizaremos um conjunto

de reações que possuem a seguinte forma:

rj : [c1.A1]a1 + ...+ [cn.An]an −→k [d1.B1]b1 + ...+ [dn.Bn]bn (5.2)

100

onde ci unidades de Ai localizadas no domínio espacial ai são consumidas em k uni-

dades de tempo para produzir dj unidades de Bj localizadas no domínio espacial bj.

Para modelar sistemas considerando suas modalidades temporais e espaciais em SELLSe,

utilizaremos a assinatura subexponencial (A,�, U) mostrada no capítulo anterior. Temos

que os únicos subexponenciais não-limitados são tω e i+, onde tω é utilizado para marcar

o conjunto de reações que pode ser usado quantas vezes for necessário e i+ representa a

unidade de tempo que se inicia em i e será usada para especificar propriedades do sistema

que serão mostradas adiante.

Considere, por exemplo, uma variável subexponencial lx : 4+. Ela pode ser instanciada

com qualquer unidade de tempo que se inicia em 4. Os subexponenciais lineares 0, 1, 2, ...

representam a unidade de tempo, enquanto que os subexponenciais lineares sa.i, sb.i, ...

representam o domínio espacial sx na unidade de tempo i.

Para cada elemento químico A no sistema, temos o símbolo de constante A em SELL

para representar esse elemento. Temos o predicado binário ct(·, ·) que representa a con-

centração do elemento. Intuitivamente, a fórmula !sb.2ct(A, c) significa que a concentração

de A no domínio espacial sb é c durante a segunda unidade de tempo. De forma usual, c

é definido como a n-ésima aplicação da função sucessor suc para a constante 0. Usamos

sucn(x) para denotar a n-ésima aplicação de suc em x.

Utilizando ct(·, ·), podemos agora definir o estado do sistema no tempo t.

Definição 5.1 (State). O estado do sistema na unidade de tempo t é definido como

state(t) =⊗s∈S

⊗Ai∈A

!s.t[ct(Ai, ci)] (5.3)

onde A denota o conjunto de reagentes e S denota o conjunto de domínios espaciais.

Se não existem reagentes do tipo Aj no espaço sk, então cj = 0.

O modelo de uma reação representado em (5.2) é uma fórmula que primeiro confere

se os reagentes necessários estão disponíveis nos domínios espaciais. Assim, os reagentes

são consumidos e os produtos são adicionados após k unidades de tempo. Definimos então

uma reação:

Definição 5.2 (Reaction). Uma reação que ocorre na unidade de tempo t é definida como

eq(t) = ∀~x.[consume(t) ( produce(t+ k)] (5.4)

101

onde ~x = x1, ..., xn.

Temos que

consume(t) =⊗s∈S

⊗Ai∈A

!s.t[ct(Ai, Ni)] (5.5)

Ni =

xi, se [ci.Ai]s não ocorre no lado esquerdo da reação

succi(xi), se [ci.Ai]s ocorre no lado esquerdo da reação

E temos que

produce(t) =⊗s∈S

⊗Ai∈A

!s.t[ct(Ai, Ni)] (5.6)

Ni =

xi, se [di.Ai]s não ocorre no lado direito da reação

sucdi(xi), se [di.Ai]s ocorre no lado direito da reação

O quantificador ∀~x permite-nos vincular o atual número de reagentes no sistema.

A fórmula consume consome os reagentes necessários e a fórmula produce adiciona tais

reagentes após k unidades de tempo. Note que a concentração dos reagentes que não são

utilizados na reação são simplesmente copiados sem alterações após t + k unidades de

tempo.

Agora, podemos modelar o conjunto de reações do sistema:

Definição 5.3 (Conjunto de reações do sistema). O conjunto de reações do sistema é

definido como

eqs =!tω{elx : 0+.[eq1(lx)&...&eqk(lx)]} (5.7)

O subexponencial não-limitado !tω permite-nos usar o conjunto de reações quantas

vezes for necessário. O quantificador elx : 0+ nos diz que, em qualquer unidade de tempo,

as reações estão disponíveis para serem realizadas. O conectivo & permite-nos escolher

uma das reações e descartar as outras.

Finalmente, podemos definir o modelo de um sistema na unidade de tempo t:

102

Definição 5.4 (System(t)). O sistema bioquímico na unidade de tempo t é definido como

system(t) = eqs⊗ state(t) (5.8)

Por exemplo, suponha que a seguinte reação química ocorre:

A −→ 2B (5.9)

rj : [1.A]a −→k [2.B]b

Ou seja, consumimos 1 quantidade de A para produzir 2 quantidades de B em k

unidades de tempo. Para especificar essa reação em SELL, iremos renomear algumas

definições para tornar a derivação de fácil leitura e entendimento. Considere:

eqs′ = elx : 0+.[∀x.∀y.(F ⊗ F ′) ( (H ⊗H ′)] (5.10)

onde

F =!lxct(A, suc(x))

F ′ =!lyct(B, y)

H =!lx+1ct(A, x)

H ′ =!ly+1ct(B, suc(suc(y)))

A equação (5.10) representa nossa reação: a partir do tempo 0 (instanciado por lx e lypara A e B respectivamente), temos a concentração suc(x) do reagente A e a concentração

y do reagente B. Após a reação, nos locations lx+1 e ly +1, a concentração de A tornou-se

x e a concentração de B tornou-se suc(suc(y)). Ou seja, consumimos 1A para produzir

2B, como em (5.9).

Considere agora a concentração inicial (arbitrária) dos elementos químicos A e B:

state(t) =!si.tct(A, 3)⊗!si.tct(B, 5) (5.11)

Ou seja, a concentração inicial de A é 3 e a concentração inicial de B é 5. Temos então

o sequente:

state(t)⊗!ωeqs′ ⇒ G (5.12)

103

onde G é a propriedade do sistema que devemos verificar. Assim, temos a derivação:

state(t)⇒ state(t)def

state(t)⇒!si.tct(A, suc(2))⊗!si.tct(B, 5)

!ωeqs′, !si.t+1ct(A, 2), !si.t+1ct(B, 7)⇒ Gdef

!ωeqs′, H,H ′ ⇒ G⊗L

!ωeqs′, H ⊗H ′ ⇒ G(L

state(t), !ωeqs′, !si.tct(A, suc(2))⊗!si.tct(B, 5) ( (H ⊗H ′)⇒ G∀L

state(t), !ωeqs′,∀x.∀y.[!si.tct(A, suc(x))⊗!si.tct(B, y) ( (H ⊗H ′)]⇒ GeL

state(t), !ωeqs′,elx : 0+.[∀x.∀y.(F ⊗ F ′) ( (H ⊗H ′)]⇒ Gdef

state(t), !ωeqs′, eqs′ ⇒ G!L

state(t), !ωeqs′, !ωeqs′ ⇒ GC

state(t), !ωeqs′ ⇒ G⊗L

state(t)⊗!ωeqs′ ⇒ G

onde def não é nenhuma regra lógica, mas sim a substituição da definição nos respec-

tivos termos. Note que na regra eL substituímos lx e ly por si.t e na regra ∀L substituímos

x por 2 e y por 5.

A concentração inicial de A era 3 e a concentração inicial de B era 5. Agora, observe

o último sequente da direita:

!ωeqs′, !si.t+1ct(A, 2), !si.t+1ct(B, 7)⇒ G (5.13)

Nesse último sequente, a concentração de A é 2 e a concentração de B é 7. Ou seja,

consumimos 1A para produzir 2B, assim como queríamos em (5.9).

Suponha agora que em nosso sistema ocorrem duas reações

A −→ 2B (5.14)

rj : [1.A]a −→k [2.B]b

A −→ C (5.15)

rj : [1.A]a −→k [1.C]c

Como temos duas reações, escrevemos as duas equações de reação

104

eq1 = ∀x.∀y.∀z.[F ⊗ F ′ ⊗ F ′′] ( [H ⊗H ′ ⊗ F ′′] (5.16)

eq2 = ∀x.∀y.∀z.[F ⊗ F ′ ⊗ F ′′] ( [H ⊗ F ′ ⊗H ′′] (5.17)

onde

F =!lxct(A, suc(x))

F ′ =!lyct(B, y)

F ′′ =!lzct(C, z)

H =!lx+1ct(A, x)

H ′ =!ly+1ct(B, suc(suc(y)))

H ′′ =!lz+1ct(C, suc(z))

Além disso, temos

eqs′ = elx : 0+.[eq1&eq2] (5.18)

state(t) =!si.tct(A, 3)⊗!si.tct(A, 5)⊗!si.tct(C, 6) (5.19)

Assim, temos a derivação

state(t)⇒ state(t)

!ωeqs′, !si.t+1ct(A, 2), !si.tct(B, 5), !si.t+1ct(C, 7)⇒ Gdef

!ωeqs′, H, F ′, H ′ ⇒ G⊗L

!ωeqs′, H ⊗ F ′ ⊗H ′ ⇒ G(L

state(t), !ωeqs′, (F ⊗ F ′ ⊗ F ′′) ( (H ⊗ F ′ ⊗H ′′)⇒ G∀L

state(t), !ωeqs′,∀x.∀y.∀z.[(F ⊗ F ′ ⊗ F ′′) ( (H ⊗ F ′ ⊗H ′′)]⇒ Gdef

state(t), !ωeqs′, eq2 ⇒ G&L

state(t), !ωeqs′, eq1&eq2 ⇒ GeL

state(t), !ωeqs′,elx : 0+.[eq1&eq2]⇒ Gdef

state(t), !ωeqs′, eqs′ ⇒ G!L

state(t), !ωeqs′, !ωeqs′ ⇒ GC

state(t), !ωeqs′ ⇒ G⊗L

state(t)⊗!ωeqs′ ⇒ G

105

Na regra ∀L substituimos x por 2, z por 6 e y por 5. Note que, como escolhemos a

reação eq2 na regra &L, a concentração de B permaneceu a mesma, pois B não reage em

(5.15). Por causa dessa escolha, temos o último sequente

!ωeqs′, !si.t+1ct(A, 2), !si.tct(B, 5), !si.t+1ct(C, 7)⇒ G (5.20)

Como queríamos (5.15), foi consumido 1A para produzir 1C.

Verificamos que SELL é um bom sistema para especificar os sistemas físicos formal-

mente. Isso vem do fato de os subexponenciais serem úteis para representar diferentes

modalidades de um sistema (neste capítulo foram modalidades espaciais e temporais).

106

6 Considerações finais

Ao longo do trabalho, verificamos que a Lógica Linear possui uma excelente estru-

tura para tratar de sistemas reais. Sem as regras de enfraquecimento e contração, existe

diferença entre os conectivos aditivos e multiplicativos e isso nos permite tratar fórmulas

como recursos a serem utilizados durante a prova. Esse controle é muito mais expressivo

com SELL, onde podemos separar as fórmulas em várias partes e cada uma representa

determinada modalidade (no capítulo 5 foram modalidades espaciais e temporais).

Provamos que a regra de corte na Lógica Linear e em SELL é uma regra admissí-

vel. Esse resultado é fundamental em teoria da prova, pois assim podemos concluir a

consistência do sistema para a Lógica Linear e para SELL. Do ponto de vista teórico, a

regra de corte é um resultado importante, pois ela nos diz que é permitido utilizar le-

mas intermediários para finalizar a prova: se um subsistema representado por Γ exibe um

comportamento D e, assumindo D, nós sabemos que ∆ conclui C, então todo o sistema

conclui C.


Γ,∆⇒ C

Do ponto de vista computacional, é complicado possuir um procedimento automático

onde se utiliza a regra de corte: o computador teria que “adivinhar” o lema D para

continuar a prova.

A busca pela ordem das regras que se aplica para terminar a prova do sequente motivou

o surgimento do focusing (ANDREOLI, 1992). Nesse sentido, uma prova que utiliza focusing,

i.e., possui regras de forma que não se perca a demonstrabilidade, é uma prova focada1.

De fato, o sistema de prova focado na Lógica Linear é completo, i.e., qualquer prova em

Lógica Linear pode ser representada por uma prova focada.

Uma perspectiva futura de trabalho é estudar SELL em sistemas focados. De fato,

se utilizarmos focusing na especificação de sistemas bioquímicos, cada passo da derivação1do inglês, “focused”

107

corresponde a um passo na reação bioquímica e temos o controle de cada iteração da reação

(OLARTE et al., 2016). Através de focusing é possível construir processos semi-automáticos

onde já existe lemas previamente demonstrados e assim temos provas automáticas. Pode-

mos então no futuro também utilizar SELL para especificar outros sistemas.

108

Referências

ANDREOLI, J.-M. Logic programming with focusing proofs in linear logic. Journal ofLogic and Computation, Oxford Univ Press, v. 2, n. 3, p. 297–347, 1992.

BARWISE, J. Handbook of Mathematical Logic. Amsterdan, London, New York, Tokyo:Elsevier, 1977.

BENTON, N. et al. A term calculus for intuitionistic linear logic. In: SPRINGER.International Conference on Typed Lambda Calculi and Applications. [S.l.], 1993. p.75–90.

DANOS, V.; JOINET, J.-B.; SCHELLINX, H. The structure of exponentials: Uncoveringthe dynamics of linear logic proofs. In: SPRINGER. Kurt Gödel Colloquium onComputational Logic and Proof Theory. Springer Berlin Heidelberg, 1993. p. 159–171.

GIRARD, J.-Y. Linear logic. Theoretical Computer Science, North-Holland, n. 50, p.1–102, 1986.

GIRARD, J.-Y. Linear logic: its syntax and semantics. London Mathematical SocietyLecture Note Series, Cambridge University Press, p. 1–42, 1995.

LINCOLN, P. Linear logic. ACM SIGACT News, ACM, v. 23, n. 2, p. 29–37, 1992.

LINCOLN, P. et al. Decision problems for propositional linear logic. Annals of pure andapplied logic, Elsevier, v. 56, n. 1-3, p. 239–311, 1992.

NEGRI, S.; PLATO, J. V. Structural Proof Theory. New York: Cambridge UniversityPress, 2001.

NIGAM, V.; MILLER, D. Algorithmic specifications in linear logic with subexponentials.In: ACM. Proceedings of the 11th ACM SIGPLAN conference on Principles and practiceof declarative programming. [S.l.], 2009. p. 129–140.

NIGAM, V.; OLARTE, C.; PIMENTEL, E. A general proof system for modalities inconcurrent constraint programming. In: SPRINGER. CONCUR. [S.l.], 2013. v. 8052, p.410–424.

NIGAM, V.; OLARTE, C.; PIMENTEL, E. On subexponentials, focusing and modalitiesin concurrent systems. Logic and Applications LAP 2016, p. 42, 2016.

NIGAM, V.; PIMENTEL, E.; REIS, G. Specifying proof systems in linear logic withsubexponentials. Electronic Notes in Theoretical Computer Science, Elsevier, v. 269, p.109–123, 2011.

OLARTE, C. et al. A proof theoretic view of spatial and temporal dependencies inbiochemical systems. Theoretical Computer Science, Elsevier, v. 641, p. 25–42, 2016.

109

OLARTE, C.; PIMENTEL, E.; NIGAM, V. Subexponential concurrent constraintprogramming. Theoretical Computer Science, Elsevier, v. 606, p. 98–120, 2015.

REIS, G. M. N. Especificação de sistemas utilizando lógica linear com subexponencias.UFMG, 2010.

ROCCA, S. R. D.; ROVERSI, L. Lambda calculus and intuitionistic linear logic. StudiaLogica, Springer, v. 59, n. 3, p. 417–448, 1997.

TROELSTRA, A. S.; SCHWICHTENBERG, H. Basic Proof Theory. 2. ed. New York:Cambridge University Press, 2000.

Documents

Um estudo de Lógica Linear com Subexponenciais...Um estudo de lógica linear com subexponenciais / Laura Fernandes Dell Orto. Natal, 20 17 . 109 f. Orientador: Prof. Dr. Carlos Alberto