ads:
Vaston Gonçalves da Costa
Compactação de Provas Lógicas
Tese de Doutorado
Tese apresentada ao Programa de Informática do Departa-
mento de I nformática da PUC–Rio como requi- sito parcial
para obtenção do título de Doutor em Informática.
Orientador: Prof. Edward Hermann Haeusler
Rio de Janeiro
Abril de 2007
PUC-Rio - Certificação Digital Nº 0220933/CA
ads:
Livros Grátis
http://www.livrosgratis.com.br
Milhares de livros grátis para download.
Vaston Gonçalves da Costa
Compactação de Provas Lógicas
Tese apresentada ao Programa de Informática do Depar-
tamento de Informática do Centro Técnico Científico da
PUC–Rio como requisito parcial para obtenção do título
de Doutor em Informática. Aprovada pela Comissão Exam-
inadora abaixo assinada.
Prof. Edward Hermann Haeusler
Orientador
Departamento de Informática — PUC–Rio
Prof. Luis Carlos Pinheiro Dias Pereira
PUC-Rio
Prof. Maurício Ayala Rincon
Unb
Prof. Marcelo da Silva Corrêa
UFF
Prof. Geiza Maria Hamazaki da Silva
PUC-Rio
Prof. José Eugenio Leal
Coordenador Setorial do Centro Técnico Científico —
PUC–Rio
Rio de Janeiro, 09 de Abril de 2007
PUC-Rio - Certificação Digital Nº 0220933/CA
ads:
Todos os direitos reservados. É proibida a reprodução total ou
parcial do trabalho sem autorização da universidade, do autor e
do orientador.
Vaston Gonçalves da Co sta
Graduou–se em Matemática pela Universidade Federal de Uber-
lândia - UFU. Obteve título de Mestre em Matemática Apli-
cada, com ênfase em Teoria da Computação, pela Universidade
de Brasília - UnB.
Ficha Catalográfica
Costa, Vaston Gonçalves da
Compactação de Provas Lógicas / Vaston Gonçalves
da Costa; orientador: Edward Hermann Haeusler. — Rio
de Janeiro : PUC–Rio, Departamento de Informática,
2007.
66 f. ; 30 cm
1. Tese (doutorado) - Pontifícia Universidade
Católica do Rio de Janeiro, Departamento de Infor-
mática.
Inclui referências bibliográficas.
1. Informática – Tese. 2. Teoria da prova. 3. Complex i-
dade de Provas. 4. Lógica Proposicional. 5. Cálculo de
Seqüentes. 6. D edução Natural. I. Hermann, Edward. II.
Pontifícia Universidade Católica do Rio de Janeiro. De-
partamento de I nformática. I II. Título.
CDD: 004
PUC-Rio - Certificação Digital Nº 0220933/CA
Esta tese é dedicada
à minha esposa Angela, meu porto s eguro, e ao meu filho Vinícius, minh a
motivação, pela compreensão e apoi o nos mui tos momentos que tive que privá-los
da minha companh ia e atenção.
PUC-Rio - Certificação Digital Nº 0220933/CA
Agradecimentos
Ao meu o ri entador Professor Edward Hermann Haeusler pel o apoio e incen-
tivo fundamentais para a realização deste t rabalho. Hermann... boas ondas!
À m inha mãe, Dona Olinda, que me incentivou e me apoiou para o meu
ingresso à vida acadêmica. Es pero ter correspon dido às suas expectativas.
Às minhas irmãs, Virgínia e Valéria, pelas palavras de apoio.
Aos meus colegas da PUC-Rio, em particul ar aos que integram ou integraram
a equipe do TecMF, pelos longos anos de convívio em um ambiente tão agradável.
Ao professor Lev Gordeev pela ajuda e contribuição.
Aos professo res da banca avaliadora pelas sugestões apresentadas para a
melhoria do trabalho final e por apon tarem direções de trabalhos fut uros.
Ao CNPq e à PUC–Rio, pelos auxí lios concedidos.
PUC-Rio - Certificação Digital Nº 0220933/CA
Resumo
Costa, Vaston Gonçalves da; Hermann, E dward. Compactação de
Provas Lógicas. Rio de Janeiro, 2007. 66p. Tese de Doutorado — De-
partamento de Informática, Pontifícia Universidade Católica do Rio de
Janeiro.
É um fato conhecido que provas clássicas podem ser demasiadamente
grandes. Estudos em teoria da prova descobriram diferenças exponenciais entre
provas normais (ou provas livres do corte) e suas respectivas provas não normais.
Por out ro lado, provadores automáticos de teorema usualmente se baseiam na
construção de provas normais, livres de corte ou provas de corte atômico, pois
tais procedimento envolvem menos escolhas. Provas de algumas t autologias são
conhecidamente grandes quanto realizadas sem a regra do corte e curtas quando
a utilizam. Queremos com este trabalho apresentar procedimentos para reduzi r o
tamanho de provas prop osicionais. Neste sentido, apresentamos dois métodos. O
primeiro, denominado método vertical, faz uso de axiomas de extensão e alguns
casos é poss ível uma redução considerável no tamanho da prova. A p resent amos
um procedimento que gera tais axiomas de extensão. O segundo, denominado
método horizontal, adiciona fórmulas máximas por meio de unificação via
substituição de variáveis proposicionais. Também apresentamos um método que
gera tal unificação durante o processo de construção da prova. O primeiro método
é aplicado a dedução natural enquanto o segundo à Dedução Natural e Cálculo
de Seqüentes. As provas produzidas correspondem de certo modo a provas não
normais (com a regra do corte).
Palavras–chave
Teoria da prova. Complexidade de Provas. Lógica Proposicion al . Cál-
culo de Seqüentes. Dedução Natural.
PUC-Rio - Certificação Digital Nº 0220933/CA
Abstract
Costa, Vaston Gonçalves da; Hermann, Edward. Logic Proofs Com-
pactation. Rio de Janeiro, 2007. 66p. PhD Thesis — Department of
Informática, Pontifícia Universidade Católica do Rio de Janeiro.
It is well-known that the size of propositi onal classical proofs can be
huge. Proof theoretical studies discovered exponential gaps between normal o r
cut-free proofs and their respective non-normal proofs. The task of automatic
theorem proving is, on the other hand, usu ally based on the construction of
normal, cut-free or on ly-atomic-cuts proofs, since this procedure produces less
alternative choices. There are familiar t autologies such that t h e cut-free proof
is huge while th e non-cut-free is small. The aim of this work is to reduce the
weight of proposicional deductions. In this sense we present two methods. The
first, namely vertical method, uses the extension axi oms. We present a method
that generates a such extension axiom. T he second, namely horizon tal method,
adds suitable (propositional) unifications mod ulo variable subs titutions. We also
present a method that generates a such un ification during the proving process.
The proofs produ ced correspond in a certain way to no n normal proofs (non
cut-free proofs).
Keywords
Proof Theory. Proof Com plexity. Propositional Logic. Sequent Calcu-
lus. Natural Deduction.
PUC-Rio - Certificação Digital Nº 0220933/CA
Sumário
1 Introdução 10
2 Preliminares 13
2.1 Sistema de Dedução Natural 14
2.2 C lasses hierárquicas e problemas lógicos 17
2.3 Sistemas de Frege 20
2.4 R esolução 21
2.5 Princípio das Casas dos Pombos-PHP 21
2.6 PHP em Resolução 23
3 Método Horizontal 24
3.1 D efinições 24
3.2 O Método 26
3.3 Formalização do método 29
3.4 C onclusão do método 39
4 Método Vertical 40
4.1 D efinições 40
4.2 M étodo 42
4.3 R esultado Principal 43
4.4 C onclusão do capítulo 46
5 Conclusão 49
A Sistemas de Frege 53
A.1 Sistemas de provas proposicionais 53
A.2 Sistemas de Frege 54
A.3 Dedução Natural 55
A.4 Frege estendido 57
B Esquema da prova de P HP
2
58
C Numeral de Church 60
D Clássica para Intuicionista 62
PUC-Rio - Certificação Digital Nº 0220933/CA
Lista de figuras
3.1 Representação gráfica do método 27
3.2 Aplicação do método vertical 27
3.3 Representação Gráfica do Método Horizontal 35
3.4 Modus Ponens 36
3.5 Esboço da redução da transitividade para (a
1
→ a
4
) → (a
4
→
a
8
) → (a
1
→ a
8
) 38
4.1 Prova U -similar 42
4.2 Esquema de uma prova encadeada 43
C.1 I
3
0
60
C.2 Numeral I
4
0
modificado. 61
PUC-Rio - Certificação Digital Nº 0220933/CA
1
Introdução
Existem diversas interconexões entre Teoria da prova e Ciência da Compu-
tação que merecem citação destacada tais como: procedimentos de tipagem para
linguagens de prog ram ações, g eração de programas p or meio de extração de con-
teúdo computacional de p rovas lógicas, complexidade computacional, estimativa
de tamanho de provas normais em certos sistemas lógicos e outros. Por outro lado,
são bem conhecidas as hierarquias de análise computacional geradas por meio de
problemas de decisão lógica. Para cada classe hierárquica pode se fornecer um pro-
blema completo representado em lógica formal. Alguns destes problemas envolvem
validade de uma fórmula em uma certa lóg ica, o que implica existência de prova. É
amplamente conhecido que o tamanho de uma prova é um tema relevante tanto na
teoria quanto na prática.
Especificamente as provas curtas po dem ser uma contra-parte d e u ma prova
teórica de computações viáveis, onde por definição o comprimento de uma p rova
curta é polinomial em relação ao comprim ento de sua conclusão. O comprim ento
de uma fórmu la ou de uma prova é dado pelo número de símbolos usado para
escrevê-la. O fato de que t oda tautologia clássica possui uma prova curta implica
que CoNP = N P , e a existência de tautologias que não possuem esta propriedade
em qualquer sistema de prova implica que CoNP = N P , e assim NP = P ,
de acordo com o teorema de Cook (CR79). Para lógica int uicionista a existência
de provas curtas para cada tautologia implica NP = P SP ACE. Além disso,
Seldin mostrou que em sistemas de Dedução Natural (doravante DN ), qualquer
tautologia clássica p ode ser p rovada com no máximo um a aplicação da regra do
absurdo clássico. A prova deste fato é realizada fornecendo u ma transformação de
uma prova em DN de α em uma prova de α em dedução natural tendo no máximo
uma aplicação da regra do absurdo e, caso a prova precise da regra, esta seria a
última regra apl icada. Posteriormente é verificado se a prova anterior é polinomial
em relação ao tamanho de α então a post erio r também será. Desta forma,
P oly(|α|)
Cla
α
se, e somente se,
P oly(|α|)
Int
¬α → ⊥. Portanto, a existência de provas polinomiais
para cada tautologia intuicionista implica na existência d e provas polinomiais para
cada tautologia clássica, assim neste caso CoNP = P SP ACE = N P . Em
outras palavras, a existência de provas polinomiais para toda tautologia intuicionista
PUC-Rio - Certificação Digital Nº 0220933/CA
Capítulo 1. Introdução 11
é equivalente a NP = CoNP = P SP ACE enquanto para o caso clássico
NP = CoNP . Estas provas devem ser consideradas em sistemas de p rovas que
polinomi al mente simulam sistemas de deduções conhecidos, t ai s como Dedu ção
Natural ou Cálculo de Seqüentes.
A decisão se as iguald ades CoN P = P SP ACE, NP = P SP ACE e
NP = CoN P são válidas ou não é uma tarefa difícil e provoca debates instigant es.
Por outro lado, enquanto não são encontradas as resp ostas para estas questões,
há exemplos bem conhecidos de limites inferiores grandes para provas de tipos
específicos tratadas em certos sistemas de prova. Um caso q ue vale mencionar é
o li mite inferior super po linomial para a prova do Princípio das Casas de Pombos
(doravante P HP ) quando tratado em sistema de provas em Resolução. Este limite
inferior é o mesmo para Cálculo de Seqüentes livres de corte. Este exemplo tem
sido muito út il para argumentar em favor da regra do corte para fornecer provas
em Lógi ca Proposicional, uma vez que tais lim ites inferiores grandes não são
conhecidos para qualquer tautologia proposicional em cálculo de seqüentes com
regra do corte.
Assim, dada uma prova Π em DN, sua correspondente prova normal Π
tem limite inferior hiper-polinomial conhecido com relação ao tamanho de Π bem
como alguns exemplos com limit e inferior hi per-polino mial com relação a Π. Um
destes exemplos pode ser encontrado em Troelst ra (vide (TS00, pp. 215)) e usa a
representação ti pada de numerais de Church para construir um prova de tamanho
polinomi al de uma tautolo gia que tem uma correspond ente prova no rmal que não
pode ser limit e de qualquer função elementar. Para lógica de primeira ordem,
Orekov apresenta exemplos de fórmulas com provas de tamanho linear para o qual
qualquer prova normal tem um limite inferior hiper-polinomial.
Toda esta discussão acima aponta para a necessidade de mecanism os para
comprimir provas. Pode se argumentar sobre o us o de já conhecidos algoritmos de
compactação para tal fato. Contudo, o seu uso é baseado no fato de que a p rova já
seja conhecida. A regra do corte é comum ente colocada de lado em qualquer imple-
mentação de provadores de teoremas, e claramente este é o problema com provas
demasiadamente grandes. O mesmo pode ser dito sob re provadores de teorem as em
Dedução Natural que são feitos para construir provas normais. Para inclusão da re-
gra do corte na implementação ( ou permitir que a imp lementação construa provas
não normais), o implementador deve considerar uma grande quantidade de alt er-
nativas em cada passo da prova. Isto tornará a implementação pouco eficiente. Por
outro lado, se algumas estratégias po n tuais que permitem que a regra do corte (uma
fórmula máxima em terminologia de DN) sejam previamente conhecidas acarreta
implementação melhor do que a anterior, sendo capaz de produzir provas curtas
para casos em que implementações livres do corte não po d em.
PUC-Rio - Certificação Digital Nº 0220933/CA
Capítulo 1. Introdução 12
Propomos dois m ét odos para a redução do tamanho de provas proposicionais.
O primei ro, denomi nado método horizontal, atinge a eficiência desejada
quando adiciona regras de atenuação conjuntamente com uma unificação via su bs-
tituição de variáveis ( proposicionais). Também apresentamos um método que gera
tal unificação durante o processo de construção da prova.
O segundo, denominado método vertical, alcança a eficiência d esejada por
meio do uso de axiomas de extensão. Apresentamos um procediment o que gera tais
axiomas de extensão.
Capítulo 2 apresenta a terminologia básica u sada no artigo, alguns resul tados
também básicos de hierarquia computacional, uma introdução de sistemas de provas
com ênfase em sistemas de Frege, o princípio das casas de po mbos e alguns
resultadas conhecidos de aplicação em sistemas de Frege em Resolu ção. Também
mostramos no final do capít ulo 2 uma tradução da lógica clássica para a lógica
intuicionista. No capítulo 3 apresentamos o método Horizontal com exemplos em
dedução Natural e formalização em um cálculo de seqüentes simplificado, SEQ
0
.
No capítulo 4 é apresentado o método Vertical para redução de p rovas. Por fim, no
capítulo 5 são apresentadas as conclusões e trabalhos fut uros.
PUC-Rio - Certificação Digital Nº 0220933/CA
2
Preliminares
Com intuito de fixar a notação, apresentaremos, neste capítulo, result ados e
definições essenciais que serão utilizados ao longo da tese.
Para indicar identidade de duas expressões, usaremos ≡.
N é utilizado para os números naturais, com zero incluído. Segui rem os as
notações padrões da teori a dos conjuntos como ∈, ⊂.
Uma fórmula proposicional é representada por letras gregas minúsculas
α, β, γ, . . . (possivelmente com sub- ou supescrito ou
) sendo cons tituída de va-
riáveis proposicionais p, q, r, . . . (possivelmente com sub- ou su pescrito ou
), e de
um conjunto de conectivos unários e binários ¬, ∧, ∨ e →.
O conjunto de variáveis proposicionais em uma fórmula α será denotado por
V (α).
O tam anh o de uma fórmula é definido pelo número total de símbolos que
aparece na fórmul a.
O tamanho de uma prova é definido pelo número total de símbolos na prova.
Definição 2.1 (Subfórmulas) A noção de subfórmula que usaremos s eguirá o
sentido de Gentzen.
Subfórmulas de α serão definidas por
(i) α é uma subfórmula de α;
(ii) α é uma subfórmula de ¬α;
(iii) Se γβ é u m a subfórmula de α então também são γ, β para = ∨, ∧, →.
Nossa avaliação de complexidade de um método levará em conta a "taxa
de crescimento" da função correspondente. Será usado o sím b olo de ordem de
magnitude O para lidar com este conceito.
Definição 2.2 Considerando f e g como funções de N em N. Então:
O(f) é o conjunto de funções g tais que para algum r > 0 e para todo n a
menos de uma quant idade finita, g(n) < r.f(n).
Usaremos com o sistema de provas o sistema de Dedução Natural (ND)
como em Prawitz (Pra65) seguindo a convenção de apresentar árvores de provas,
colocando as premiss as maiores das regras de eliminação no lado esquerdo.
PUC-Rio - Certificação Digital Nº 0220933/CA
Capítulo 2. Preliminares 14
2.1
Sistema de Dedução Natural
Definição 2.3 (Sistemas de Dedução Natural)
Um sistem a de d edu ção natural (ND) é determinado a partir de um conj unto
de regras d efin idas sobre fórmulas d e uma linguagem que representam a introdução
e a eliminação dos op eradores lógicos, e uma noção de dedução.
As regras são expressões da forma:
S
1
, S
2
, . . . , S
n
S
tal que S
1
, S
2
, . . . , S
n
e S são f órmulas. Neste caso, dizemos que S é inferida
a partir de S
1
, S
2
, . . . , S
n
ou de S
1
, S
2
, . . . , S
n
se infere S.
Em dedução natural, nenhum fórmula é considerada axioma ticamente válida,
porém é permi tido intro duzir, a qualquer momento, uma fórmula como hipótese.
Como resul tado dessas introduções nas inferências, podemos determinar se uma
dada fórmu la depende ou não de uma certa hipótese. Quando a fórmula in ferida se
torna independente de alguma das hipóteses, dizemos então que esta descarrega a
hipótese em questão. Na linguagem proposicional, por exemplo, existem tres formas
de descarregar as hipóteses:
1- Dada uma dedução de β a p artir de {α} ∪ Γ, podemos inferir α → β a partir
de Γ, sendo ent ão a hipótese α descarregada.
2- Dada uma dedução de ⊥ a partir d e {α} ∪ Γ, podemos inferir ¬α a par tir de
Γ, sendo então a hipótese α descarreg ada.
3- Dadas três deduções: u m a de α ∨β, outra de γ a partir de {α} ∪Γ
1
, e a terceira
de γ a partir de {β}∪Γ
2
, podemos inferir γ a parti r d e Γ
1
∪Γ
2
∪{α∨β} , send o
α e β as hipóteses descarregadas (α da segunda dedução e β da terceira
dedução).
As regras de in ferência consistem de uma regras de intro dução e outra de
eliminação para cada operador lógico além de dua s regras para o ⊥, u m a usad a
para a lógica intuicionista (⊥
i
) e outra para a lógica clássi ca (⊥
c
)
Para facilitar a leitura da dedução, col oca-se as hipóteses descarregadas
entre parênteses, entendendo assim que a nova dedução não depende das hipóteses
que foram descarregadas.
Π
1
α
Π
2
β
α ∧ β
∧I
Π
1
α ∧ β
α
∧E
r
Π
1
α ∧ β
β
∧E
L
PUC-Rio - Certificação Digital Nº 0220933/CA
Capítulo 2. Preliminares 15
[α]
u
Π
1
β
α → β
→I,u
Π
1
α → β
Π
2
α
β
→E
Π
1
α
α ∨ β
∨I
R
Π
1
β
α ∨ β
∨I
L
Π
1
α ∨ β
[α]
u
Π
2
C
[β]
v
Π
2
C
C
∨E,u,v
Π
1
⊥
α
⊥
i
α diferente de ⊥.
[¬α]
u
Π
1
⊥
α
⊥
c
α não p ossui a forma β → ⊥.
Nas aplicações de E-regras, a premi ssa contendo a ocorrência de operadores
lógicos que serão eliminados é dita premissa maior; a outra premissa é dita
premissa menor da regra de aplicação.
2.1.1
Corte em Dedução Natural
Durante o processo de construção de uma derivação, não parece ser adequado
a introdução de algo e a posterior eliminação em seguida. Este é o conceito chave
para simpli ficação de uma derivação: ev itar uma eliminação após um a introdução.
Se uma derivação possui uma introd ução seguida por uma elimin ação, então
pode-se, como regra, simplificá-la.
Apresentaremos os resultados, contud o , eles não serão demonstrados. Maio-
res detalhes podem ser encontrados em van Dalen (vD9 7).
Definição 2.4 Uma fórm ula γ é um corte em um a derivação quando ela é a
conclusão de uma regra de int rodução e a premissa maior de uma regra de
eliminação. γ é dita a fórm ula do corte.
Derivações p odem ser simplificadas através de eliminações de cortes, por
exemplo:
α
Π
β
α → β
Π
α
β
→E
converte para
Π
α
Π
β
Denotamos p or Π >
1
Π
para representar "Π converte para Π
". Π > Π
para
representar que "existe uma seqüência finita de conversões Π = Π
0
>
1
Π
1
>
1
. . . >
1
Π
n−1
= Π"e Π ≥ Π
para representar Π > Π
ou Π = Π
. (Π reduz a Π
).
PUC-Rio - Certificação Digital Nº 0220933/CA
Capítulo 2. Preliminares 16
Definição 2.5 Se não existe Π
1
tal q ue Π
1
>
1
Π
1
(i.e se Π
1
não cont ém cortes),
então chamamos Π
1
uma derivação normal, ou diz emos que Π
1
está na forma
normal, e se Π ≥ Π
onde Π
é norma l, então d izemos que Π é normaliza do a
Π
.
Dizemos que > possui a propriedade de normalização forte se > não existe
uma seqüência infinita de reduções. E > possui a propriedade d e normalização fraca
se qualquer derivação puder ser normalizada.
Temos que:
Teorema 2.6 (Normalização fraca) Toda derivação em lógica clássica pode ser
normalizad a.
Definição 2.7 Um ramo em uma derivação π é uma seqüência α
1
, . . . , α
n
de
ocorrências de fórmulas tal que:
i) α
1
é uma hipótese;
ii) se α
i
não é uma premissa menor de → E nem a fórmula final de π, então
α
i+1
é a fór m ula que ocorre imediatamente abaixo de α
i
;
iii) α
n
é premis sa menor de uma aplicação de → E ou a fórmula fin al da
dedução.
O teorema a seguir é uma conseqüência imediata do teorema de normalização.
Teorema 2.8 Se π é uma derivação normal e β = A
1
, . . . , A
n
um ramo de π, então
temos:
i) Uma parte de eliminação de β (possivelmente vazia) A
1
, . . . , A
i−1
na qual
toda fórmula é premissa maior d e um a regra de eliminação e contém a
fórmula imediatamente sucedente como subfórmula;
ii) uma parte mínima A
i
de β que é conseqüência de uma regra de eliminação,
se i = 1, e premis sa de uma regra de int rodução ou de ⊥
c
, se i = n;
iii) Uma parte de introdução de β (possivelment e vazi a) A
i+1
, . . . , A
n
na qual
toda fórmu la é consequência de uma aplicação de uma regra de introdução
e contém a fórmula imediatament e precedente como sua subfórmula.
Teorema 2.9 (Princípio de Subfórmulas) Toda ocorrência de uma fórmula em
uma dedução normal de A a partir de Γ é subfó rmula de A ou de alguma
fórmula de Σ, com exceção das hipóteses descarregadas por aplicações d e ⊥
c
e
das ocorrências de ⊥, que estão imedia tamente abaixo de tais h ipóteses.
PUC-Rio - Certificação Digital Nº 0220933/CA
Capítulo 2. Preliminares 17
2.2
Classes hierárquicas e problemas lógicos
Para facilitar a compreensão e tornar motivante o estudo de sistemas de provas
proposicionais, vamos fazer uma revisão de algumas das teorias de P e NP .
Por convenção, P denota a class e de conjuntos de str ings reconhecida por
uma máquina de Turing determi nística em tempo limitado por um polinômio no
tamanho da entrada. N P é o mesmo p ara máquinas de Turing não determinísticas.
Se T AUT denotar o conjunto de tautologias sobre qualquer conjunto fixo
adequado de conectivos, temos q ue P = NP se e somente se T AUT está em P
(Pap94).
Agora P = NP não s omente pode i mplicar a existência de alg o ritmos
relativamente rápidos para qualquer algoritmo i n teressante e aparentemente sem
solução em NP , como também pode ter uma conseqüência filosófica int eressant e
em matemática. Se P = NP , então existe um polinômio p e um algoritm o A com a
propriedade de que qualquer proposição S da teoria de conjuntos e q ualquer inteiro
n, A determina com apenas p(n) passos se S possui uma prova de tamanho n, ou
menor.
Para ver que a existência de A origina-se de P = NP , observe q ue o problema
solucionado por A est á em NP .
De fato, uma máquina de Turing não-det erminística pode escrever qualquer
string de tamanho n em sua fita e, então, verificar se a st ring é uma prova da
proposição dada. Para qualquer teoria lógica razoável , esta verificação pode ser
realizada em tempo limit ado por um polinômio em n. Assim, a importância de
mostrar que P = NP .
Outra importante questão decisiva está relacionada com o fato de NP ser
fechado ou não sobre complementação, i. e., Σ
∗
− L está em NP se L está em N P .
Se NP não é fechado sobre complementação, então claramente P = NP (Pap94).
Assim o seguinte resultado é importante:
Teorema 2.10 NP é fechado sob complementação se e somente se T AUT está em
NP .
Notação 2.11 L é o conjunto de funções f : Σ
∗
1
→ Σ
∗
2
, Σ
1
, Σ
2
, quaisqu er alfabeto
finito, tal que f pode ser computada por um máquina de Turing determin ística em
tempo limitado polinomialmente no tamanho da entrada.
Prova.(do teorema 2.10) O complemento do conjunto de taut ologias está em NP ,
uma vez que para verificar que a fórmula não é uma tautologia pode-se atribuir um
valor verdade e verificar que este falsifica a fórmula. Inversamente, suponha que o
conjunto d e tautologias está em NP . Como qualquer conjunto L em NP é reduzido
ao comp lemento das tautologias no sentido que existe um a função f em L tal que
PUC-Rio - Certificação Digital Nº 0220933/CA
Capítulo 2. Preliminares 18
para todas strings x, x ∈ L sse f (x) não é uma tautologia (vide (Pap94)). Assim, um
procedimento não determinístico para aceitar o complemento de L é: sob entrada
x, compu te f(x), e aceite x se f (x) é uma tautologia, usando o procedimento não
determinístico para tautologias assumido acima. Assim o complemento de L está
em NP .
Por convenção utiliza-se CoNP para representação do complemento de N P .
Desta forma o teorema 2.10 pode ser enunciado da seguinte forma:
Teorema 2.12 NP = CoNP se e somente se T AUT ∈ N P
A questão se T AUT está em NP é equivalente a de existir um sistema de
prova proposicional em qu e toda tautologia possu i uma prova curta, formalmente:
Definição 2.13 (Sistema de Prova) Seja L ⊆ Σ
∗
, um sistema de prova para L é
uma função f : Σ
∗
1
→ L para algum alfabeto Σ
1
e f em L t al que f é sobrejetiva.
Dizemos que o sistema de prova é limitado polinomialmente sse existe um
polinômio p(n) tal que para todo y ∈ L existe x ∈ Σ
∗
1
tal que y = f(x) e
|x| ≤ p(|y|), onde |z| denota o tamanho de uma string z.
Exemplo 2.14 (Sistema de prova proposicional) Para q ue a noção de sistema de
prova p roposicional (maiores detalhes são fornecidos em A.1) se encaixe com a
definição (2.13), pri mei ro devemos notar que a s fórmulas podem s er consideradas
como strings sobre um alfa beto finito.
O único p roblema é que uma variável proposi ci onal também deve s er consi-
derada como uma string de forma que exista um suprimento ilimitad o de variáveis
proposici onais.
Então uma p rova π no si stema proposicional que é uma seqüência de fórmu-
las, pode ser naturalmente considerada como uma string sobre um alfabeto finito
que i nclui a vírgul a como um símbolo separador bem como os símbolos necessários
para especificação das fórmulas.
A função f que abstratamente específica o sistema será dada por f (π) = A
se π provar A, e f(π) = A
0
para alguma tautologia fixa A
0
se π não é uma string
que corresponda a uma prova no sistema.
Teorema 2.15 Um conjunt o L está em NP sse L = ∅ ou L t em um sist ema de
provas limitado polinomialmente.
Prova. Se L ∈ N P , então alguma máquina de Turing não determinística M que
aceita L em temp o po linomial. Se L = ∅, definimos f t al que se x codifica a
computação de M q u e aceita y, então f(x) = y. Se x não codifica uma compu tação
que aceita, então f(x) = y
0
para algum y
0
∈ L fixo. Então f é claramente um
sistema de prova para L l imitado polinomialmente.
PUC-Rio - Certificação Digital Nº 0220933/CA
Capítulo 2. Preliminares 19
Para a volta, se f é um sistema de prova para L limitado po linomialmente,
então um algoritmo não-determinístico rápido para aceitar L é, sob entrada y,
atribua uma p rova curta x de y e verifique f(x) = y.
Podemos então i nferir a partir dos teoremas acima que NP é fechado sob
complementação se e somente se T AUT tiver um sistema de provas limitado
polinomi al mente.
Com o intuito de verificar se o s s istemas de provas convencionais são limita-
dos polinomialmente, Cook e Rechkow em (CR79) definiram classes de equivalên-
cias para sistemas de provas de forma que a resposta fosse a mesma para sistemas
equivalentes.
A relação de equivalência associada é a p-simulação.
Notação 2.16 L é o conjunto de funções f : Σ
∗
1
→ Σ
∗
2
, Σ
1
, Σ
2
qualquer alfabeto
finito, tal que f possa ser verificada por uma máquina de Turing determinísti ca em
tempo limitado por um polinômio no tamanho da entrada.
Existem duas no ções mais comuns de comprimento de prova. A primeira é
o número de linhas que aparecem em uma prova, usualmente chamada número de
linhas ou número de inferências de uma prova.
A segunda é a noção de número d e símbolos aparecendo na prova e esta,
como já foi mencion ado no começo desta seção, será a medida que utilizaremos no
decorrer do texto.
Definição 2.17 Se f
1
: Σ
∗
1
→ L e f
2
: Σ
∗
2
→ L são sistemas de provas para L,
então f
2
p-simula f
1
se existir uma função g : Σ
∗
1
→ Σ
∗
2
tal que g está em L , e
f
2
(g(x)) = f
1
(x) para todo x.
Segue d a definição acima e da definição (2.13) que:
Teorema 2.18 Se um sistema de prova para L, f
2
, p-simula um outro sistema de
provas pa ra L, f
1
, limit ado polinomialment e então f
2
também é limit ado polinomi-
almente.
PUC-Rio - Certificação Digital Nº 0220933/CA
Capítulo 2. Preliminares 20
2.3
Sistemas de Frege
Nesta seção definiremos sistemas de Frege, sistemas de Frege com subs titui-
ção e sistemas de Frege estendidos. Alguns resultados envolvendo sistemas de Frege
e p-simulação também serão apresentaados. Maiores informações são apresentadas
no apêndice A.
Definição 2.19 Um sistema de Frege, F, é definido por um conjunto completo
de conectivos proposicionais, tendo um conjunto finito de regras de inferência
esquematicamente definido. O sistema admite modus ponens como uma regra
derivada e precis a s er completo e consistente.
Um sistema de Frege com Substituição, SF, é definido por adici onar a F a
seguinte regra d e substituição
A(p)
A(B)
onde simultâneas substituições da fórmu la B são permitidas para a variável p.
Definição 2.20 (Sistema de Frege estendido) ,
Um sistem a de Frege estendido, e-F , é ob tido por adicionar a F a seguinte
regra:
p ↔ A
onde A é qualquer fórmula e p é uma variá vel que não ocorre nem A nem em
qualquer regra de extensão usada na prova e nem na fórmu la final da prova.
A idéia da regra de extensão é permitir que a variável p aja como uma
abreviação pa ra a fórmula A.
Teorema 2.21 Um sistema de Frege estendido é limitado polinomialmente se e
somente se todos os sistemas de Frege estendidos sob todos os conj untos de
conectivos forem l imitados polinomialmente. Além disso, um sistema de Frege
estendido é po linomialmente limitado se e somente se existir um limi te polinomial
sob o número de l inhas nas provas em eF . Desta forma, se P = N P , então não
existe um limite polinomial sob o número de linhas em provas em sistemas de Frege
estendidos, sistemas de Frege ou sistema de Dedução Natural.
PUC-Rio - Certificação Digital Nº 0220933/CA
Capítulo 2. Preliminares 21
2.4
Resolução
O sistem a de Resolução trabalha com variáveis proposicionais p
1
, p
2
. . . e suas
negações ¬p
1
, ¬p
2
, . . . e n ão tem nenhum outro conectivo lógico, ou s ej a, κ = ∅.
O objeto b ásico em Resolução é uma cláusula, um conju nto finito de literais
(variáveis proposicionais ou variáveis proposicionais negadas). Ou seja, uma linha
em resolução é um cláus ula.
Uma cláusula pode ser vista como uma disjunção de literais. Desta forma,
uma atribuição de verdade s at isfaz uma cláusula C se e somente se satisfizer pelo
menos um literal de C. A Regra de resolução nos p erm ite derivar novas cláusulas
C
1
∪ C
2
de duas cláusulas C
1
∪ {p} e C
2
∪ {¬p}
C
1
∪ {p} C
2
∪ {¬p}
C
1
∪ C
2
Não existem restrições so b ocorrências de literais p, ¬p em C
1
ou C
2
. Uma
propriedade óbvia de resolução é que, se uma atribuição de verdade satisfaz as duas
cláusulas superiores da regra, então ela também satisfaz a cláusula inferior.
Uma refutação em resolução de um conjunto de cláusulas C = {C
1
, . . . , C
n
}
é uma seqüência de cláusu la D
1
, . . . , D
t
tal qu e cada D
i
é ou um elemento de C ou
é derivado por regra de reso lução de alguns D
u
, D
v
, u, v < i anteriores, e tal que a
última cláusula é a cláusula vazia.
Teorema 2.22 Um conjunto de cláus ulas é insatisf atível: isto é, não existe ne-
nhuma atribuição de verdade q ue simultaneam ente sati sfaça to das as cláusulas no
conjunto, se e soment e se existir uma refutação em resolução do conjunto.
2.5
Princípio das Casas dos Pombos-PHP
Tautologias expressando versões d o p rincípio das casas dos pom bos têm sido
importantes casos usados para teste com o in tuito de obter limites no compri mento
de provas proposicio n ai s e de comparar o poder de prova dos vários sistemas
proposicionais.
O primei ro artigo de Cook e Rechkow (CR79) mostrou que o princípio das
casas dos pombos possui p rova de tamanho polinomial em sist emas de Frege
estendido. Buss em (Bus87) mostrou que o princípio também poss ui uma prova
polinomi al em sistema de Frege.
Já Haken em (Hak85) m ostrou que uma refutação em resolução do princípio
das casas dos pombos requer um tamanho exponencial.
Apresentaremos, nesta seção, o prin cí pio das casas dos pombos proposicional
e um esquema das provas em F e e-F , uma vez que o utilizaremos nas próximas
seções para aplicar nosso resultado.
PUC-Rio - Certificação Digital Nº 0220933/CA
Capítulo 2. Preliminares 22
2.5.1
P HP
n
Para cada número natural n ≥ 1, seja P HP
n
a fórmu la proposicion al que
expressa que "se n + 1 pombos descansam em n casas então alguma casa contém
mais que um pombo". Formalmente, se [n] denota o conjunto {0, 1, . . . , n − 1}; se
f : [n + 1] → [n] então existem 0 ≤ i < j ≤ n t al que f (i) = f(j). Para expressar
proposicionalm ente uti lizaremos a variável proposicional p
i,j
significando f(i) = j
e definiremos P HP
n
pela fórmula.
n
i=0
n
j=0
p
i,j
→
0≤i<m≤n
n
j=0
(p
i,j
∧ p
m,j
)
O lado esquerdo da fórmula expressa que a função é total e o lado direito que a
função não é injetiva. Note que o tam anh o d e P HP
n
é proporcional a n
3
.
Uma p rova informal do princípio pode ser dada por um a indução sobre n. É
claro que o princíp io é verdadeiro para n = 2.
Em geral, se f : [n + 1] → [n], então seja f
: [n] → [n − 1] definida por
f
(i) =
f(i), se f (i = n − 1)
f(n), caso con trário
Se f é injetiva, é fácil verificar que f
também o é, contradizendo a hipótese de
indução.
Para formalizar esta prova em sistema de Frege estendi do e-F , usamos
novas variáveis p roposicionais q
k
i,j
para representar a asserção f
k
(i) = j. Isto é,
definiremos q
k
i,j
como segue:
q
k
i,j
↔ p
i,j
, 0 ≤ i ≤ n, 0 ≤ j < n,
q
n
i,j
↔ q
k+1
i,j
∨ (q
k+1
i,k
∧ q
k+1
k+1,j
), 0 ≤ i ≤ k, 0 ≤ j < k, 1 ≤ k < n.
Seja A
k
a fórmula proposicional
k
i=0
k
j=0
q
k
i,j
→
0≤i<m≤k
k
j=0
(q
k
i,j
∧ q
k
m,j
)
Fica claro que existe uma prova d e ¬P HP
n
→ ¬A
n
e ¬A
k+1
→ ¬A
k
para
todo 1 ≤ k < n em que cada prova possui tamanho O(n
6
). Este tamanho estimado
é obtido através da observação de que existe uma prova em e-F de ¬A
k+1
→ A
k
com O(n
3
) linhas e cada fórmula nesta prova tem tamanho O(n
3
).
Uma vez que existe uma prova em e-F de A
1
= q
1
0,0
∧ q
1
1,0
→ q
1
0,0
∧ q
1
1,0
.
Usando Modus Ponens n vezes p ara combinar as provas em e-F de ¬P HP
n
→
PUC-Rio - Certificação Digital Nº 0220933/CA
Capítulo 2. Preliminares 23
¬A
n
e ¬A
k+1
→ ¬A
k
obtemos uma prova em e-F de P HP
n
de tamanho O(n
7
).
Uma forma simp les de converter esta p rova em e-F para uma prova em
F é su bstituir cada variável p roposicional introduzida pela regra de extensão pela
fórmula que el a abrevia. A nova prova terá o mesmo n úmero de linhas. Entretanto,
o tamanho das fórmulas q
n
0,0
e q
1
1,0
apresentará um tamanho de ordem 3
n
. Assim, o
tamanho da prova em F será O(n
4
.3
n
).
Acreditava-se que o princípio das casas dos pombos seria um exemplo que
mostra a separação exponencial entre e-F e F . Entretanto, Buss em (Bus87)
provou que P HP
n
possui uma prova polinomial também em F .
Para mostrar este resultado Buss apresenta uma prova pol inomial em e-F de
PHP cujas regras de extensão, ao serem substi tuídas, geram uma prova em F que
continua sendo polin omial.
A estratégia, para a escolha das regras d e ext ensão, envolve vetor adição e
vetor contagem para circuitos de profundidade lo garítmica que aparecem em Ofman
(Ofmry) e Wallace(Wal64).
2.6
PHP em Resolução
Apresentaremos um resultado devido Haken, Buss e Turán (Kra95) no qual o
tamanho mínimo de uma refutação em resolução de ¬P HP é exponencial.
Se considerarmos as variáveis proposicionais p
ij
, i = 0, . . . , n ej =
0, . . . , n − 1 então ¬P HP
n
pode ser considerado como o conjunto de cláusulas
{¬p
ik
, ¬p
jk
}, para todo i = j e k
{p
i0
, . . . , p
i(n−1)
}, para todo i.
Teorema 2.23 Em qualqu er refutação em resolução do conjunto ¬P HP
n
existem
pelo menos 2
Ω(
n
2
m
)
cláusulas diferentes.
Como o p ri ncípio das casas dos pombos possui prova pol inomial tanto em
F quanto em e-F , concluímos que Resolução não é nem um sistema d e Frege e
nem um sistema de Frege estendido.
Uma vez que o sist ema de resol ução pode ser vist o como um cálculo de
sequentes com cortes de tamanho 1, tem os que o teorema acima nos reforça a idéia
de que a introdução de cortes de tamanho maior que 1 seria uma al ternativa para
reduzir o tamanho de provas proposicionais.
PUC-Rio - Certificação Digital Nº 0220933/CA
3
Método Horizontal
Este método u n ifica ramos em uma prova e, p o r meio de introduções de uma
nova regra de "atenuação", constrói uma prova menor da mesma conclusão.
Apresentaremos na primeira seção deste capítulo a definição de unificador,
o algoritmo de un ificação e exemplo de aplicação do alg oritmo em formulas
proposicionais.
Na segunda seção apresentaremos o método e na terceira formalizaremos o
método utilizando cálculo de seqüentes.
3.1
Definições
Definição 3.1 Uma substituição θ é denominada um unificador para o conjunto
{E
1
, . . . , E
k
} se e somente se E
1
θ = E
2
θ = · · · = E
k
θ. O conjunto {E
1
, . . . , E
k
}
é dito unificável se existe um unificador para el e.
Definição 3.2 O par em desacordo de um conjunto não vazio de expressões W
é obtido l ocalizando os primeiros símbolos (contando da esquerda) no qual nem
todos as expressões em W tem exatamente os mesmos símbolos, e então extraindo
de cada expressão em W a sub-expressão que começa com o símbolo o cup ando esta
posição. O conjunto desta respectivas sub-expressões é o conjunto em desacordo de
W .
Exemplo 3.3 Se W é {→ (→ (A
2
, A
3
), → (→ (A
1
, A
2
), → (A
1
, A
3
))); → (→
(A
1
, A
3
), → (→ (A
4
, A
1
), → (A
4
, A
3
)))}, ent ão as primeiras posições na qual
nem todas fórmulas em W são exatamente as m esmas é a quinta, uma vez q ue todas
fórmulas possuem os qua tro primeiros símbolos iguais → (→ (. Então o conjunto
em desacordo consiste das respectivas sub-expressões (termos sublinhados) que
começam na posição cinco, ou seja o conj u nto {A
2
, A
1
}.
Exemplo 3.4 Considere o conjun to W do exemplo 3.3.
1. σ
0
= e W
0
= W . Desde que W
0
não é unitário, σ
0
não é o unifi cad or de
W .
PUC-Rio - Certificação Digital Nº 0220933/CA
Capítulo 3. Método Horizontal 25
Algorithm 1 Algorit mo de Unificação adaptado por emparelhamento
1: k = 0, S
k
= S, P
k
= {} e σ
k
= {}.
2: Se S
k
é unitário, substitua as variáveis originais (remanescentes) de S p or novas
variáveis aplicando α
k
/(v
k
, v
k
) para cada variável original remanescente v
k
e
adicione α
k
/(v
k
, v
k
) a σ
k
; σ
k
é o unificador de S. Caso contrário, se S
k
não é
unitário, encontre o par em desacordo D
k
de S
k
.
3: Se existirem elementos v
k
e t
k
em D
k
tal que v
k
seja uma variável que não
ocorre t
k
, vá para o passo 4. Caso contrário, pare; S não é unificável.
4: Se D
k
/∈ S
k
, construa S
k+1
substituindo as ocorrências de D
k
em S
k
por α
k
,
onde α
k
é uma variável que não está presente nem S e nem S
k
. Caso contrário,
construa S
k+1
substituindo as ocorrências de D
k
em S
k
pelo α
k
previamente
associado. Faça S
k+1
= S
k
∪ D
k
5: Faça k = k + 1 e vá para o passo 2.
2. O par em desacordo D
0
= (A
2
, A
1
). Em D
0
, existe uma variável v
0
= A
2
que não ocorre em t
0
= A
1
.
3. D
0
/∈ σ
0
. Faça σ
1
= α
0
/(A
2
, A
1
).
S
1
={→ (→ (α
0
, A
3
), → (→ (A
1
, A
2
), → (A
1
, A
3
))),
→ (→ (α
0
, A
3
), → (→ (A
4
, A
1
), → (A
4
, A
3
)))}
e P
1
= {(A
2
, A
1
)}.
4. S
1
não é unitário e o par em desacordo de S
1
é:
D
1
= (A
1
, A
4
)
5. De D
1
, temos que v
1
= A
2
e t
1
= A
4
.
6. Como D
1
/∈ S
1
. Seja σ
2
= {α
0
/(A
2
, A)
1
), α
1
/(A
1
, A
4
)}.
S
1
={→ (→ (α
0
, A
3
), → (→ (α
1
, A
2
), → (A
1
, A
3
))),
→ (→ (α
0
, A
3
), → (→ (α
1
, A
1
), → (A
4
, A
3
)))}
e P
2
= {(A
2
, A
1
), ( A
1
, A
4
)}.
7. Uma vez que os próximos pares em desacordo já possuem um α
i
previamente
associado, geramos após doi s passos
σ
4
={α
0
/(A
2
, A)
1
), α
1
/(A
1
, A
4
)}
S
4
={→ (→ (α
0
, A
3
), → (→ (α
1
, α
0
), → (α
1
, A
3
))),
→ (→ (α
0
, A
3
), → (→ (α
1
, α
0
), → (α
1
, A
3
)))}
PUC-Rio - Certificação Digital Nº 0220933/CA
Capítulo 3. Método Horizontal 26
e P
4
= {(A
2
, A
1
), ( A
1
, A
4
)}.
S
4
é unitário e uma variável original que permanece é A
3
. Aplicando
α
2
/(A
3
, A
3
)
geramos
σ
5
= {α
0
/(A
2
, A)
1
), α
1
/(A
1
, A
4
), α
2
/(A
3
, A
3
)}
e
S
5
= {→ (→ (α
0
, α
2
), → (→ (α
1
, α
0
), → (α
1
, α
2
)))}
que contém a f órmula resultante do processo de uni ficação.
Teorema 3.5 Se S = {γ
1
, γ
2
} é um con junto com um par de fórmulas proposicio-
nais então o algo ritmo 1 sempre pára em tempo O(n), onde n = max{|γ
i
| ; γ
i
∈
S, i = 1, 2}.
Prova.
Primeiramente, provaremos que o algoritmo pára.
Suponha por absurdo que o algoritmo não pare.
Desta forma, seria gerada uma seqüência infinita Sσ
0
, Sσ
1
, Sσ
2
. . . de con-
juntos de fórmulas, finitos e não vazios com a propriedade que cada novo conjunto
contém uma variável original (remanescente) a menos que seu predecessor (por
exemplo, Sσ
k
contém v
k
enquanto Sσ
k+1
não contém).
Isto é impossível, pois S contém uma quantidade finita de variáveis.
Para provar a estimativa de tempo consumido pelo algori tmo, basta observar
que o algoritmo caminha simultaneamente po r γ
1
e γ
2
comparando os símbolos
de cada um das fórm ulas, substit uindo cada sí mbolo por uma nova variável e
armazenando informações em dois conjuntos, P
k
e σ
k
. Como o tempo para realizar
estas operações pode ser cons iderado O(1), temos que o algoritmo consumirá
n.O(1) = O(n).
3.2
O Método
Nosso método para reduzir o tamanho de uma prova durante o processo de
construção consiste em substituir duas fórmulas similares pela fórmula resultante
obtida pelo algoritmo 1.
Começamos construindo uma prova norm al de σ de baixo para cima usando
o conjunto de premissas Σ. Se durante a construção da p rova encontramos duas
fórmulas si milares, no sentido apresentado no algo ri tmo 1, construímos u ma prova
PUC-Rio - Certificação Digital Nº 0220933/CA
Capítulo 3. Método Horizontal 27
da fórmula resultante do algori tmo de unificação em vez de construir dois novos
ramos para cada uma das fórmulas similares.
Uma representação gráfica do método é apresentada na figura 3.1.
Γ
Π
1
α
1
Γ
Π
2
α
2
Σ
σ é transformada em
Γ
Π
α
Σ
σ
Figura 3.1: Representação g ráfica do método
Antes de apresentar o método em detalhes, vejamos como seria a sua aplica-
ção em um exemplo.
Exemplo 3.6 Considere a seguinte prova de uma adaptação do numeral de Church
(A
1
→ A
2
) → ((A
2
→ A
3
) → ((A
4
→ A
1
) → (A
4
→ A
3
))) (maiores detalhes
sobre a ad aptação do numeral de Church são apresent ados na a pêndice C).
[A
1
→ A
2
]
5
[A
2
→ A
3
]
4
[A
1
]
1
[A
1
→ A
2
]
2
A
2
[A
2
→ A
3
]
3
A
3
(A
1
→ A
3
)
1
(A
1
→ A
2
) → (A
1
→ A
3
)
2
(A
2
→ A
3
) → ((A
1
→ A
2
) → (A
1
→ A
3
))
3
(A
1
→ A
2
) → (A
1
→ A
3
)
(A
1
→ A
3
)
[A
4
]
6
[A
4
→ A
1
]
7
A
1
[A
1
→ A
3
]
8
A
3
(A
4
→ A
3
)
6
(A
4
→ A
1
) → (A
4
→ A
3
)
7
(A
1
→ A
3
) → ((A
4
→ A
1
) → (A
4
→ A
3
))
8
(A
4
→ A
1
) → (A
4
→ A
3
)
(A
2
→ A
3
) → ((A
4
→ A
1
) → (A
4
→ A
3
))
(A
1
→ A
2
) → ((A
2
→ A
3
) → ((A
4
→ A
1
) → (A
4
→ A
3
)))
Figura 3.2: Aplicação d o método vertical
Temos, pelo exemplo 3.4 que as fórmulas no final das áreas marcadas na
figura 3.2 são unificáveis com unificador
σ = {α
0
/(A
2
, A)
1
), α
1
/(A
1
, A
4
), α
2
/(A
3
, A
3
)}
e fórmula resultante
(α
0
→ α
2
) → ((α
1
→ α
0
) → (α
1
→ α
2
)).
O que faremos, então, será substi tuir as d uas derivações que estão marcadas
na figura por uma nova derivação.
[A
1
→ A
2
]
[A
2
→ A
3
]
(α
0
→ α
2
) → ((α
1
→ α
0
) → (α
1
→ α
2
))
(A
2
→ A
3
) → ((A
1
→ A
2
) → (A
1
→ A
3
))
σ
−1
1
(A
1
→ A
2
) → (A
1
→ A
3
)
(A
1
→ A
3
)
(α
0
→ α
2
) → ((α
1
→ α
0
) → (α
1
→ α
2
))
(A
1
→ A
3
) → ((A
4
→ A
1
) → (A
4
→ A
3
))
σ
−1
1
(A
4
→ A
1
) → (A
4
→ A
3
)
(A
2
→ A
3
) → ((A
4
→ A
1
) → (A
4
→ A
3
))
(A
1
→ A
2
) → ((A
2
→ A
3
) → ((A
4
→ A
1
) → (A
4
→ A
3
)))
PUC-Rio - Certificação Digital Nº 0220933/CA
Capítulo 3. Método Horizontal 28
onde a derivação de (α
0
→ α
2
) → ((α
1
→ α
0
) → (α
1
→ α
2
)) é apresentada
abaixo.
α
1
(α
1
→ α
0
)
α
0
(α
0
→ α
2
)
α
2
(α
1
→ α
2
)
(α
1
→ α
0
) → (α
1
→ α
2
)
(α
0
→ α
2
) → ((α
1
→ α
0
) → (α
1
→ α
2
))
Como dito no capít ulo 2, para que o sistema de dedução natural se encaixe
na definição de um sistema de Frege ele precisa ser visto como um grafo aciclico
direto, ou seja, u ma vez que uma fórmula é derivada em uma posição d a prova se
precisarmos novamente de tal fórmula não precisamos derivá-la outra vez. Desta
forma, a derivação de (α
0
→ α
2
) → ((α
1
→ α
0
) → (α
1
→ α
2
)) precisa s er
realizada apenas uma vez, com isso reduzimos o tamanho da prova.
Uma po ssível apresentação de uma prova em d edução natural com o um grafo
acíclico direto é obtid a se for utilizado o estilo devido a Fitch d e apresentação de
provas.
PUC-Rio - Certificação Digital Nº 0220933/CA
Capítulo 3. Método Horizontal 29
Exemplo 3.7 Utilizando o estil o Fitch para exibir a prova do exemplo 3 . 6.
1
α
1
hipótese
2 α
1
→ α
0
hipótese
3 α
0
1,2 →E
4 α
0
→ α
2
hipótese
5
α
2
2,3 →E
6 α
1
→ α
2
1, 5 →I
7
(α
1
→ α
0
) → (α
1
→ α
2
) 2, 6 →I
8 (α
0
→ α
2
) → ((α
1
→ α
0
) → (α
1
→ α
2
)) 4, 7 →I
9
(A
2
→ A
3
) → ((A
1
→ A
2
) → (A
1
→ A
3
)) 8, θ
1
10
(A
2
→ A
3
) hipótese
11
(A
1
→ A
2
) → (A
1
→ A
3
) 9, 10, → E
12
(A
1
→ A
2
) hipótese
13 (A
1
→ A
3
) 11, 12 →E
14
(A
1
→ A
3
) → ((A
4
→ A
1
) → (A
4
→ A
3
)) 8, θ
2
15
(A
4
→ A
1
) → (A
4
→ A
3
) 13, 14 →E
16
(A
2
→ A
3
) → ((A
4
→ A
1
) → (A
4
→ A
3
)) 10, 15 →I
A prova é apresentada em 3 colunas. Na primeira coluna existe uma numeração
que será ut ilizada como endereço da fórmula que é apresentada na seg unda coluna.
Na terceira coluna são in formadas a ori gem da fórmula da segunda coluna. Por
exemplo, a informação 1, 2, → E indica que a fórm ula presente na segunda coluna
foi obtida por → E usando as fó rmulas das linhas 1 e 2 como premissas.
Observe que a fórmula (α
0
→ α
2
) → ((α
1
→ α
0
) → (α
1
→ α
2
)) foi
utilizada como premissa para deduzir as fórmulas (A
2
→ A
3
) → ((A
1
→ A
2
) →
(A
1
→ A
3
)) e (A
1
→ A
3
) → ((A
4
→ A
1
) → (A
4
→ A
3
)). No entanto, só foi
necessário realizar u m a prova apenas de (α
0
→ α
2
) → ((α
1
→ α
0
) → (α
1
→
α
2
)).
3.3
Formalização do m étodo
No que segue, formalizaremos os conceitos v istos nesta introdução de seção.
PUC-Rio - Certificação Digital Nº 0220933/CA
Capítulo 3. Método Horizontal 30
A apresentação de uma dedução como um grafo acíclico direto, em vez de
apresentação como uma árvore, nos permite reduzir o tamanho da dedução, uma
vez que apagam os da dedução subdeduções repetidas.
O que o nosso método propõ e é eli minar não só os ramos idênticos, mas
também os ramos similares. No nosso caso, ramos similares são aqueles em que as
conclusões são unificáveis pelo algoritm o 1.
Voltando ao exemplo 3.6, observe que introduzimos uma nova regra, θE, que
aplica uma subst ituição à fórmula que é sua premissa. Isto é,
α
α
θE
onde α
é a fórmula resultante do processo de unificação de α
1
e α
2
utilizando o
algoritmo 1.
Ou seja, o ganho de redução d o tamanho da prova é obtid o por elimin ar, de
forma consistente, deduções d e fórmulas similares.
Devemos observar certas condições para garantir a consi stência neste n ovo
sistema de prova. Primeiro, precisamos garantir que a nova fórm ula obtida pelo
processo de unificação não possui variáveis utilizadas previamente na prova e
segundo não permiti r a un ificação de premissas que ainda serão ut ilizadas na prova.
O algoritmo de unificação gera uma fórmula que possui apenas variáveis
novas , o qu e atende a primeira cond ição.
O segundo cuidado deve ser t omado durante a construção da prova, preci-
samos verificar se as fórmulas que foram empregadas na prova de α
, serão des-
carregadas depois da conclusão. Isto é, devemos atentar para os ramos abertos da
derivação. No exemplo a seguir tratamos de um caso com esse p roblema.
Exemplo 3.8 Considere os dois trechos de prova a seguir.
[A
1
]
1
[A
1
→ A
2
]
2
A
2
A
2
→ A
3
A
3
(A
1
→ A
3
)
1
(A
1
→ A
2
) → (A
1
→ A
3
)
2
[A
4
]
1
[A
4
→ A
1
]
2
A
2
A
1
→ A
3
A
3
(A
4
→ A
3
)
1
(A
4
→ A
1
) → (A
4
→ A
3
)
2
Na segunda linha de cada dedução, contando de cima para baixo, aparecem
as fórmulas A
2
→ A
3
e A
1
→ A
3
que serão descarregadas mais abaixo na prova.
Se aplicarmos o algoritmo 1 às fórmulas (A
1
→ A
2
) → (A
1
→
A
3
) e (A
4
→ A
1
) → (A
4
→ A
3
), obtermos um u nificador θ =
{α
0
/(A
1
, A
4
), α
1
/(A
2
, A
1
), α
2
/(A
3
, A
3
)} e fórmula resultante do processo d e uni-
ficação α
= (α
0
→ α
1
) → (α
0
→ α
2
).
PUC-Rio - Certificação Digital Nº 0220933/CA
Capítulo 3. Método Horizontal 31
Para realizar o processo de unificação de derivações de prova é preciso
também aplicar θ as hipóteses não descarregadas. Fa zendo isto, geramos o segui nte
trecho de prova:
[α
1
]
1
[α
1
→ α
1
]
2
α
1
α
1
→ α
2
α
2
(α
0
→ α
2
)
1
(α
0
→ α
1
) → (α
0
→ α
2
)
2
A fórmula α
1
→ α
2
ainda deve ser descarregada e convertida para sua
fórmula original , pois no restante da prova tal fórmula não aparece.
Isto é, devemos descarregar a hipótese (α
1
→ α
2
) como premissa de → I
aplicar θ
1
E e depois eliminar (A
2
→ A
3
) por → E. Ou seja , fazemos uso de um
"corte", como pode ser visto abaixo:
(A
2
→ A
3
)
[α
1
]
1
[α
1
→ α
1
]
2
α
1
[α
1
→ α
2
]
∗
α
2
(α
0
→ α
2
)
1
(α
0
→ α
1
) → (α
0
→ α
2
)
2
(α
1
→ α
2
) → ((α
0
→ α
1
) → (α
0
→ α
2
))
→ I
∗
(A
2
→ A
3
) → ((A
1
→ A
2
) → (A
1
→ A
3
))
θ
1
E
(A
1
→ A
2
) → (A
1
→ A
3
)
→ E
O exemplo acima explica como devemos interpretar as traduções de hipóteses
não descarregadas qu and o trabalhamos no sistema de dedução natural. Durante o
processo de construção da prova, este "corte"se torna desnecessário.
Como a construção de provas em dedução natural com controle de hipóteses
a serem utilizadas é quase o mesmo que construir provas em cálculo de seqüentes
(vide (Hae90)) optamos por apresentar este formalismo em um cálculo de s eqü entes
simplificado, SEQ
0
devido a Schütt e (Sch50).
3.3.1
O sistema SEQ
0
Apresentaremos nesta seção u m sist ema simpli ficado de cálculo de seqüentes,
SEQ
0
. Estes tipos de sistemas também são conhecidos por seqüentes de um lado
(One-Side sequent ) p ois as in fo rmações de cada linha de uma derivação são
colocadas apenas n o lado direito da fórmula. Por este motivo se torna desnecessário
o uso do símbolo separador (ou ⇒) na apresentação do cálculo.
PUC-Rio - Certificação Digital Nº 0220933/CA
Capítulo 3. Método Horizontal 32
Linguagem SEQ
0
(Forma de Schütte-Rasiowa-Sikorski)
Variáveis: v
0
, v
1
, . . . , v
i
Literais: x ou ¬x.
Fórmulas: Construídas a partir dos literais usando dois conectivos, ∨ e ∧.
Seqüentes: Conjunto finito de fórmulas (em particular qualq uer fórmula α é um
sequente {α} ). Em geral seqüentes são apresentados como listas de fórmulas,
i.e., Γ = α
1
, α
2
, . . . , α
k
para significar {α
1
, α
2
, . . . , α
k
}.
Regras
1. Axiomas Γ, α, ¬α
2.
Γ, α, β
Γ, α ∨ β
Regra ∨
3.
Γ, α Γ, β
Γ, α ∧ β
Regra ∧
4.
Γ
Γ, α
W
5.
Γ, α, α
Γ, α
C
¬α é definido por indução usando as regras de De Morgan:
1. ¬x := ¬x
2. ¬¬x := x
3. ¬(α ∨ β) := ¬α ∧ ¬β
4. ¬(α ∧ β) := ¬α ∨ ¬β
3.3.2
Dedução estruturada como árvore vs. dedução estruturada como cir-
cuito em SEQ
0
Dedução estruturada como árvore
Definição 3.9 Seja Γ qu alquer seqüente em SEQ
0
. Uma dedução de Γ estruturada
como árvore é um a árvore cujo vértice mais abaixo (=raiz) é Γ, e os vértices mais
acima (=folhas) são axi omas, e exceto pelas folhas cada vértice é a conclusão de
uma instância de uma regras de inf erência em SEQ
0
cujas premissas estã o logo
acima da conclusão. O peso e a altura da dedução estruturada como árvore é o
número total de vértices e o comprimento do caminho máximo, respectivamente.
PUC-Rio - Certificação Digital Nº 0220933/CA
Capítulo 3. Método Horizontal 33
Dedução estruturada como circuitos
Definição 3.10 Uma dedução de Γ estruturada como circuito é um circui to finito,
i.e. um grafo acíclico direto , satisfazendo t odas condições da definição anterior; o
peso e a altu ra são definidos como no caso de dedução estruturada como árvore.
Obviamente, tod a dedução estr uturada como árvore é uma dedução estrut u-
rada como circuito.
3.3.3
Regras auxiliares de inferência em SEQ
0
Corte
A regra do corte é uma inferência da forma
Γ, C Γ, ¬C
Γ
como circuito
Γ, C
Γ, ¬C
Γ
para um fórmula arbitrária C.
Inversões válidas em SEQ
0
.
Para qualquer s eqü ente em SEQ
0
definimos suas inversões válidas pelas
seguintes cláusulas recursivas.
1. Γ, F e Γ, G são inversões válidas de Γ, F ∧ G.
2. Γ, F, G é inversão válida de Γ, F ∨ G.
Atenuação por substituição em SEQ
0
.
A regra de atenuação por substituição, W S, e a regra de atenuação por subs-
tituição inversa, W IS, em SEQ
0
são as seguintes inferências, respectivamente:
Γ
θ(Γ), Σ
e
Γ
θ(Γ
−
), Σ
como circuito
Γ θ(Γ), Σ e Γ θ(Γ
−
), Σ
para quaisquer Γ, Σ, inversão válida Γ
−
de Γ em SEQ
0
, e qual quer θ : Variáveis →
Variáveis.
PUC-Rio - Certificação Digital Nº 0220933/CA
Capítulo 3. Método Horizontal 34
Teorema 3.11 Para qualquer seqüente proposicional Γ = F
1
, . . . , F
k
, a fórmula
F
1
∨ · · · ∨ F
k
é válida em lógica p roposicional se, e somente, se:
1. Γ tem uma dedução estruturada como árvore em SEQ
0
,
2. Γ tem uma dedução estruturada como circuito em SEQ
0
.
Em particula r, qualquer fórmula propo sicional F é vál ida em lógica propo-
sicional se, e somente, se, exi stir uma dedução em SEQ
0
e se, e somente, se existir
uma dedução estruturada como circuito em SEQ
0
.
Prova. O ítem 1 é bem conhecido. O item 2 é facilmente deduzido de 1.
Teorema 3.12 A regra do corte é válida em SEQ
0
. Isto é, se Γ, C e Γ, ¬C são
deduzidas em SEQ
0
então também o é Γ, tanto em como árvore quanto como
circuito. Assim, adicionar corte a SEQ
0
não estende o conjunto de seqüentes que
se podem deduzir, tanto como árvore quanto como circuito.
Prova. A prova segue diretamente do teorema 3.11.
Teorema 3.13 A regra atenuação por substituição inversa é válida em SEQ
0
.
Isto é, para quaisquer seqüentes Γ e Σ, qualquer substituição de variáveis θ e
qualquer inversão válida Γ
−
de Γ, se Γ é deduzida por uma dedução estrutu rada
como árvore (ou por dedução estruturada como circuito) em SEQ
0
, então também
é d edu zida como dedução estruturada como árvore (ou por dedução estrut urada
como circuito) Γ
−
,Σ.
Assim adicionar Corte e/ou adicionar WS e/ou adicionar WIS a SEQ
0
não
estende o conjunto de seqüentes que podem ser deduzidos em deduções estruturadas
como árvores (ou em dedução estru turada como circuitos )
Prova. Suponha qu e Γ = F
1
, . . . , F
k
é deduzida em SEQ
0
. Assim, pelo teo-
rema 3.11, F
1
∨ · · · ∨ F
k
é valida em lóg ica proposicional.
Agora, se Γ
−
= F
−
1
, . . . , F
−
l
é uma inversão válida de Γ, então F
−
1
∨· · ·∨F
−
l
também é uma fórmula válida. Ainda, como, po r definição, a validade de fórmulas
é preservada por atribuição de variáveis, temos que θ
F
−
1
∨· · ·∨θ
F
−
l
também é
válida, e obviamente também é válida qualquer atenuação θ
F
−
1
∨ · · · ∨ θ
F
−
l
∨
G
1
∨ · · · ∨ G
m
, onde Σ = G
1
, · · · , G
m
.
Disto e pelo teorema 3.11 obtemos a dedução de θ (Γ
−
),Σ.
PUC-Rio - Certificação Digital Nº 0220933/CA
Capítulo 3. Método Horizontal 35
3.3.4
O Método em SEQ
0
Nosso método para reduzir o tamanho de uma prova durante o processo de
construção da mesma, consi ste em subs tituir duas fórmulas simil ares pela fórmula
obtida pelo algoritmo 1.
Começamos construindo u ma prova norm al de α de baixo para cima usando
Γ como premissas. Em um certo ponto da prova encontramos du as fórmulas
unificáveis quando submetidas ao algoritmo 1. Construímos uma prova da fórmula
obtida no final do algoritmo em vez de construir dois novos ramos de prova um para
cada uma das fórmul as similares.
Uma representação gráfica do método horizontal em SEQ
0
pode ser vista na
figura 3.3.
D
1
Γ, α
1
D
2
Γ, α
2
.
.
.
Γ, α é transform ada em
D
Γ, α
Γ, α
1
Γ, α
2
WIS
.
.
.
Γ, α
i.e.
D
1
⇒ Γ, α
1
D
2
⇒ Γ, α
2
⇒ Γ, α é transformada em
D
⇒ Γ, α
Γ, α
1
Γ, α
2
⇒ Γ, α
Figura 3.3: Representação Gráfica do Méto do Horizontal
A regra W IS é a aplicação inversa do algorit mo 1, isto é, se duas fórmulas
α
1
e α
2
são unificáveis quanto sub metidas ao algoritmo 1 e a fórmula resultante do
processo de unificação é α
então
Γ, α
Γ, α
1
Γ, α
2
W IS
e
Γ, α
1
Γ, α
2
Γ, α
W S
3.3.5
Exemplo de aplicação: Nu merais de Church
Vejamos como o método se comporta em SEQ
0
. Aplicamos o método ao
exemplo 3.6, depois de convertê-lo a linguagem de SEQ
0
.
Modus Ponens
Em SEQ
0
, podemos inferir Γ, B de Γ , A e Γ, ¬A ∨ B.
Usaremos MP para abreviar o esquema apresent ado n a figura 3.4 .
PUC-Rio - Certificação Digital Nº 0220933/CA
Capítulo 3. Método Horizontal 36
Γ, A Γ, ¬A ∨ B
Γ, B
Figura 3.4: Modu s Ponens
Exemplo 3.14 Considere a prova de σ = (¬A
1
∨ A
2
) ∨ (¬(¬A
4
∨ A
3
) ∨ (¬(A
4
∨
A
1
) ∨ (¬A
4
∨ A
3
))) .
.
.
.
(¬A
1
∨ A
2
)
.
.
.
(¬A
2
∨ A
3
)
Π
2
F
2
¬(¬A
1
∨ A
2
) ∨ (¬A
1
∨ A
3
)
M P
(¬A
1
∨ A
3
)
M P
Π
1
F
1
¬(A
4
∨ A
1
) ∨ (¬A
4
∨ A
3
)
M P
¬(¬A
4
∨ A
3
), ¬(A
4
∨ A
1
) ∨ (¬A
4
∨ A
3
)
¬(¬A
4
∨ A
3
) ∨ (¬(A
4
∨ A
1
) ∨ (¬A
4
∨ A
3
))
(¬A
1
∨ A
2
), ¬(¬A
4
∨ A
3
) ∨ (¬(A
4
∨ A
1
) ∨ (¬A
4
∨ A
3
))
(¬A
1
∨ A
2
) ∨ (¬(¬A
4
∨ A
3
) ∨ (¬(A
4
∨ A
1
) ∨ (¬A
4
∨ A
3
)))
onde F
1
= ¬(¬A
1
∨ A
3
) ∨ (¬(¬A
4
∨ A
1
) ∨ (¬A
4
∨ A
3
)) e F
2
= ¬(¬A
2
∨ A
3
) ∨
(¬(¬A
1
∨ A
2
) ∨ (¬A
1
∨ A
3
)).
Π
1
é a seg uinte derivação:
A
4
.
.
.
¬A
4
∨ A
1
A
1
M P
.
.
.
¬A
1
∨ A
3
A
3
M P
¬A
4
, A
3
(¬A
4
∨ A
3
)
¬(¬A
4
∨ A
1
), ( ¬A
4
∨ A
3
)
¬(¬A
4
∨ A
1
) ∨ (¬A
4
∨ A
3
))
¬(¬A
1
∨ A
3
), ( ¬(¬A
4
∨ A
1
) ∨ (¬A
4
∨ A
3
))
¬(¬A
1
∨ A
3
) ∨ (¬(¬A
4
∨ A
1
) ∨ (¬A
4
∨ A
3
))
a derivação Π
2
é similar a derivação de Π
1
Aplicando o algorit mo 1 em F
1
= ¬(¬A
1
∨A
3
)∨(¬(¬A
4
∨A
1
)∨(¬A
4
∨A
3
))
e F
2
= ¬(¬A
2
∨ A
3
) ∨ (¬(¬A
1
∨ A
2
) ∨ (¬A
1
∨ A
3
)) temos que as duas fórmulas
são unificáveis.
O unificador é θ = {α
0
/(¬A
2
, ¬A
1
), α
1
/(¬A
1
, ¬A
4
), α
2
/(¬A
2
, ¬A
1
),
α
3
/(A
3
, A
3
)} e a fórmula resultante do processo de unificação é F
= ¬(α
0
∨ α
3
) ∨
(¬(α
1
∨ α
2
) ∨ (α
1
∨ α
3
)).
PUC-Rio - Certificação Digital Nº 0220933/CA
Capítulo 3. Método Horizontal 37
Seja Π
a derivação de F
. Temos que Π
é:
¬α
1
.
.
.
α
1
∨ α
0
α
0
.
.
.
¬α
0
∨ α
3
α
3
α
1
, α
3
(α
1
∨ α
3
)
¬(α
1
∨ α
2
), ( α
1
∨ α
3
)
¬(α
1
∨ α
2
) ∨ (α
1
∨ α
3
)
¬(α
0
∨ α
3
), ¬(α
1
∨ α
2
) ∨ (α
1
∨ α
3
)
a derivação é transformada em:
⇒ F
W IS
F
1
· · ·
F
2
¬(¬A
4
∨ A
1
) ∨ (¬A
4
∨ A
3
) ⇒ γ
3.3.6
Exemplo de aplicação: transitividade da implicação
Considere uma prova de a
1
→ a
2
k
a partir de um conjun to de hipó teses
{a
i
→ a
i+1
, i = 1, 2, . . . k − 1}. Isto é, a prova da tautologia (a
1
→ a
2
) → (a
2
→
a
3
) . . . (a
2
k−1
→ a
2
k
) → (a
1
→ a
2
k
). Onde 2
k
= 2
2
2
.
.
.
2
k .
Uma p rova normal desta fórmula p o ssui O(2
k
) linhas. Por outro lado, se
usamos a prova de (A → B) → (B → C) → (A → C) para tratar a transit ividade
de →, e se partirmos em duas cada conclusão intermediária, ist o é,
de a
1
→ a
2
k−1
e a
2
k−1
→ a
2
k
derivar a
1
→ a
2
k
de a
1
→ a
2
k−2
e a
2
k−2
→ a
2
k−1
derivar a
1
→ a
2
k−1
e o mesmo sendo aplicado as outras premissas de form a recursiva.
Teremos assim uma prova linear da fórmula apresentada inicialmente.
PUC-Rio - Certificação Digital Nº 0220933/CA
Capítulo 3. Método Horizontal 38
Π
S
3
= (A → B) → (B → C) → (A → C)
S
S
S
S
iv
S
v
S
vi
(a
1
→ a
4
) → (a
4
→ a
8
) → (a
1
→ a
8
)
Figura 3.5: Esb oço da redução da transitividade para (a
1
→ a
4
) → (a
4
→ a
8
) →
(a
1
→ a
8
)
Transitividade em SEQ
0
Seja Γ
2
n
uma representação em SEQ
0
da fórmula acima.
Γ
2
n
:= ¬a
1
, a
1
∧ ¬a
2
, a
2
∧ ¬a
3
, . . . , a
2
n
−1
∧ ¬a
2
n
, a
2
n
Uma prova de Γ
2
n
em SEQ
0
+ W S teria o seguinte aspecto:
Γ
2
k−1
, Π ∆, Γ
∗
2
k−1
Γ
2
k
onde
Γ
∗
2
k−1
= ¬a
2
k−1
+1
, a
2
k−1
+1
∧ ¬a
2
k−1
+2
, a
2
k−1
+2
∧ ¬a
2
k−1
+3
, . . . , a
2
k
−1
∧ ¬a
2
k
, a
2
k
.
Onde Γ
∗
2
k−1
= θ(Γ
2
k−1
) e θ é a seguinte substituição:
θ(a
i
) = a
2
k−1
+i
.
Aplicando o processo de substituição recursivamente em Γ
2
k−1
, Γ
2
k−2
, . . .
obtemos a redução desejada também em SEQ
0
+ W S.
3.3.7
Aplicação em PHP
O princípio das casas de p ombos seria um bom candidat o para se aplicar um
processo de elim inação de ramos semelhantes na prova. Isto é, PHP seria um bom
candidato para se trabalhar com SEQ
0
+ W S.
Finger em (Fin05) apresenta uma prova pol inomial do princíp io da casas
dos pombos como grafo acíclico direcionado (DAG) em Tableaux que podem
PUC-Rio - Certificação Digital Nº 0220933/CA
Capítulo 3. Método Horizontal 39
ser facilmente traduzidas para SEQ
0
+ W S (sem corte). Contudo, a con strução
proposta por Finger faz u so de substituições não triviais (i.e s u bstituições qu e
exigem a in tervenção do usuário).
Em suma, é po ssível produzir uma prova polinomial de PHP em SEQ
0
+W S.
Mas, analisando os trabalhos de Cook (Coo76) e Finger (Fin05) e as características
de uma prova de PHP, temos fortes indícios para crer que as substituições necessá-
rias para produzir uma prova curta dependeriam da intervenção d o usuário.
Como a nossa intenção é apresentar méto dos qu e não dependam da interven-
ção do usuário preferimos omitir a apresentação da tradução para SEQ
0
+ W S do
exemplo apresentado por Finger.
3.4
Conclusão do método
O método apresentado nesta seção atende os requisitos propos tos na introdu-
ção da presente tese. Senão, vejamos:
– O método pode ser aplicado durante o processo de con strução da prova.
Esta característica é de fundamental i mportância, uma vez que pretendemos
utilizar este método em provadores automáticos de teorema.
– O mét odo é de fácil implementação. Um algoritmo é fornecido para o caso
em que a substituição seja um renomeamento de variáveis.
– O método é correto e completo. Como mostrado no teorema 3.13 a adição das
regras W S e W IS n ão alteram o poder de SEQ
0
que é completo e correto.
Algumas melhorias naturais que podem ser acrescentadas ao método, que
serão temas para trabalhos futu ros, são:
– Apresentar uma maneira eficaz de buscar por pares de fórmulas semelhantes
durante a const rução do grafo de prova.
Não abordamos na tese qual a melhor forma de buscar as possíveis fórmulas
semelhantes na prova. Mostramos q u e, uma vez encontradas tais fórmulas
semelhantes o processo de produzir o unificante consumiria um tempo linear.
Apesar de não apresentarmos u m processo de bu sca por fórmulas em um
grafo acíclico, temo s fortes indícios de que os recursos con sumidos na busca
seria compensado pelo redução de recursos necessários para a construção da
prova.
– Estender o método para lógica de predicados.
Todo s os resultados apresentados para SEQ
0
são estend idos para SEQ, a
versão predicativa de SEQ
0
. Precisamos trabalhar num algoritmo de unifica-
ção que produza um substituição θ : vari áveis → termos.
PUC-Rio - Certificação Digital Nº 0220933/CA
4
Método Vertical
Neste capítulo, apresentamos o método vertical para redução do tamanho de
uma prova proposicional. Resumidament e, este método procura po r similaridades
na prova e as substitu i por uma nova variável que não aparece na prova.
O que queremos dizer por simi laridades e, como ident ificá-las, é assu nto da
primeira seção deste capítulo.
Na segunda seção, apresentamos o método. Na terceira seção apresentamos o
resultado principal do capítulo.
Na quarta seção apresentamo s uma alternativa para apli car este método a
provas combinatori ai s.
4.1
Definições
Definição 4.1 (Fórmulas U-similares) Dizemos que duas fórmulas proposicio-
nais, H
1
e H
2
onde V (H
1
) ⊆ V (H
2
), são U-similares se e somente se
1. |H
1
| = 1 (ou |H
2
| = 1). Neste caso, dizemos que o conj unto de U-axiomas
de H
1
e H
2
é o conjunto unitár io {H
1
↔ H
2
}, e
2. H
1
= h
1
1
h
1
2
e H
2
= h
2
1
h
2
2
com ≡ , h
1
1
é U-similar a h
2
1
(ou h
1
2
é
U-similar a h
2
2
).Neste caso o conjunto de U-axiomas de H
1
e H
2
é o conjunto
U
1
∪ U
2
onde U
1
é o conjunto de U -axiomas de h
1
1
e h
2
1
e U
2
é o conjunto de
U-axiomas de h
1
2
e h
2
2
.
Observação 4.2 1. Note que não consideramos o conectivo unári o ¬ n a defini-
ção acima. Este conectivo receberá uma atenção especial futuramente.
2. Se H
1
e H
2
são U-similares, então os primeiro s k conectivos biná rios das
duas fórmulas são ig uais.
3. Não necessariamente |H
1
| = |H
2
|.
4. Sem perd a de generalidade, consideraremos que o la do esquerdo de cada
elemento do conjunto de U-axioma s é atô mico.
PUC-Rio - Certificação Digital Nº 0220933/CA
Capítulo 4. Método Vertical 41
Definição 4.3 (Grau de U-axioma) Seja U = {h
1
, . . . , h
n
} o conjunto de U-
axiomas de H
1
e H
2
. Definimos o grau de U , denotado por deg(U), p or
deg(U) = |1 − min{|h
1
|; i ∈ 1 . . . n}|
Exemplo 4.4 Considere as seguintes fórmulas pro posicionais H
1
e H
2
.
H
1
=
(p
00
∧ p
10
) ∨ (p
00
∧ p
20
) ∨ (p
00
∧ p
30
) ∨ (p
01
∧ p
11
) ∨ (p
01
∧ p
21
) ∨ (p
01
∧ p
31
) ∨
(p
02
∧ p
12
) ∨ (p
02
∧ p
22
) ∨ (p
02
∧ p
32
) ∨ (p
10
∧ p
20
) ∨ (p
10
∧ p
30
) ∨ (p
11
∧ p
21
) ∨
(p
11
∧ p
31
) ∨ (p
12
∧ p
22
) ∨ (p
13
∧ p
32
) ∨ (p
20
∧ p
30
) ∨ (p
21
∧ p
31
) ∨ (p
22
∧ p
32
)
H
2
={[(p
00
∨ (p
02
∧ p
20
)) ∧ (p
10
∨ (p
12
∧ p
20
))]∨
[(p
00
∨ (p
02
∧ p
20
)) ∧ (p
20
∨ (p
22
∧ p
20
))]∨
[(p
01
∨ (p
02
∧ p
21
)) ∧ (p
11
∨ (p
12
∧ p
21
))]∨
[(p
00
∨ (p
02
∧ p
20
)) ∧ (p
10
∨ (p
12
∧ p
20
))]∨
[(p
10
∨ (p
12
∧ p
20
)) ∧ (p
20
∨ (p
22
∧ p
20
))]∨
[(p
11
∨ (p
12
∧ p
21
)) ∧ (p
21
∨ (p
22
∧ p
21
))]}
Temos que p
00
é U-similar a p
00
∨(p
02
∧p
20
), p
10
é U-similar a p
10
∨(p
12
∧p
20
)
e assim por di ante. O conjunto de U-axioma s é:
U = {p
00
↔ p
00
∨ (p
02
∧ p
20
), p
10
↔ p
10
∨ (p
12
∧ p
20
),
p
01
↔ p
01
∨ (p
02
∧ p
21
), p
11
↔ p
11
∨ (p
12
∧ p
21
),
p
20
↔ p
20
∨ (p
22
∧ p
20
), p
21
↔ p
21
∨ (p
22
∧ p
21
)}
Neste exemplo deg(U) = |1 − 4| = 3
Segue a definição de provas U-similares.
Definição 4.5 (Prova U -similar) Uma prova como a da figura 4.1 é dita U-similar
se e somente se H
1
e H
2
forem f órmulas U-similares.
PUC-Rio - Certificação Digital Nº 0220933/CA
Capítulo 4. Método Vertical 42
H
1
¬[H
2
]
1
.
.
.
.
⊥
H
2
1
⊥
c
Figura 4.1: Prova U-similar
4.2
Método
Considere uma prova U-similar onde H
2
é a premissa da ¬-introdução e H
1
é a hipót es e, como n a figura 4.1.
Nosso m ét odo de compactação segue os q uatro passos apresentados no algo-
ritmo 2.
Algorithm 2 Método Vertical
1: Encontre o conjunto de U -axiomas, U =
k
i=1
h
1
i
↔ h
2
i
, de H
1
e H
2
.
2: Substitua o lado esquerdo de cada elemento do conjunto de U-axio mas U
por uma nova variável, digamos q
i
, criando assim um novo conjunto U
=
k
i=1
q
i
↔ h
2
i
.
3: Substitua cada ocorrência de h
2
1
em H
2
pelo q
i
associado no passo ant erio r.
4: Construa uma nova prova similar à anterior apenas trocando o conjunto de
hipóteses H
2
pelo novo conjunto H
2
∪ U
.
Lema 4.6 (Lema de Compactação) Seja Π uma prova U -similar. Então p odemos
transformar Π em uma nova prova Π
tal que |Π| ≥ |Π
| + n.(r − 1), ond e r e n
são o grau do U-axioma presente e a quantidade de U -axiomas presentes em Π,
respectivamente.
Prova. Seja H
1
e H
2
fórmulas em Π que são U -simil ares.
Aplicando o algoritmo em H
1
e H
2
obtemos no terceiro passo uma nova prova
Π
onde n de fórmulas de tamanho menor que r s ão substituídas por uma nova
variável.
Portanto, teremos que |Π| − r.n ≥ |Π
|. Isto é, |Π| ≥ |Π
| + n(r − 1), como
desejávamos.
PUC-Rio - Certificação Digital Nº 0220933/CA
Capítulo 4. Método Vertical 43
4.3
Resultado Principal
Definição 4.7 Considere uma prova como na figura 4.2 tal que H
1
e H
2
formem um
par U-si m ilar que produza após aplicação do algoritmo 2 o conjun to de hipóteses
H
2
∪U
1
e que também H
2
e H
3
formem um par U-similar com conj unto de hipóteses
H
3
∪ U
2
produzido pelo algoritmo 2 e assim por diante, até que H
k
e H
k+1
formem
um par U -simila r com conjunto de hipóteses geradas pelo algoritmo 2 igual a
H
k
∪ U
k−1
.
Uma prova Π na qual é possível a aplicação de k U-similaridades encade-
adas é denominada u ma prova U-similar encadeada. O valor de k é denominado
a profundidade da prova U-similar encadeada e é denotada por depth(Π). Cada
conclusão de uma ¬-introdução é denominada o nível da prova U-similar encade-
ada. Os níveis da prova U-similar encadeada serão ordenados de cima para baixo
e serão denotados por 1,2,...,k.
¬[H
n
]
k
[H
n−1
]
1
.
.
.
.
⊥
¬H
n−1
1
[H
n−2
]
2
.
.
.
.
⊥
¬H
n−2
2
.
.
.
.
⊥
H
n
k
Figura 4.2: Esquem a de uma prova encadeada
Teorema 4.8 (Método Vertical Geral) Se Π é uma prova U-similar encadeada
com profund idade k entã o existe uma prova Π
com a mesma conclusão de Π tal
que |Π| ≥ |Π
| + n.k.r para algum r ∈ N e n a quan tidade de ocorrências de
U-axioma s em Π.
Prova. Seja r
i
dado por
r
i
= min{deg( U
i
)}
Mostraremos por indução em k que |Π| = |Π
k
| + n
k
i=1
r
i
. Onde Π
k
é a k-ésima
modificação de Π após aplicação de k U-simi laridades.
Base: Se k = 1, então estamos n a condição do lema 4.6 e portanto |Π| ≥
|Π
1
| + n.(r − 1).
PUC-Rio - Certificação Digital Nº 0220933/CA
Capítulo 4. Método Vertical 44
Passo indutivo: Se depth(Π) = k. Aplicando o lema 4.6 ao primeiro nível de Π
produzimos um novo ramo com um conjun to de hipóteses H
2
∪ U
1
e com
partes de algumas li nhas sendo reduzidas a uma variável.
Estendendo as substitu ições de variáveis ao rest ante d a prova obtemos uma
nova prova Π
1
tal que |Π
1
| ≥ |Π
1
| + n
1
.(r
1
− 1 ). Ond e n
1
é a quantidade de
ocorrências de U-axiomas no primeiro nível de Π e r
1
o grau do U-axio ma no
primeiro nível de Π.
Pela hipótese de indução aplicada a partir do segundo ní vel até o final da
prova Π
1
, obteremos uma n ova prova, digamos Π
k
tal que |Π
1
| ≥ |Π
k
| +
n
.
k−1
i=1
(r
i
− 1), onde n
é quantidade de ocorrências de U-axiomas em Π
1
e r
i
o grau do U-axiomas nos n íveis de 1 a k − 1.
Portanto, |Π| ≥ |Π
k
| + n
k
i=2
(r
i
− 1) + n
1
.(r
1
− 1).
Para r = 1 + min{r
i
, i = 1, . . . , k}, tem os que |Π| ≥ | Π
k
| + n.k.r, on d e
n =
k
i=1
n
i
Observe que se n
i
= n
i−1
.(r
i
− 1 ), isto é, se as aplicações de U-axiomas em
cada novo nível fossem realizadas em posições previamente modi ficadas por ou tro
U-axioma, teríamos que a nova prova Π
k
seria tal que:
|Π| ≥ |Π
k
| +
k
i=1
(r
i
− 1)
i
.n
k−i+1
Para r = 1 + min{r
i
, i = 1, . . . , k}, temos
|Π| ≥ |Π
k
| +
k
i=1
r
i
.n
k−i+1
Exemplo 4.9 Considere
P
n
=
0≤i<m≤n
n−1
j=0
(p
i,j
∧ p
m,j
)
P
n−1
=
0≤i<m≤n−1
n−2
j=0
(((p
i,j
∨ (p
i,n−1
∧ p
n−1,j
)) ∧ (p
m,j
∨ (p
m,n−1
∧ p
n−1,j
)))
P
n−2
=
0≤i<m≤n−2
n−3
j=0
(((p
i,j
∨ (p
i,n−1
∧ p
n−1,j
)) ∨ ((p
i,n−2
∨ (p
i,n−1
∧ p
n−1,j
) ∧ (p
n−2,j
∨ (p
n−2,n−1
∧
p
n−1,j
)))∧
(((p
m,j
∨(p
m,n−1
∧p
n−1,j
))∨((p
m,n−2
∨(p
m,n−1
∧p
n−1,j
)∧(p
n−2,j
∨(p
n−2,n−1
∧
p
n−1,j
)))
PUC-Rio - Certificação Digital Nº 0220933/CA
Capítulo 4. Método Vertical 45
No caso em que n = 3, teríamos:
P
3
=(p
00
∧ p
10
) ∨ (p
00
∧ p
20
) ∨ (p
00
∧ p
30
) ∨ (p
01
∧ p
11
) ∨ (p
01
∧ p
21
) ∨ (p
01
∧ p
31
)∨
(p
02
∧ p
12
) ∨ (p
02
∧ p
22
) ∨ (p
02
∧ p
32
) ∨ (p
10
∧ p
20
) ∨ (p
10
∧ p
30
) ∨ (p
11
∧ p
21
)∨
(p
11
∧ p
31
) ∨ (p
12
∧ p
22
) ∨ (p
13
∧ p
32
) ∨ (p
20
∧ p
30
) ∨ (p
21
∧ p
31
) ∨ (p
22
∧ p
32
)
P
2
=[(p
00
∨ (p
02
∧ p
20
)) ∧ (p
01
∨ (p
02
∧ p
21
))]∨
[(p
00
∨ (p
02
∧ p
20
)) ∧ (p
20
∨ (p
22
∧ p
20
))]∨
[(p
01
∨ (p
02
∧ p
21
)) ∧ (p
11
∨ (p
12
∧ p
21
))]∨
[(p
00
∨ (p
02
∧ p
20
)) ∧ (p
10
∨ (p
12
∧ p
20
))]∨
[(p
10
∨ (p
12
∧ p
20
)) ∧ (p
20
∨ (p
22
∧ p
20
))]∨
[(p
11
∨ (p
12
∧ p
21
)) ∧ (p
21
∨ (p
22
∧ p
21
))]
P
1
=(p
00
∨ (p
02
∧ p
20
)) ∨ ((p
01
∨ (p
02
∧ p
20
)) ∧ (p
10
∨ (p
12
∧ p
20
)))∧
(p
10
∨ (p
12
∧ p
20
)) ∨ ((p
11
∨ (p
12
∧ p
21
)) ∧ (p
10
∨ (p
12
∧ p
20
)))
Um trecho de prova com a seguinte estrutura:
¬P
3
[P
2
]
.
.
.
⊥
¬P
2
[P
1
]
.
.
.
⊥
¬P
1
.
.
.
P
3
É reduzida a seguinte prova:
¬P
3
[P
2
]
.
.
.
⊥
¬P
2
[P
1
]
.
.
.
⊥
¬P
1
.
.
.
P
3
PUC-Rio - Certificação Digital Nº 0220933/CA
Capítulo 4. Método Vertical 46
onde
P
2
= (q
1
00
∧q
1
01
)∨(q
1
00
∧q
1
20
)∨(q
1
01
∧q
1
11
)∨(q
1
00
∧q
1
10
)∨(q
1
10
∧q
1
20
)∨(q
1
11
∧q
1
21
),
P
1
= (q
1
00
∨ (q
1
01
∧ q
1
10
)) ∧ (q
1
10
∨ (q
1
11
∧ q
1
10
)) e
P
1
= (q
2
00
∧ q
2
10
).
4.4
Conclusão do capítulo
O méto do apresentado n este capítulo pode ser implementado e esta caracte-
rística atende um dos qu esitos que propusemos na introdução da t ese.
Infelizmente conseguimos uma redução satisfatória apenas para provas que
possuam aplicações encadeadas d o absurdo clássico, o que restringe muito a sua
utilização em um provador automático de teoremas.
A aplicação do método ao princípio das casas de pombos se mostra eficiente.
Contudo já se conhece um prova polino mial de tal princípio apresentada por Cook
em (Coo76) a qual serviu de guia para a construção do nosso método.
Apresentaremos a seguir uma alternativa para produzir provas curtas de
princípios combinatoriais. N esta proposta o processo de construção da regra de
extensão é feito por considerar combinações de elementos de uma matriz g erada
a partir de informações da fórmula que se deseja provar.
Uma vez que as informações necessárias estão presentes na fórmula que se
deseja provar, o processo de construção da regra de extensão p ode ser automatizado.
4.4.1
Uma alternativa curta para provas combinatoriais
Considere uma fórmula combinatorial da forma
P
n
≡
n
i=0
n−1
j=0
a
i,j
→ Φ (4-1)
onde Φ é qualquer fórmul a sobre os símbolos proposicionais a
ij
Uma forma de provar que P
n
é verdadeira é supor ¬P
n
e concluir ⊥, isto é,
provar que ¬P
n
→ ⊥
Devido a quanti dade d e ∨ presentes em P
n
, teríamos que fazer uso de muitas
regras ∨E o que tornaria a derivação d e ¬P
n
→ ⊥ bastante grande.
Se nos inspirarmos no trabalho de Cook (Coo76). Uma alternativa para
reduzir a quantidade ∨E seria tentar reduzir a prova de P
n
a u ma prova de P
n−1
usando axiomas auxiliares na forma de definições por extensão.
Apresentaremos a seguir um método para produzir provas curtas em Dedução
Natural de princípios combinatoriais com o o apresentado na fórmula 4-1.
PUC-Rio - Certificação Digital Nº 0220933/CA
Capítulo 4. Método Vertical 47
Pretendemos reduzir P
n
a P
n−1
preservando a propriedade descrita por a
ij
.
Faremos isso eliminando da representação de P
n
as fórmulas a
i,j
com i = 1, . . . , n,
j fixo e a
i,j
com j = 1, . . . , n − 1 e i fixo.
Se visualizarmos P
n
como uma matriz n×n−1, o que pretendemos é elimin ar
da matriz P
n
uma lin h a e u ma coluna. N a matriz abaixo optamos por elimi n ar a
última linha e a última coluna.
a
00
a
01
· · · a
0,n−2
a
0,n−1
a
10
a
11
· · · a
1,n−2
a
1,n−1
.
.
.
.
.
.
.
.
.
.
.
.
· · ·
a
n0
a
n1
· · · a
0,n−2
a
n,n−1
Os valores de b
ij
em P
n−1
serão herdados d os valores de P
n
da seguinte
maneira:
b
ij
= a
ij
∨ γ
Onde ¬Φ ∧ b
ij
deve deduzir ⊥.
Vejamos como est e procedimento se comporta na prova de P HP
n
.
P HP
n
com extensão
Lembrando que:
P HP
n
≡
n
i=0
n−1
j=0
p
i,j
→
0≤i<m≤n
n
j=0
(p
i,j
∧ p
m,j
)
Queremos mostrar que:
¬P HP
n
→ ⊥
E faremos isto aplicando reduções consecutivas, da seguinte forma,
¬P HP
n
→ ¬P HP
n−1
. . . ¬P HP
3
→ ¬P HP
2
≡ ¬((q
1
0,0
∧ q
1
1,0
) → (q
1
0,0
∧ q
1
1,0
))
obtidas através do uso da seguinte regra de extensão:
q
n
i,j
↔ p
i,j
, q
k
i,j
↔ q
k+1
i,j
∨ (q
k+1
i,k
∧ q
k+1
k+1,j
) (4-2)
Trabalhando com ¬P HP
n
da seguinte forma:
P HP
n
≡ (
n
i=0
n−1
j=0
p
i,j
) ∧ ¬(
0≤i<m≤n
n
j=0
(p
i,j
∧ p
m,j
))
PUC-Rio - Certificação Digital Nº 0220933/CA
Capítulo 4. Método Vertical 48
Temos que:
¬P HP
n
∧E
n
i=0
n−1
k=0
q
n
ik
======== ∧E
n−1
k=0
q
n
0k
¬P HP
n
∧E
n
i=0
n−1
k=0
q
n
ik
======== ∧E
n−1
k=0
q
n
1k
· · ·
¬P HP
n
∧E
n
i=0
n−1
k=0
q
n
ik
======== ∧E
n−1
k=0
q
n
n−1,k
Agora devemos aplicar as regras ∨E. Faremos a demonstração apenas para
uma parte do primei ro ramo acima. A construção dos demais ramos segue de forma
análoga.
[q
n
00
]
∨I
q
n
00
∨ (q
n
00
∧ q
n
00
)
ext
q
n−1
00
================= ∨I
n−2
k=0
q
n−1
ik
[q
n
01
]
∨I
q
n
01
∨ (q
n
00
∧ q
n
01
)
ext
q
n−1
01
================= ∨I
n−2
k=0
q
n−1
ik
· · ·
Obtemos P HP
n−1
a partir de P HP
n
utilizando a regra de extensão 4-2,
gerando:
¬P HP
n
∧E
n
^
i=0
n−1
_
k=0
q
n
ik
========== ∧ E
n−1
_
k=0
q
n
0k
[q
n
00
]
∨I
q
n
00
∨ (q
n
00
∧ q
n
00
)
ext
q
n−1
00
=================== ∨I
n−2
_
k=0
q
n−1
ik
[q
n
01
]
∨I
q
n
01
∨ (q
n
00
∧ q
n
01
)
ext
q
n−1
01
=================== ∨I
n−2
_
k=0
q
n−1
ik
· · ·
========================================================================= ∨E
n−1
^
i=0
n−2
_
k=0
q
n−1
ik
Agora, o l ado direito de P HP
n
:
¬P HP
n
∧E
¬
n−1
_
k=0
_
0≤i<j≤n
(q
n
ik
∧ q
n
jk
)
======================
n−1
^
k=0
^
0≤i<j≤n
¬(q
n
ik
∧ q
n
jk
)
∧E
^
0≤i<j≤n
¬(q
n
i0
∧ q
n
j0
)
∧E
¬(q
n
00
∧ q
n
10
)
============
(¬q
n
00
∨ ¬q
n
10
)
·
·
·
·
∨E + ext
¬(q
n−1
00
∧ q
n−1
10
)
·
·
·
·
∧E
^
0≤i<j≤n
¬(q
n
i0
∧ q
n
j0
)
∧E
¬(q
n
00
∧ q
n
20
)
============
(¬q
n
00
∨ ¬q
n
20
)
·
·
·
·
∨E + ext
¬(q
n−1
00
∧ q
n−1
20
)
·
·
·
·
∧E
^
0≤i<j≤n
¬(q
n
i0
∧ q
n
j0
)
∧E
¬(q
n
00
∧ q
n
30
)
============
(¬q
n
00
∨ ¬q
n
30
)
·
·
·
·
∨E + ext
¬(q
n−1
00
∧ q
n−1
30
) · · ·
============================================================================= ∧I
^
0≤i<j≤n−1
¬(q
n−1
i0
∧ q
n−1
j0
)
A construção da prova é feita de cima para baixo e sempre qu e possível devemos
introduzir a regra de extensão. Isto é, a medida que alg um dos elemento s do lado
direito de 4 -2 aparecem na derivação, devemos utilizar o regra de ∨I para gerar uma
prova que permit a o uso da regra de extensão.
PUC-Rio - Certificação Digital Nº 0220933/CA
5
Conclusão
Neste trabalho estudamos dois métodos que podem s er utili zados para com-
pactar provas lógicas. Em suma, o trabalho consi stiu em apresentar dois métodos de
compactação para provas proposicionais, que podem ser utilizados du rant e a cons-
trução da prova, para dois casos específicos.
O primeiro métod o apresentado, que se aplica a provas que possuem ramos
semelhantes, consegue reduzir o tamanho da prova quando elimina das provas es-
tes ramos semelhantes. A semelhança que tratamos nesta tese envolve basicamente
renomeamento de variáveis. Este método correspond e a introdução de fórmulas má-
ximas na prova, e tem garantida a di minuição de tamanho da prova quando a prova
é representada como um grafo acíclio direto conforme mostrado na seção 3.3.2,
em dedução natu ral a redução é alcançada quando a prova é representada usando o
estilo devido a Fitch.
O segundo método apresentado, que se aplica em provas com ⊥
c
encadeados,
reduz o tamanho da prova empregando axiomas de extensão.
As principais contribuições do trabalho são:
– Apresentamos métodos para reduções de provas proposicionais.
Sabemos que provas curtas são importantes tanto para Ciência da Com puta-
ção quanto para Teoria da Prova e muito pouco se sabe sobre como obtê-las e
o nosso trabalho apo nta alternativas neste sentido.
– Os métodos apresentados, são implementáveis e podem ser utilizados durante
a execução de um provador de teoremas sem a i ntervenção do usuário.
Os provadores aut o máticos de teoremas no rmalmente são feitos para realizar
provas normais (ou livres da regra do corte), po is fazem uso do princípio
de subfórmulas. Para permitir a inserção de cortes, o implementador deve
considerar uma grande quanti dade de alternativas em cada passo da prova o
que torna a implementação pouco eficiente.
Extensões naturais deste trabalho incluem:
– Um refinamento do método ho ri zon tal no que se refere a busca por fórmulas
semelhantes.
PUC-Rio - Certificação Digital Nº 0220933/CA
Capítulo 5. Conclusão 50
Isto implica o desenvolvimento de um algoritmo de busca em grafo acícli-
cos de provas. Na apresentação do método consideramos não-determinística
a escolha de fórmulas possivelmente semelhantes que seriam aplicadas ao
algoritmo 1. O não-determinis mo na escolha não nos permit e eliminar com-
pletamente a intervenção humana durante a construção da prova.
– A elaboração dos métodos para lógica de predicados.
Os resultados apresentados para SEQ
0
do método horizontal são natural-
mente estendidos para lógica de predicados SEQ. Como a grande dife-
rença de complexidade entre eliminação de corte prop osicional e elimin a-
ção d e corte em lógica de predicados é devida a repetições "desn ecessá-
rias" de instancias idênticas da regra do ∀. Tais instâncias são unificáveis
por substituições apropriadas, e assim equivalentes modulo W S. Portanto,
usar SEQ + W S pode reduzir sens ivelmente o peso da regra de eliminação
do corte.
– A implementação de um provador automáti co de teoremas que utilize os
métodos apresentados. Para comprovar o que foi apresentado teoricamente.
PUC-Rio - Certificação Digital Nº 0220933/CA
Referências Bibliográficas
[Bus87] Samuel R. Buss . Polynomial size proofs of the prop ositional pigeonh ole
principle. Journal o f Symbolic Logic, 52(4):916–9 27, December 1987.
2.5, 2.5.1, A.4
[Coo76] S.A. Cook. A short proof of the p igeon hole principle using extended
resolution. ACM SIGACT News, 8(4):28–32, 1976. 3.3.7, 4.4, 4.4.1
[CR79] S. A. Cook and R. A. Reckhow. The relative efficiency of propositi onal
proof systems. Journal of Symbolic Logic, 44 (1): 36–50, March 1 979. 1,
2.2, 2.5, A.2, A.4
[dPN01] Maria da Paz Nunes. Traduções via teoria da prova: aplicações à lógica
linear. PhD thesis, Pontifícia Universidade Católica do Rio de Janeiro,
2001. D
[Fin05] Marcelo Finger. Dag sequents with sub stitution. In Sergei N. Artëmov,
Howard Barringer, Art ur S. d’Avil a Garcez, Luís C. Lamb, and John Wo-
ods, editors , We Wil l Show Them! (1), pages 671–686. College Publicati-
ons, 2005. 3.3.7
[Hae90] Edward Hermann Haeusler. Prova Automática de Teoremas em Dedução
Natural: Uma a bordagem Abastrata. PhD thesis, Pontifícia Universidade
Católica do Rio de Janeiro, 1990. 3.3
[Hak85] A. Haken. The intractability o f resolut ion. Theoretical Computer Science,
39:297–308, 1985. 2.5
[Kra95] Jan Krají
ˇ
cek. Bounded arithmetic, prop ositional logic, and complexity
theory, volume 60 of Encyclopedia of Mathematics and its Applications.
Cambridge University Press, Cambridge, 1995 . 2.6
[Ofmry] Yu. Ofman. On the algorithmic complexity of discrete functions.
Sov. Phys., Dokl., 7(7): 589–591, 1963 , J anuary. 2.5. 1
[Pap94] C. H. Papadimitriou. Computational Complexity. Addison-Wesley, 1994.
2.2, 2.2
PUC-Rio - Certificação Digital Nº 0220933/CA
Referências Bibliográficas 52
[Pra65] Dag Prawitz. Natural Deduction, A Proof-Theoretical Study. Almqvist &
Wiksell, 1965 . 2
[Sch50] Kurt Schütte. Schluβweissen-Kalkül e der Praädikatenlogik. Mathematis-
che Annalen, 122:47–65, 1950. 3.3
[TS00] A. S. Troelstra and H. Schwichtenberg. Basic Proof Theory. Cambridge
University Press, Cambridge, England, 2 edition, 2000. 1
[vD97] Dirk van Dalen. Logic and Structu re. Springer-Verlag, Berlin, Germany,
2 edition , 1 9 97. 2.1.1
[Wal64] Wallace. A suggestion for a fast multiplier. IEEETC: IEEE Transactions
on Computers, 13, 1964. 2.5.1
PUC-Rio - Certificação Digital Nº 0220933/CA
A
Sistemas de Frege
Apresentaremos nesta seção os si stemas de Frege. Mostraremos também que
o sistema de dedução natural é um sistema de Frege.
Começaremos, assim, com a apresentação de notações e terminologias para
sistemas de provas proposicion ai s.
A.1
Sistemas de provas proposicionais
Considere κ um conjunto de conectivo s prop osicionais adequado, binários,
unários e zeroários. Adequado significa qu e toda função verdade pode ser expressa
por fórmulas con struídas da maneira usual a partir de variáveis proposicionais e
conectivos de κ, usando n otação infixa.
Se A
1
, . . . , A
n
, B são fórmulas, então escrevemos A
1
, . . . , A
n
|= B se B é
conseqüência lógica de A
1
, . . . , A
n
(i. e. toda atribuição de verdade sat isfazendo
A
1
, . . . , A
n
satisfaz B). Cada um dos sistemas de prova proposi ci o nal será definido
sob algum conjunto de conectivos κ, e será capaz de provar to das as tautologias
sobre κ por meio d e provas que utilizam as fórmulas construídas usand o κ.
Uma derivação em tal sistema é uma seqüência finita de linhas, terminando
na linha provada.
Uma linha é sem pre uma fórmula, exceto no caso de sis temas de dedução
natural (seção A.3). Cada linha deve ser uma hipótese ou seguir da linha anterior
por meio de regras de inferência.
Se a derivação não tiver hipó teses, ele é dita uma p rova.
Portanto, para especificar um sistema de prova p roposicional, são necessários
apenas a especificação κ, a definição de linh a e a existência de um conjunto finito
de regras de inferência.
Para que esta noção de sistema de prova se encaixe com a definição (2.13 ),
primeiro devemos notar que as fórmulas podem ser consid eradas como strings sobre
um alfabeto finito.
O único problema é que uma variável propo sicional também deve ser consi -
derada como uma string de forma que exista um suprimento ilimitado de variáveis
proposicionais.
PUC-Rio - Certificação Digital Nº 0220933/CA
Apêndice A. Sistemas de Frege 54
Então uma prova π no sistema proposicional que é uma seqüência de fór-
mulas, pode ser naturalmente considerada como uma string sobre um alfabeto finito
que inclui a vírgula como um s ímbolo separador bem como os símbolos n ecessários
para especificação das fórm ulas.
A função f q ue abstratamente específica o sistema será dada por f(π) = A
se π provar A, e f(π) = A
0
para alguma tautologia fixa A
0
se π não é uma string
que corresponda a uma prova no sistema.
A notação A
1
. . . , A
n
π
S
B significa que π é uma derivação de B a partir das
hipóteses A
1
, . . . , A
n
no sistema de p rovas S .
Notação A.1 Se L = (A
1
, . . . , A
k
) → A é uma linha, então o comprimento, l, de
L, é dado por l(L) = l(A
1
) + . . .+ l(A
k
) + l(A). Se π é u ma derivação, então λ(π)
é o número de linhas em π, e ρ(π) é o máximo de l(L), para toda L em π.
A.2
Sistemas de Frege
Temos, agora, condições de realizar a apresentação da definição de sistema de
Frege.
Muitos resultados d esta seção serão apresentados sem suas respectivas de-
monstrações.
Maiores detalhes pod em ser encontrados em, por exemplo, (CR79).
Definição A.2 Se D
1
, . . . , D
k
são fórmulas e P
1
, . . . , P
k
são variáveis proposicio-
nais distintas, então σ = (D
1
, . . . , D
k
)/(P
1
, . . . , P
k
) é uma substituição, e σA é a
fórmula resultan te da subs tituição de P
i
por D
i
, i = 1, ..., k, na f órmula A.
Uma regra de Frege é um sistema de fórmulas (C
1
, . . . , C
k
)/D, onde
C
1
, . . . , C
k
|= D. Se n = 0, a regra é um esquema de axioma. Para q ualquer
substituição σ dizemos que σD segue de σC
1
, . . . , σC
n
pela regra (C
1
, . . . , C
n
)/D.
Um sistema de inferência F é um conjunto finito de regras de Frege.
Fica evidenciado p el a definição d e regra de Frege que se A
1
, . . . , A
n
F
B
então A
1
, . . . , A
n
|=
F
B. Ou seja, um sistema d e Frege é um sistema de in ferência
implicacionalm ente completo.
Observação A.3 O sistema de Frege o riginal n ão encaixa na definição acima ,
porque ele possui a xi omas em vez de esquemas de axiomas, e explicitamente inclui
a regra de substituição. Se modificamos a definição original de Frege para a atual,
o resultado t erá conectivos κ = {¬, →}, a regra de inferência
A, A → B
B
e os seis esquemas de axiomas
PUC-Rio - Certificação Digital Nº 0220933/CA
Apêndice A. Sistemas de Frege 55
A → (B → A),
(C → (B → A)) → ((C → B) → (C → A)),
(D → (B → A)) → (B → (D → A)),
(B → A) → (¬A → ¬B),
¬¬A → A,
A → ¬¬A.
Teorema A.4 Para quaisquer dois sistemas de Frege F
1
e F
2
sob κ existe uma
função f em L e constante c tal que para todas fórmu las A
1
, . . . , A
n
, B e derivações
π, se A
1
, . . . , A
n
π
F
1
B então A
1
, . . . , A
n
f(π)
F
2
B, e λ(f(π)) ≤ cλ(π) e
ρ(f(π)) ≤ cρ(π)
Como conseqüência imediata do teorema acima e do teorema (2.18) podemos
dizer que:
Corolário A.5 Qu aisquer dois sistemas de Frege sob κ p-si m ulam um a o outro .
Assim um sistema de Frege sob κ é polinomialmente limitado se e somente se todos
sistemas de Frege sob κ forem.
A.3
Dedução Natural
Para o sistema proposicional de Prawitz se adequar à definição de sistema
de Frege, é imprescindível que a noção d e prova de Prawitz seja mais um grafo
acíclico di reto do que uma árvore. Isto é, uma vez que uma fórmula é derivada
de um con junto de hipóteses, não será necessário derivá-la novamente se ela for
utilizada uma outra vez.
Desta forma, apresentamos as provas em sistema de dedução natural como
seqüências de li nhas, e cada linha terá a forma A
1
, . . . , A
n
→ A, onde A
1
, . . . , A
n
são hipóteses que implicam A.
Definição A.6 Um linha de dedução natural é um par Γ → A, onde Γ é uma
seqüência fini ta de fórmulas , e A é uma fórmula. Se Γ é vazio, escrevemos s im-
plesmente → A.
Se ∆ é uma seqüência B
1
, .., B
n
de fó rmulas e L é a linha (A
1
, . . . , A
n
) → A,
então ∆L é a linha ( B
1
, . . . , B
2
, A
1
, . . . , A
n
) → A.
Se Λ é um conjunt o de linhas, ∆ é uma seqü ência de fórmulas e σ é uma
substituição, então Λ |= L i m plica que ∆σ(Λ) |= ∆σ(L), onde as operações ∆ e
σ são estendidas para conjuntos de linha s de forma natural.
PUC-Rio - Certificação Digital Nº 0220933/CA
Apêndice A. Sistemas de Frege 56
Se Λ é um conjunto finito de linhas e L é uma linha tal que Λ |= L, então o
sistema R = Λ/ L é uma regra de dedução natural.
A linha L
segue de Λ
pela regra R se para alguma subs tituição σ e seqüência
∆, Λ
= ∆σ(Λ), e L
= ∆σ(L).
Um sistema de dedução natural é u ma conjunto finito de regras de dedução
natural que é completo implicacio nalmente.
Notação A.7 Dada um linha L = (A
1
, . . . , A
m
) → A ass ociamos L a fórmula
L
∗
=
(¬A
1
, . . . , ¬A
m
, A). Se P é uma variável proposicional qualquer então
(P M)
∗
denota
(P, ¬A
1
, . . . , ¬A
m
, A).
Toda derivação em F , digamos B de A
1
, . . . , A
n
pode ser transformada
em uma derivação B de A
1
, . . . , A
n
em um sistema de dedução natural nd(F )
simplesmente adici onando o símbolo → à esquerda de todas as fórmulas na
derivação.
Inversamente, todo sistema de dedução nat u ral N pode ser transformado em
um sistema de Frege fr(N ), onde as regras de fr(N ) consis tem de duas regras
R
= Λ
∗
/L
∗
e R
= (P Λ)
∗
/(P L)
∗
para cada regra R = Λ/L de N .
Agora se π = L
1
, . . . , L
n
é qualquer derivação em N , então afirmamos que
π
∗
= L
∗
1
, . . . , L
∗
n
é uma derivação em f r(N ). Se L
i
segue do L
j
s anterior por
uma regra R = Λ/L em N . Então para alguma substituição σ e seqüência ∆.
L
∗
1
segue do L
∗
j
pela regra Frege R
= Λ
∗
/L
∗
por σ, desde que, para qualquer
linha M, (σ(M))
∗
= σ(M
∗
). Se ∆ não é vazio, então L
∗
i
segue do L
∗
j
pela
regra R
= (P Λ)
∗
/(P L)
∗
e substituição σ
, onde σ
é a substituição obtida
por aplicações simultâneas da substituição σ e
(¬A
1
, . . . , ¬A
k
)/P , onde ∆ é
A
1
, . . . , A
k
. Precisamos do fato que para qualquer linh a M sem ocorrências de P ,
σ
((P M)
∗
) = (∆σ(M))
∗
.
Portanto σ
∗
é uma derivação em f r(N ) para qualquer derivação π em N .
Note que desde que (→ A)
∗
= A, se π é uma derivação em N de B a partir de
A
1
, . . . , A
l
, então π
∗
é uma derivação em fr(N ) de B de A
1
, . . . , A
l
. Além di sso,
é p reciso n otar que λ(π
∗
) = λ(π) e ρ(π
∗
) ≤ cρ(π), o nde a constante c depende
apenas do conjunto de conectivos κ.
Temos então o seguinte teorema:
Teorema A.8 Dado os sistemas de dedução natural N
1
e N
2
sobre κ existe uma
função f em L e uma constante c tal que para todas l inhas L
1
, . . . , L
n
, L e
derivações π, se L
1
, . . . , L
n
π
N
1
L, então L
1
, . . . , L
n
f(π)
N
1
L, e λ(f (π)) ≤ cλ(π)
e ρ(f(π)) ≤ cρ(π).
Corolário A.9 Sej a κ qualq uer conjunto de conectivos adequados. Todo sistema de
dedução de Frege e sistema d e Dedução Natural sobre κ p−simu la todos os outros
PUC-Rio - Certificação Digital Nº 0220933/CA
Apêndice A. Sistemas de Frege 57
sistemas de Frege e sistemas de Dedução Natural sobre κ. Assim, tal s istema s obre
κ é limitad o polino mialmente se e somente se todos tais sistemas sobre κ forem
limitados polinomialm ente.
A.4
Frege estendido
Cook e Rechkow (CR79) apresentaram uma estensão natural para o sistemas
de Frege alegando que tal s istema produziria provas mais curtas.
Foi utilizado o princípio d as casas dos pomb os para il ustrar a eficiência, em
termos de tamanho de prova, d o sistema de Frege estendi do em relação ao sistema
de Frege não estendido.
Contudo, Buss em (Bus87) mostrou que o princípio das casas de pombos
não po de ser usado para separar o sistema de Frege do sistema de Frege estendi do
apresentando, como justificativa, uma prova polinomial do princípio em sistema de
Frege.
Teorema A.10 Se π é uma derivação de B a partir de A
1
, . . . , A
n
em eF , então
existe uma deri vação π
de B a partir de A
1
, . . . , A
n
em F com λ(π
) ≤ λ(π) +cm
onde c depende apena s de F e m é o número de f órmulas defini das em π
Teorema A.11 Sejam eF e eF
dois sistemas de Frege sob κ e κ
, respectiva-
mente, e suponha L(n) ≥ n é uma função natural tal que toda tautologia A sob
κ tenha uma prova π em eF com λ(π) ≤ L(l(A)). Ent ão to da tautologia A
sob
κ
possui uma prova π
em eF
tal que λ(π
) ≤ cL(cl(A
)), onde a constante c
depende apenas de F e F
.
Corolário A.12 U m sistema de Frege estendido é limitado polino m ialmente se
e somente se todos os sistemas de Frege estendidos sob todos os conjuntos de
conectivos forem l imitados polinomialmente. Além disso, um sistema de Frege
estendido é po linomialmente limitado se e somente se existir um limi te polinomial
sob o número de l inhas nas provas em eF . Desta forma, se P = NP , então não
existe um limite polinomial sob o número de linhas em provas em sistemas de Frege
estendidos, sistemas de Frege ou sistema de Dedução Natural.
PUC-Rio - Certificação Digital Nº 0220933/CA
B
Esquema da prova de P HP
2
Faremos a prova de ¬P HP
2
→ ¬P HP
1
= ⊥, onde
P HP
2
=
(p
00
∨ p
01
) ∧ (p
10
∨ p
11
) ∧ (p
20
∨ p
21
) →
(p
00
∧ p
10
) ∨ (p
01
∧ p
11
) ∨ (p
00
∧ p
20
) ∨ (p
01
∧ p
21
) ∨ (p
10
∨ p
20
) ∨ (p
11
∧ p
21
)
Para facilitar a apresentação das deduções que serão apresentadas a seguir
usaremos α para representar o lado esquerdo de P HP
2
e β para representar o lado
direito.
Trabalharemos, sem perda de generalidade, com ¬P HP
2
≡ α ∧ ¬β.
A prova de que P HP
2
→ P HP
1
, terá o seguinte aspecto:
α ∧ ¬β
¬β
α ∧ ¬β
α
β ∨ σ
σ
α ∧ ¬β
¬β
¬α ∨ ¬σ
α ∧ ¬β
α
¬σ
⊥
A seguir apresentaremos a prova de
α
β ∨ σ e de
¬β
¬α ∨ ¬σ
Usaremos o s eguinte processo para abreviar a representação de ∨ encadeados.
α ∨ β γ ∨ δ
σ σ σ σ
σ
Comecemos com a prova de
α
β ∨ σ:
De α, obtemos as seguintes fórmulas po r ∧E.
α
(p
00
∨ p
01
)
α
(p
10
∨ p
11
)
α
(p
20
∨ p
21
)
Agora, aplicando ∨E produziremos:
PUC-Rio - Certificação Digital Nº 0220933/CA
Apêndice B. Esquema da prova de P HP
2
59
p
00
∨ p
01
p
10
∨ p
11
p
20
∨ p
21
a
b
c
d
e
f
g
h
i
j
k l
onde a = (p
00
∧ p
10
), b = (p
01
∧ p
11
), c = (p
00
∧ p
20
), d = (p
01
∧ p
21
),
e = (p
10
∧ p
20
), f = (p
11
∧ p
21
), g = (p
00
∧ p
11
), h = (p
01
∧ p
10
), i = (p
00
∧ p
21
),
j = (p
01
∧ p
20
), k = (p
11
∧ p
20
) e l = (p
10
∧ p
21
).
Temos que β = a ∨ b ∨ c ∨ d ∨ e ∨ f .
Aplicando ∨I produzimos uma fórmula β ∨ σ onde σ = g ∨ h ∨ i ∨ j ∨ k ∨ l.
Ou seja, partindo de α dedu zi mos β ∨ σ, como desejávamos.
A prova de
¬β
¬α ∨ ¬σ segue de modo análo g o.
PUC-Rio - Certificação Digital Nº 0220933/CA
C
Numeral de Church
Seja p uma variável, e defina os tipos iterados por
0p := p;
(k + 1)p := kp → kp
Os numerais de Church de tipo kp é definidos por
I
n
k
= λy
kp→kp
x
kp
.y
n
(x)
Exemplo C.1 O exemplo a seguir, representa o numeral d e Church I
3
0
p → p
p → p
p → p p
p
p
p
p → p
(p → p) → (p → p)
Figura C.1: I
3
0
A profundidade de I
n
0
é n + 2.
Notação C.2 Seja "h yp" a função hiper-exponencial definida por
hyp(x, 0, y) = z, hyp(x, Sx, z) = x
hyp(x,y,z )
Abreviamos,
2
i
k
:= hyp(2, k, i), 2
k
= hyp(2, k, 1),
Um fato interessante dos numerais de Church está na facilidade de gerar
exemplos de provas normais com profundidade hyper-exponencial e provas não
normais curtas. Por exemplo o numeral I
2
n
0
tem prova norm al de profundidade 2
n
+ 2
enquanto que a prova não normal possui profundidade n + 3.
PUC-Rio - Certificação Digital Nº 0220933/CA
Apêndice C. Numeral de Church 61
A prova segue d iretamente da seguinte redução:
I
2
n−1
I
2
n−2
. . . I
2
0
=
β
I
2
n
0
. (C-1)
O lado esquerdo tem profundidade n + 3 enquanto o lado esquerdo tem
profundidade 2
n
+ 2.
Substituindo algumas p osições ocupadas por p p or variáveis A
i
, conseguimos
gerar uma nova prova com ramos distintos.
Exemplo C.3 Considerando os numerais I
2
0
e I
2
1
.
p p → p
p p → p
p
p → p
(p → p) → (p → p)
(p → p) (p → p) → (p → p)
(p → p) (p → p) → (p → p)
(p → p)
(p → p) → (p → p)
Podemos representar I
4
0
da seguinte forma:
(p → p) I
2
0
(p → p) I
2
0
(p → p)
(p → p) → (p → p)
A figura abaixo representa o numeral I
4
0
modificado, as partes marcadas na
figura representam modificações do numeral I
2
0
.
[A
1
→ A
2
]
5
[A
2
→ A
3
]
4
[A
1
]
1
[A
1
→ A
2
]
2
A
2
[A
2
→ A
3
]
3
A
3
(A
1
→ A
3
)
1
(A
1
→ A
2
) → (A
1
→ A
3
)
2
(A
2
→ A
3
) → ((A
1
→ A
2
) → (A
1
→ A
3
))
3
(A
1
→ A
2
) → (A
1
→ A
3
)
(A
1
→ A
3
)
[A
4
]
6
[A
4
→ A
1
]
7
A
1
[A
1
→ A
3
]
8
A
3
(A
4
→ A
3
)
6
(A
4
→ A
1
) → (A
4
→ A
3
)
7
(A
1
→ A
3
) → ((A
4
→ A
1
) → (A
4
→ A
3
))
8
(A
4
→ A
1
) → (A
4
→ A
3
)
(A
2
→ A
3
) → ((A
4
→ A
1
) → (A
4
→ A
3
))
(A
1
→ A
2
) → ((A
2
→ A
3
) → ((A
4
→ A
1
) → (A
4
→ A
3
)))
Figura C.2: Numeral I
4
0
modificado.
PUC-Rio - Certificação Digital Nº 0220933/CA
D
Clássica para Intuicionista
Conforme anunciado na introdução, apresentam os u ma versão da prova de
normalização de Seldin. Também mostraremos como é possível definir uma tradu-
ção da lógica clássica para a lógica intuicionista a partir da normalização de Seldin.
Este trabalho encontrasse melh or fundamentado em (dPN01).
Definição D.1 (Profundidade de uma derivação) A profunidade de uma deriva-
ção π, denotado por d(π), é o número de ocorrência s de fórmulas de π. Mas preci-
samente d(π) é definido, por indução, como segue:
i) Se π é constituída por apenas uma hipótese, então l(π) = 1;
ii) Se π é
Σ
1
A
1
· · ·
Σ
2
A
n
C , então d(π) = d ( Σ
1
) + · · · + d(Σ
n
) para n ≤ 3.
Teorema D.2 Se π é uma derivação de C a partir de ∆ em S, então π pode ser
transformada em uma derivação π
de C a partir de ∆ em S tal que π
contém no
máximo uma aplicação da regra de abs urdo clássico e, caso esta aplicação ocorra,
é a última inferência de π
.
Prova. Prova por ind ução n a profundidade de π.
Se a profundidade de π é igual a 1 , é imediato. Nos demais casos, seja π a
derivação abaixo e r a sua última inferência.
Σ
1
A
1
Σ
2
A
2
Σ
3
A
3
C
Pela hipótese de indução, as subderivações Σ
1
, Σ
2
e Σ
3
podem ser transfor-
madas respectivamente nas derivações Σ
1
, Σ
2
e Σ
3
tais que, se existirem aplicações
da regra de absurdo clássico em cada uma delas, existe apenas uma e é a última
inferência da derivação. Seja π
1
o resul tado da substitui ção de cada Σ
i
, i ≤ 3, po r
Σ
i
em π.
Se nenhum Σ
i
, i ≤ 3, termina com uma aplicação de absurdo clássico, então
π
1
é a derivação desejada. Nos outros casos, mostraremos que a derivação π
1
pode
ser transformada em uma derivação π
1
na qual a única aplicação de ⊥
c
é a sua
última inferência.
PUC-Rio - Certificação Digital Nº 0220933/CA
Apêndice D. Clássica para Intuicionista 63
Caso 1 r é a aplicação de →-E ou ∧-E.
1. Para algum i < 2, Σ
i
termina com uma aplicação de ⊥
c
Sem perda de
generalidade seja i = 1.
π
1
≡
[¬A
1
]
k
Σ
1
⊥
A
1
k
Σ
2
A
2
C
r
π
1
≡
[A
1
]
k
Σ
2
A
2
C
r
[¬C]
j
⊥
[¬A
1
]
k
Σ
1
⊥
C
j
2. Σ
1
e Σ
2
terminam com uma aplicação de ⊥
c
π
1
≡
[¬A
1
]
j
Σ
1
⊥
A
1
i
[¬A
2
]
j
Σ
2
⊥
A
2
i
C
r
π
1
≡
[A
1
]
i
[A
2
]
j
C
r
[¬C]
k
⊥
[¬A
1
]
i
⊥
[¬A
2
]
j
Σ
2
⊥
C
k
Caso 2 r é aplicação de →-I
π
1
≡
[A
1
]
i
[¬B]
j
Σ
1
⊥
B
j
A → B
r,i
π
1
≡
[A]
i
[B]
j
A → B
r
[¬(A → B)]
k
⊥
[¬B]
Σ
1
⊥
B
r,i
A → B [¬(A → B)]
k
⊥
A → B
k
Caso 3 r é uma aplicação de ∧-E ou ∨-I.
π
1
≡
[¬A
1
]
i
Σ
1
⊥
A
1
i
C
r
π
1
≡
[A
1
]
i
C
r
[¬C]
j
⊥
[¬A
1
]
i
Σ
1
⊥
C
j
Caso 4 r é uma aplicação de ∧-E
PUC-Rio - Certificação Digital Nº 0220933/CA
Apêndice D. Clássica para Intuicionista 64
1. Apenas Σ
1
termina com uma aplicação de ⊥
c
π
1
≡
[¬(A ∨ B)]
i
Σ
1
⊥
A ∨ B
[A]
j
Σ
2
C
[B]
k
Σ
3
C
C
r,j,k
π
1
≡
[A ∨ B]
i
[A]
l
Σ
2
C
[B]
k
Σ
3
C
C
r,j,k
[¬C]
l
⊥
[¬(A ∨ B)]
i
Σ
1
⊥
C
l
2. Apenas Σ
2
termina com uma aplicação de ⊥
c
π
1
≡
Σ
1
A ∨ B
[A]
j
[¬C]
i
Σ
2
⊥
C
[B]
k
Σ
3
C
C
r,j,k
π
1
≡
Σ
1
A ∨ B
[A]
j
[¬C]
i
Σ
2
⊥
[B]
k
Σ
3
C [¬C]
i
⊥
⊥
r,j,k
C
i
3. Apenas Σ
3
termina com uma aplicação de ⊥
c
Similar ao caso anterior
4. Σ
1
, Σ
2
, Σ
3
terminam com uma aplicação de ⊥
c
π
1
≡
[¬(A ∨ B)]
i
Σ
1
⊥
A ∨ B
i
[A]
j
[¬C]
l
Σ
2
⊥
C
l
[B]
k
[¬C]
l
Σ
3
⊥
C
l
C
r,j,k
π
1
≡
[A ∨ B]
i
[A]
j
[¬C]
l
Σ
2
⊥
[B]
k
[¬C]
l
Σ
3
⊥
⊥
r,j,k
[¬(A ∨ B)]
i
Σ
1
⊥
C
l
PUC-Rio - Certificação Digital Nº 0220933/CA
Apêndice D. Clássica para Intuicionista 65
Caso 5 r é aplicação de absurdo clássi co
π
1
≡
[¬⊥]
i
[¬C]
j
Σ
1
⊥
⊥
i
C
r,j
π
1
≡
[¬⊥]
i
¬⊥
i
[¬C]
j
Σ
1
⊥
C
D.0.1
Tradução da ló g ica clássica para a lógica intui cio n ista
De posse do resultado anterior, definiremos uma função que associa fórmulas
da linguagem clássica a fórmulas da lin guagem intuicio nista.
Definição D.3 Seja h
1
uma função que associ a fórmulas da linguagem clássica a
fórmulas da linguagem intuicionista definida recursivamente como segu e:
h
1
(A) =
def
A, se A é uma fórmula atômica.
h
1
(A → B) =
def
h
1
(A) → h
1
(B)
h
1
(A ∧ B) =
def
h
1
(A) ∧ h
1
(B)
h
1
(A ∨ B) =
def
h
1
(A) ∨ h
1
(B)
Definição D.4 Seja h
2
uma função que associ a fórmulas da linguagem clássica a
fórmulas da linguagem intuiciontista definida como segue:
h
2
(A) =
def
¬¬h
1
(A), para toda fórmula A pertencente a linguagem clás-
sica.
h
2
é uma função tradução da l ógica clássica na lógica intuicionista, como
veremos.
Lema D.5
C
A ↔ h
2
(A)
Prova. Como (B ↔ ¬¬B) é teorema em ló gica clássica, para qualquer B perten-
cente a linguagem clássica, temos que
c
h
1
(A) ↔ ¬¬h
1
(A). As sim, para mostrar
que A ↔ h
2
(A) é o teorema em lógica clássica, será suficiente provar que:
C
A ↔ h
1
(A) (D-1)
Pois, por definição temos que h
2
(A) é ¬¬h
1
(A).
A prova de (D-1) segue imediatamente por ind ução no comprimento da prova
A.
PUC-Rio - Certificação Digital Nº 0220933/CA
Apêndice D. Clássica para Intuicionista 66
Lema D.6 Γ
C
A se, e somente se, h
2
(Γ) h
2
(A).
Prova. Segue imediatam ente do lema anterior.
Lema D.7 Se h
2
(Γ)
C
h
2
(A), então h
2
(Γ)
I
h
2
(A).
Prova. De h
2
(Γ)
C
h
2
(A) temos, pelo teorema D.2 , que existe u ma derivação pi
de h
2
(A) a partir de h
2
(Γ) tal que a única aplicação de ⊥
C
, se existir, é a última
inferência de π. Se a última inferência de π não é uma aplicação de ⊥
c
, claramente
π é uma derivação em I e conseqüentement e π seria a derivação desejada.
Caso contrário, π seria:
h
2
(Γ) [¬h
2
(A)]
i
Σ
⊥
h
2
(A)
⊥
C
,i
Do fato da subderivação Σ de π não ter aplicações de absurdo clássico e de
(¬B → ¬¬B) s er um t eorem a da lógica intuicionista, temos a seguinte derivação
de h
2
(A) a partir de h
2
(Γ) em I como desejávamos.
h
2
(Γ)
[¬h
1
(A)]
i
¬h
1
(A) → ¬¬¬h
1
(A)
¬¬¬h
1
(A)
¬h
2
(A)
def
Σ
⊥
¬¬h
1
(A)
i
h
2
(A)
def
Como o sist ema intu icionista é um subsistem a do sistema clássi co, t emos:
Lema D.8 Se h
2
(Γ) I h
2
(A), então h
2
(Γ) C h
2
(A).
Como conseqüência imediata dos lemas D.6 e D.8, temos.
Teorema D.9 Γ C A se, e somente se, h
2
(Γ) I h
2
(A).
Observe que a transformação h
2
é polin omial em relação ao tamanho de
A. Além disso a nova d erivação de clássica para intuicionista no teorema D.7 é
realizada apenas acrescentado 3 linhas a derivação clássica, no pior caso. Ou seja,
a transformação de uma prova em sistema clássico para uma prova em sistema
intuicionista pode ser realizada poli nomialmente.
PUC-Rio - Certificação Digital Nº 0220933/CA
Livros Grátis
( http://www.livrosgratis.com.br )
Milhares de Livros para Download:
Baixar livros de Administração
Baixar livros de Agronomia
Baixar livros de Arquitetura
Baixar livros de Artes
Baixar livros de Astronomia
Baixar livros de Biologia Geral
Baixar livros de Ciência da Computação
Baixar livros de Ciência da Informação
Baixar livros de Ciência Política
Baixar livros de Ciências da Saúde
Baixar livros de Comunicação
Baixar livros do Conselho Nacional de Educação - CNE
Baixar livros de Defesa civil
Baixar livros de Direito
Baixar livros de Direitos humanos
Baixar livros de Economia
Baixar livros de Economia Doméstica
Baixar livros de Educação
Baixar livros de Educação - Trânsito
Baixar livros de Educação Física
Baixar livros de Engenharia Aeroespacial
Baixar livros de Farmácia
Baixar livros de Filosofia
Baixar livros de Física
Baixar livros de Geociências
Baixar livros de Geografia
Baixar livros de História
Baixar livros de Línguas
Baixar livros de Literatura
Baixar livros de Literatura de Cordel
Baixar livros de Literatura Infantil
Baixar livros de Matemática
Baixar livros de Medicina
Baixar livros de Medicina Veterinária
Baixar livros de Meio Ambiente
Baixar livros de Meteorologia
Baixar Monografias e TCC
Baixar livros Multidisciplinar
Baixar livros de Música
Baixar livros de Psicologia
Baixar livros de Química
Baixar livros de Saúde Coletiva
Baixar livros de Serviço Social
Baixar livros de Sociologia
Baixar livros de Teologia
Baixar livros de Trabalho
Baixar livros de Turismo
