Livro - Ciencia Da Computação -Mat, Manuais, Projetos, Pesquisas de Eletromecânica

Baixe Livro - Ciencia Da Computação -Mat e outras Manuais, Projetos, Pesquisas em PDF para Eletromecânica, somente na Docsity! Lógica e aplicações: Matemática, Ciência da Computação e Filosofia (Versão Preliminar - Caṕıtulos 1 a 5) W.A. Carnielli1, M.E. Coniglio1 e R. Bianconi2 1Departamento de Filosofia Universidade Estadual de Campinas C.P. 6133, CEP 13081-970 Campinas, SP, Brasil E-mail: {carniell,coniglio}@cle.unicamp.br 2Instituto de Matemática e Estat́ıstica Universidade de São Paulo C.P. 66281, CEP 05315-970 São Paulo, SP, Brasil E-mail: bianconi@ime.usp.br c© Todos os direitos reservados (Comentários e sugestões são muito bem-vindos) 16 de maio de 2005 Sumário 1 Histórico e Paradoxos 3 1.1 Os Paradoxos Lógicos e o Infinito . . . . . . . . . . . . . . . . 3 1.2 Algumas Propriedades Paradoxais do Infinito . . . . . . . . . 4 1.2.1 O Paradoxo de Galileu . . . . . . . . . . . . . . . . . . 4 1.2.2 O Passeio de Cantor e os tipos distintos de infinito . . 5 1.2.3 O Hotel de Hilbert . . . . . . . . . . . . . . . . . . . . 8 1.2.4 O Lema de König . . . . . . . . . . . . . . . . . . . . 8 1.3 Os Paradoxos Lógicos . . . . . . . . . . . . . . . . . . . . . . 9 1.3.1 O significado dos paradoxos . . . . . . . . . . . . . . . 9 1.3.2 Paradoxos e antinomias mais conhecidos . . . . . . . 11 1.3.3 O que podemos aprender com os paradoxos? . . . . . 14 2 Linguagem e Semântica da lógica proposicional clássica 15 2.1 Linguagens proposicionais . . . . . . . . . . . . . . . . . . . . 15 2.1.1 Assinaturas e linguagens . . . . . . . . . . . . . . . . . 15 2.1.2 Indução estrutural . . . . . . . . . . . . . . . . . . . . 20 2.1.3 A linguagem da LPC . . . . . . . . . . . . . . . . . . . 24 2.1.4 Exerćıcios . . . . . . . . . . . . . . . . . . . . . . . . . 28 2.2 Semântica da LPC . . . . . . . . . . . . . . . . . . . . . . . . 29 2.2.1 Semântica dos conectivos . . . . . . . . . . . . . . . . 29 2.2.2 Tautologias, contradições e contingências . . . . . . . 33 2.2.3 Formas normais . . . . . . . . . . . . . . . . . . . . . . 37 2.2.4 Conjuntos adequados de conectivos . . . . . . . . . . . 41 2.2.5 Conseqüência semântica . . . . . . . . . . . . . . . . . 44 2.2.6 Exerćıcios . . . . . . . . . . . . . . . . . . . . . . . . . 48 3 Axiomática e Completude 49 3.1 Métodos de Dedução . . . . . . . . . . . . . . . . . . . . . . . 49 3.2 Sistemas Axiomáticos . . . . . . . . . . . . . . . . . . . . . . 50 1 ores menores que N claramente ultrapassam N (o resultado do produto de números menores que N pode ser maior que N). Dessa forma, somos obri- gados a trabalhar com a hipótese de que a seqüência dos números naturais é ilimitada, ou seja, infinita de algum modo. Este modo de tratar as quantidades ilimitadas corresponde ao chamado infinito potencial, isto é, teoricamente não limitado. A esse conceito se con- trapõe a idéia do infinito atual ou infinito completado, quando tratamos uma classe infinita como um todo. Por exemplo, se queremos estudar as propriedades do conjunto N dos números naturais (o qual, em termos de or- dem, também nos referimos como ω) estamos tratando com o infinito atual, ou em outras palavras, assumindo-o como completado. Muitos paradoxos antigos (como os paradoxos de Zenão de Eléia) exploram esta distinção: se assumimos que o infinito atual é posśıvel, o paradoxo se resolve (como dis- cutiremos a seguir). Mas assumir que o infinito atual existe tem seu preço, e cria outros paradoxos, como veremos mais adiante. Podemos ver o mecanismo de prova por indução que será bastante u- sado neste livro (ver Caṕıtulo 2) como um mecanismo que permite passar, dentro da aritmética, do infinito potencial ao infinito atual. Dessa forma, na matemática usual, não precisamos nos preocupar com a distinção entre infinito atual e potencial, embora essa distinção continue a ser um problema filosófico interessante. Quando assumimos o infinito atual, como mostrou o matemático russo Georg Cantor, criador da moderna teoria dos conjuntos, somos obrigados a admitir que existe não um, mas infinitos tipos de infinito. Por exemplo, Cantor mostrou que a quantidade infinita de números naturais, embora seja a mesma quantidade dos números racionais, é distinta da quantidade infinita de números reais. A seguir, com finalidade de interessar o leitor sobre o que podemos chamar a Grande Questão do Infinito, vamos mostrar alguns tipos de pro- priedades e de problemas que ilustram de maneira simples o caráter para- doxal do infinito, antes de passarmos aos outros paradoxos que envolvem mecanismos mais sofisticados (como a auto-referência, que como veremos, encerra de algum modo uma idéia de regresso infinito). 1.2 Algumas Propriedades Paradoxais do Infinito 1.2.1 O Paradoxo de Galileu Consta do folclore que Galileu Galilei haveria ficado muito intrigado com a seguinte questão: se o conjunto dos números pares está contido propriamente 4 no conjunto dos números naturais, deve haver menos pares que naturais (por exemplo, os ı́mpares não são pares, e eles são infinitos). Porém se fizermos a seguinte identificação: 2 7→ 1 4 7→ 2 6 7→ 3 ... 2n 7→ n ... podemos fazer o conjunto dos pares ocupar todo o conjunto dos naturais. Como é posśıvel que a parte não seja menor que o todo? Justamente, falhar a propriedade de que o todo seja maior que as partes é uma caracteŕıstica das coleções infinitas, o que explica em parte nossa dificuldade em compreendê-las. 1.2.2 O Passeio de Cantor e os tipos distintos de infinito Durante muito tempo (até pelo menos o século XIX) pensou-se que os números racionais não poderiam ser enumeráveis (ou contáveis) como os naturais, uma vez que entre cada dois racionais a b e c d existe sempre outro, que é sua média aritmética: a.d+ b.c 2.b.d e portanto entre dois racionais há infinitos outros. Georg Cantor mostrou por um artif́ıcio muito simples que, embora real- mente entre cada dois racionais haja infinitos outros, basta contarmos os racionais de uma maneira diferente da usual (por “usual” entendemos a or- dem dos números reais, vistos como pontos de uma reta) para que possamos nos convencer que há precisamente tantos racionais quanto números natu- rais. Para isso, estabeleceremos uma enumeração dos números racionais positivos (maiores que zero), e a partir dáı, é posśıvel (por um argumento análogo àquele da prova da similaridade entre os pares e os naturais) provar a enumerabilidade dos racionais: 5 1/1 // 1/2 }}{{ {{ {{ {{ 1/3 // 1/4 }}{{ {{ {{ {{ 1/5 . . . 2/1  2/2 =={{{{{{{{ 2/3 }}{{ {{ {{ {{ 2/4 =={{{{{{{{ 2/5 . . . 3/1 =={{{{{{{{ 3/2 }}{{ {{ {{ {{ 3/3 =={{{{{{{{ 3/4 3/5 . . . 4/1  4/2 =={{{{{{{{ 4/3 4/4 4/5 . . . 5/1 =={{{{{{{{ 5/2 5/3 5/4 5/5 . . . ... ... ... ... ... Nessa tabela, mesmo que algumas frações equivalentes apareçam várias vezes (como, por exemplo, 1/1, 2/2, 3/3, . . . etc.), todos os racionais positivos certamente aparecem, e cada um recebe um número natural, como mostra o caminho traçado no diagrama acima (chamado de passeio de Cantor). Por outro lado, os números reais não podem, de fato, ser enumerados: suponhamos, para poder chegar a um absurdo, que os reais sejam enu- meráveis. Se assim o fosse, os reais no intervalo fechado [0, 1] também se- riam. E dentro dessa suposição imaginemos que temos uma lista completa deles usando a expansão decimal, de modo que se o número não é uma d́ızima como 0, 345 escrevemo-lo com infinitos zeros à direita 0, 345000 . . .; mais ainda, o número 1 é representado como 0, 999 . . . : 6 Se a vida na Terra não se acabar, existe uma pessoa que vai ter infinitos descendentes. Sugestão: pense numa árvore e use o Lema de König. 2. O Problema da Caixa de Bolas Uma caixa contém inicialmente uma bola marcada com um número arbitrário. Imagine que podemos sempre trocar uma bola por uma quantidade qualquer (finita) de bolas, mas marcadas com um número menor. Por exemplo, podemos trocar uma bola marcada com 214 por 1.000.000 de bolas marcadas com 213, e assim por diante. No caso porém de retirarmos uma bola marcada por zero, não colocamos nenhuma outra. Será posśıvel por esse processo esvaziar a caixa? Sugestão: pense numa árvore cujos nós sejam as bolas, e cujos nós sucessores sejam as que foram colocadas em seu lugar. Use o Lema de König. 1.3 Os Paradoxos Lógicos 1.3.1 O significado dos paradoxos Vários exemplos na literatura e na pintura, como os quadros do pintor belga René Magritte e os desenhos do holandês M. C. Escher, fazem uso da noção de auto-referência e de seu caráter paradoxal como elemento de estilo. Numa passagem do “Ulisses” de James Joyce, por exemplo, uma das personagens centrais, Molly Bloom, questiona o próprio autor. Um dos mais simples, e provavelmente o mais antigo, dos paradoxos lógicos é o “Paradoxo do Mentiroso”, formulado por um pensador cretense do século VI A.C., Epimênides, que dizia: “Todos os cretenses são mentirosos”. Esta sentença, só superficialmente problemática, é frequentemente con- fundida com o paradoxo de Eubulides de Mileto, que afirma “Eu estou mentindo”, esta sim, uma afirmação paradoxal e que está na raiz de um dos resultados da lógica formal mais importantes do século XX. A versão de Epimênides figura na B́ıblia, tornando a lógica a única disciplina com referência b́ıblica: “Os cretenses são sempre mentirosos, feras selvagens, glutões preguiçosos”, adverte a eṕıstola de São Paulo a Tito (1:12-13), chamando a atenção para o fato de que o próprio cretense Epimênides o afirma. O paradoxo do mentiroso na versão de Eubulides (na forma “Eu estou mentindo” ou “Esta sentença é falsa”), longe de ser uma simples banalidade 9 do pensamento, está ligado, como veremos, a um dos teoremas mais profun- dos do pensamento lógico e matemático, o Teorema de Gödel, formulado em 1936. Pode parecer que a auto-referência é a causa destes paradoxos; contudo, a auto-referência, por si mesma, não é nem sempre responsável pelo caráter paradoxal das asserções, nem mesmo suficiente para causar paradoxos: por exemplo, se um cretense afirma “Os cretenses nunca são mentirosos”, ou se Eubulides afirma “Não estou mentindo” estas afirmações auto-referentes são apenas pretensiosas. Por outro lado, mesmo que aboĺıssemos a auto-referência não elimi- naŕıamos os paradoxos: por exemplo, um paradoxo conhecido desde a época medieval imagina o seguinte diálogo entre Sócrates e Platão: Sócrates: “O que Platão vai dizer é falso” Platão: “Sócrates acaba de dizer uma verdade”. Nenhuma das sentenças pode ser verdadeira, e nem falsa; nesse caso, a causa do paradoxo é a referência cruzada ou circular, e não a auto-referência. Mas nem mesmo a circularidade da referência é sempre responsável pelos paradoxos: uma simples mudança no diálogo entre Sócrates e Platão (basta trocar “falso” por “verdadeiro” e vice-versa) elimina o paradoxo, embora a circularidade continue presente. Na realidade, um dos problemas lógicos mais dif́ıceis é determinar quais são as condições que geram paradoxos, além das tentativas de eliminar, solu- cionar ou controlar os já existentes. Este problema é, em muitos casos, in- solúvel, e tal fato tem obviamente um enorme significado para o pensamento cient́ıfico em geral, e para a lógica em particular. Apresentamos aqui alguns dos mais conhecidos paradoxos, antinomias e ćırculos viciosos. A análise dos paradoxos serve como motivação ao es- tudo da lógica matemática, que poderia ser pensada como a formalização do pensamento racional livre de paradoxos, pelo menos dos paradoxos que a destroem. Se aceitamos as leis básicas da lógica tradicional (isto é, leis que regem os operadores “ou”, “e”, “se... então”, “não”, “para todo”, “existe”), que são o objeto de estudo deste livro, há basicamente duas maneiras de “resolver” um paradoxo: 1. a primeira (seguindo uma tradição iniciada pelo lógico inglês Bertrand Russell) que propõe que certos enunciados paradoxais deixem de ser considerados como enunciados propriamente ditos; 10 2. a segunda (a partir de idéias devidas ao lógico polonês Alfred Tarski) propõe que sejam considerados como regulares os enunciados onde não ocorre o predicado de “ser verdade” (ou assemelhados, como “ser falso”); os enunciados lingúısticos que não são regulares fazem parte da metalinguagem. Costuma-se ainda fazer distinção, na literatura, entre paradoxos e antino- mias: estas seriam as contradições lógicas, como o Paradoxo de Russell e do Mentiroso, enquanto os paradoxos propriamente ditos seriam os enunciados que não envolvem contradição, mas desafiam nossas intuições ou crenças. As situações paradoxais apresentadas a seguir são formuladas na lin- guagem natural (isto é, em português corrente); como exerćıcio, você deve tentar analisá-las, informalmente, e decidir se se trata de antinomia, se existe solução, ou simplesmente de uma situação paradoxal que escapa à intuição. Os problemas aqui encontrados servirão de motivação para que seja intro- duzida uma linguagem formal, muito mais simples que a linguagem natural, mas também muito mais exata, e que com base nesta linguagem sejam for- muladas cuidadosamente as regras e leis que regem a lógica. Dessa forma, podemos então considerar a lógica não como uma teoria que resolve todos os paradoxos, mas como uma disciplina que aprende com eles e que tenta erigir um domı́nio em que se minimizem seus efeitos. 1.3.2 Paradoxos e antinomias mais conhecidos 1. Numa folha de papel em branco escreva: “A sentença do outro lado é verdadeira”. No outro lado escreva: “A sentença do outro lado é falsa”. As sentenças são verdadeiras ou falsas? 2. (Paradoxo de Bertrand Russell, numa carta a G. Frege, em 1902) Con- sidere o conjunto de todos os conjuntos que não são membros de si mesmos. Este conjunto é membro de si próprio? 3. (Paradoxo do Barbeiro) Um barbeiro foi condenado a barbear todos e somente aqueles homens que não se barbeiam a si próprios. Quem barbeia o barbeiro? 4. (Paradoxo de Kurt Grelling) Podemos dividir os adjetivos em duas classes: autodescritivos e não-autodescritivos. Por exemplo, são au- todescritivos os adjetivos “polisśılabo”, “escrito”, e não-autodescritivos os adjetivos “monosśılabo”, “verbal”, etc. O adjetivo “não-autodescriti- vo” é autodescritivo ou não-autodescritivo? 11 Analise agora as sentenças abaixo, conhecidas como Paradoxos do con- hecimento: (a) “Ninguém acredita nesta sentença”. Mostre que esta sentença não faz parte do conhecimento de ninguém. (b) “Eu não acredito nesta sentença”. É posśıvel que você acredite nesta sentença? (c) “Ninguém conhece esta sentença”. Mostre que esta sentença é verdadeira, mas não faz parte do conhecimento de ninguém. 1.3.3 O que podemos aprender com os paradoxos? Na seção precedente optamos por colocar os paradoxos como questões, de- safiando você a tentar resolvê-los. Não mostramos as soluções, porque em geral elas não existem: os paradoxos não podem ser resolvidos como simples exerćıcios. Na verdade os paradoxos colocam problemas que vão muito além da capacidade do conhecimento da lógica e mesmo da ciência. Portanto, não devemos nos surpreender com o fato de que os paradoxos possam conviver lado a lado com a lógica; o que podemos concluir é que o jardim organi- zado e seguro da lógica representa apenas uma parte da floresta selvagem do pensamento humano. Dentro deste pequeno jardim podemos usar nosso instrumento formal, que é o que será introduzido neste livro, e através dele colher algumas belas flores, algumas até surpreendentemente bonitas e cu- riosas; muitas outras podem estar perdidas na floresta, esperando ser de- scobertas. Dessas, este livro não vai tratar, mas esperamos que você pelo menos compreenda onde estão os limites do jardim da lógica. 14 Caṕıtulo 2 Linguagem e Semântica da lógica proposicional clássica 2.1 Linguagens proposicionais 2.1.1 Assinaturas e linguagens Apesar de diversos autores e obras tentarem apresentar a lógica como uma teoria do racioćınio, os paradoxos, como vimos, mostram que é dif́ıcil aceitar que raciocinemos com alguma lógica, pelo menos com uma determinada. Preferimos considerar a lógica como uma teoria da comunicação do racioćınio, isto é, uma teoria da argumentação vista como o encadeamento de seqüências de sentenças por meio de uma (ou várias) relação do tipo “. . . segue de . . .”. Dessa forma, precisamos nos preocupar com três tarefas básicas: 1. especificar a linguagem com que expressamos os argumentos; 2. esclarecer os mecanismos que produzam ou que verifiquem os argu- mentos válidos; e 3. definir as noções de provas ou demonstrações, isto é, as seqüências de argumentos que produzam o fim desejado. Contentamo-nos com as sentenças ditas declarativas, evitando assim sen- tenças interrogativas, temporais, modais, etc. De nosso ponto de vista, a lógica se interessa pelo racioćınio matemático tradicional, e para tal fim as sentenças declarativas são suficientes. 15 A rigor, podemos considerar também as sentenças performativas, u- sadas por exemplo em linguagens computacionais, que são também sentenças matemáticas, mas tais sentenças performativas podem ser interpretadas (i.e., reescritas) como sentenças declarativas. Precisamos obter uma linguagem precisa para a matemática, que possa ela mesma ser objeto de análise matemática. Iniciamos nossa análise com as proposições estudando assim a lógica sentencial, também chamada de cálculo proposicional, cálculo sentencial ou lógica proposicional clássica, a qual denotaremos por LPC. Mais tarde aumentaremos nossa linguagem para levar em conta as pro- priedades de indiv́ıduos, expressas por meio de relações envolvendo indiv́ıduos e variáveis, estudando então a lógica de predicados também chamada de cálculo de predicados ou lógica de primeira ordem. De acordo com as tarefas básicas com que devemos nos ocupar, o processo de formalização da LPC consiste de: 1. especificar a linguagem formal; 2. especificar o processo de obter proposições válidas nessa linguagem; 3. especificar o processo de obter seqüências de proposições válidas. Começamos especificando a linguagem, através da técnica de definições indutivas, que consiste em apresentar primeiro as proposições atômicas (i.e., que não são decompońıveis em sentenças mais simples) e, num segundo estágio, especificar como as sentenças mais complexas são constrúıdas a partir dessas utilizando conectivos. Os conectivos são funções que conec- tam sentenças dadas para formar sentenças mais complexas. Exemplos de conectivos são a negação ¬, que permite formar a sentença ¬ϕ a partir da sentença ϕ, a conjunção ∧ que permite, dadas as sentenças ϕ e ψ, formar a sentença (ϕ ∧ ψ), etc. Usualmente os conectivos são constantes (isto é, sem argumentos) ou funções de um ou dois argumentos. Porém, para não perder a generalidade, podemos definir linguagens formais onde podemos ter conectivos de qualquer número de argumentos. Chegamos assim à definição seguinte: Definição 2.1.1. Uma assinatura proposicional é uma famı́lia C = {Cn}n∈N tal que cada Cn é um conjunto, sendo que Cn ∩ Cm = ∅ se n 6= m. Os ele- mentos do conjunto Cn são chamados de conectivos n-ários. Em particular, os elementos de C0 são chamados de constantes. A idéia da construção de linguagens formais proposicionais é a seguinte: partindo de um conjunto infinito fixado V = {pn : n ∈ N} de śımbolos, 16 no lugar de ¬(ϕ) e ∨(ϕ,ψ), respectivamente. Freqüentemente economizare- mos parênteses, omitindo os mais externos. Assim, escrevemos ϕ ∨ ψ ao invés de (ϕ ∨ ψ) quando a leitura não for comprometida. 4 Exemplo 2.1.5. A assinatura C1 consiste dos seguintes conectivos: • C11 = {¬} (negação); • C12 = {⇒} (implicação); • C1n = ∅ se n 6= 1, n 6= 2. Temos que |C1| = {¬,⇒}. É fácil ver que as expressões ¬(⇒(p3, p7)) e ⇒(p0,⇒(¬(p0), p1)) são fórmulas sobre C1. O conjunto L(C1) das fórmulas sobre C1 será chamado de Prop1. Como antes, escreveremos ¬ϕ e (ϕ⇒ ψ) no lugar de ¬(ϕ) e⇒(ϕ,ψ), respectivamente. Também omitiremos freqüen- temente parênteses, quando não houver risco de confusão. Assim, as duas fórmulas acima podem ser escritas como ¬(p3 ⇒ p7) e p0 ⇒ (¬p0 ⇒ p1). 4 Exemplo 2.1.6. A assinatura C2 consiste dos seguintes conectivos: • C21 = {¬} (negação); • C22 = {∨,∧,⇒} (disjunção, conjunção e implicação); • C2n = ∅ se n 6= 1, n 6= 2. Temos que |C2| = {¬,∨,∧,⇒}. Assumindo as mesmas convenções dos dois exemplos anteriores, as expressões p0 ⇒ p0, p4 ⇒ (p4 ∨ p5) e ¬p6 ⇒ (p3∨ (p3∧p5)) são fórmulas sobre C2. O conjunto L(C2) das fórmulas sobre C2 será chamado de Prop2. 4 O leitor perspicaz poderia perguntar-se se é sempre posśıvel construir o conjunto L(C). De fato, a resposta é afirmativa. Assumindo a teoria de conjuntos (vide Apêndice XXX) como base formal para todas as nossas construções podemos simplesmente definir L(C) através da seguinte fórmula: L(C) = ⋂ {X ⊆ EC : X satisfaz as propriedades 1 e 2 da Definição 2.1.3}. A notação ⋂ F acima utilizada denota a interseção do conjunto de conjuntos F , isto é, ⋂ F = {x : x ∈ X para todo X ∈ F}. 19 Dado que o próprio EC satisfaz as propriedades 1 e 2 da Definição 2.1.3, então o conjunto de todos os subconjuntos de EC satisfazendo essas pro- priedades é não vazio, existindo portanto a sua interseção L(C), a qual também satisfaz as propriedades 1 e 2. Claramente L(C) é o menor dos subconjuntos de EC satisfazendo estas propriedades. Outra maneira (talvez mais construtiva) de provar a existência de L(C) é a seguinte: Dado um conjunto arbitrário X, defina o conjunto FC(X) = {c(ϕ1, . . . , ϕn) : n ∈ N, c ∈ Cn e ϕ1, . . . , ϕn ∈ X} ∪X. Defina agora, para cada n ∈ N e para cada conjunto X, o seguinte conjunto: F 0C(X) = X, e F n+1 C = FC(F n C(X)). Claramente este processo sempre pode ser (idealmente) efetuado. Finalmente, juntando todas as expressões definidas através deste processo, teremos uma construção do conjunto L(C): L(C) = ⋃ {FnC(V) : n ∈ N}. Deixamos para o leitor provar que esta última construção define de fato o conjunto L(C). Observação 2.1.7. As letras ϕ1, . . . , ϕn utilizadas para falar em fórmulas arbitrárias, assim como a letra c usada para denotar um conectivo arbitrário, são chamadas metavariáveis, isto é, objetos na metalinguagem que se referem aos objetos sendo estudados. A metalinguagem é simplesmente a linguagem (natural ou matemática) na qual falamos sobre nossa linguagem formal. Us- aremos letras gregas minúsculas (com ou sem ı́ndices) como meta-variáveis de fórmulas. Reservamos p0, p1, p2, . . . para denotar as variáveis proposi- cionais propriamente ditas. 2.1.2 Indução estrutural Em geral, as propriedades das proposições são estabelecidas por um processo indutivo (similar ao usado na definição de L(C)) pelo qual, se queremos provar uma certa propriedade P a respeito das proposições, começamos mostrando que P vale para as proposições atômicas, e depois, supondo a propriedade válida para as componentes de uma proposição, provamo-la para a proposição mais complexa. A rigor, tal processo pode ser inteiramente convertido numa prova ar- itmética, usando a conhecida indução aritmética com relação a um parâmetro numérico qualquer. Por exemplo podemos usar como parâmetro da indução o número de śımbolos (i.e., o comprimento da proposição), o número de parênteses, etc. 20 O teorema a seguir demonstra que de fato as propriedades das proposições podem ser provadas pelo processo indutivo. Este teorema é muito impor- tante porque muitas propriedades da lógica (na verdade, podeŕıamos dizer que a maioria) são provadas através deste processo indutivo. Introduzimos a seguinte notação (semi)formal: P (ϕ) denota que a sen- tença ϕ satisfaz a propriedade P (note que P (ϕ) é um enunciado da meta- linguagem, que pode portanto ser verdadeiro ou falso). Por exemplo, P (ϕ) poderia ser o enunciado “a sentença ϕ tem tantos parênteses esquerdos quan- tos parênteses direitos”, ou o enunciado “em ϕ somente ocorrem variáveis proposicionais e conectivos de aridade 1 ou 2”. Temos portanto o seguinte: Teorema 2.1.8. Seja P uma propriedade sobre expressões, e considere o conjunto X = {ϕ ∈ L(C) : P (ϕ) vale}. Suponha que X satisfaz o seguinte: 1. V ⊆ X; 2. para todo n ∈ N, c ∈ Cn e ϕ1, . . . , ϕn ∈ L(C), se ϕi ∈ X (para i = 1, . . . , n) então c(ϕ1, . . . , ϕn) ∈ X. Então conclúımos que X = L(C). Demonstração: Por definição temos que X ⊆ L(C). Uma vez que L(C) é o menor conjunto de expressões sobre C com as propriedades 1 e 2 satisfeitas por X (veja Definição 2.1.3) inferimos que L(C) ⊆ X, e dáı X = L(C). Quando este teorema é aplicado para provar alguma propriedade de proposições, dizemos que se trata de uma prova por indução nas proposições. Observe que uma formulação equivalente do Teorema 2.1.8 é a seguinte: Teorema 2.1.9. Seja P uma propriedade. Suponha o seguinte: 1. P (p) vale para toda proposição atômica p; 2. para todo n ∈ N, c ∈ Cn e ϕ1, . . . , ϕn ∈ L(C), se P (ϕi) vale (para i = 1, . . . , n) então P (c(ϕ1, . . . , ϕn)) vale. Então conclúımos que P (ϕ) vale para toda sentença ϕ de L(C). Veremos a seguir algumas aplicações do Teorema 2.1.8 que nos ajudarão a entender as caracteŕısticas das linguagens L(C). Um resultado impor- tante a ser provado é com relação à unicidade da escrita das fórmulas: se 21 Demonstração: Considere o seguinte conjunto de sentenças: X = {ϕ ∈ L(C) : existe um único s ∈ S tal que f(ϕ) = s}. Claramente V ⊆ X, pois a primeira cláusula (e apenas ela) se aplica a cada variável p ∈ V. Seja c ∈ Cn e ϕ1, . . . , ϕn ∈ X. Dado que existe um único valor si = f(ϕi) para cada i = 1, . . . , n, e dado que c(ϕ1, . . . , ϕn) admite uma escrita única (pela Proposição 2.1.12) então existe um único valor designado para c(ϕ1, . . . , ϕn) por f , dado por f(c(ϕ1, . . . , ϕn)) = Hc(s1, . . . , sn). Portanto c(ϕ1, . . . , ϕn) ∈ X. Pelo Teorema 2.1.8 temos que X = L(C). Isto prova que existe ao menos uma função f : L(C) → S satisfazendo as propriedades do enunciado do teorema. Provaremos agora que a função f é de fato única. Para isso, suponhamos que g : L(C) → S é uma função que satisfaz as propriedades do enunciado. Considere o conjunto Y = {ϕ ∈ L(C) : f(ϕ) = g(ϕ)}. É imediato que, pelo Teorema 2.1.8, Y = L(C) (deixamos os detalhes da prova para o leitor), portanto g = f . Isto conclui a prova do teorema. 2.1.3 A linguagem da LPC Os resultados apresentados até agora são gerais e valem para qualquer lin- guagem da forma L(C). Vamos agora nos concentrar em três assinaturas particulares, que usaremos daqui em diante, sendo que cada uma delas é suficiente para descrever a lógica proposicional clássica (de aqui em diante, abreviada por LPC). As assinaturas são C0, C1 e C2, descritas nos exem- plos 2.1.4, 2.1.5 e 2.1.6, respectivamente. Como um exemplo de aplicação do Teorema 2.1.15, definimos a função grau de uma proposição. Considere Max(X) como sendo o máximo do conjunto X (com relação a uma ordem dada; veja o Caṕıtulo 5). Então definimos o seguinte: Definição 2.1.16. A função grau é a função g : Prop → N definida como segue: 1. g(ϕ) = 0, se ϕ é atômica; 2. g(ϕ ∨ ψ) = Max({g(ϕ), g(ψ)}) + 1; 24 3. g(¬ϕ) = g(ϕ) + 1. A partir do Teorema 2.1.15 é imediato que a função g está bem definida, considerando S = N, H(p) = 0 para todo p ∈ V, H¬(x) = x + 1 para todo x ∈ N, e H∨(x, y) = Max({x, y}) + 1. Analogamente, podemos definir outra medida para as fórmulas. Definição 2.1.17. A função complexidade é a função l : Prop→ N definida como segue: 1. l(ϕ) = 1, se ϕ é atômica; 2. l(ϕ ∨ ψ) = l(ϕ) + l(ψ) + 1; 3. l(¬ϕ) = l(ϕ) + 1. De novo, a partir do Teorema 2.1.15 prova-se imediatamente que a função l está bem definida, considerando S = N, H(p) = 1 para todo p ∈ V, H¬(x) = x+ 1 para todo x ∈ N, e H∨(x, y) = x+ y + 1. Observação 2.1.18. Observe que as funções g e l podem ser definidas em qualquer linguagem L(C): para g definimos 1. g(ϕ) = 0, se ϕ ∈ V ∪ C0; 2. g(c(ϕ1, . . . , ϕn)) = Max({g(ϕ1), . . . , g(ϕn)}) + 1. Para l definimos 1. l(ϕ) = 1, se ϕ ∈ V ∪ C0; 2. l(c(ϕ1, . . . , ϕn)) = 1 + n∑ i=1 l(ϕi). Outra função útil a ser definida sobre o conjunto Prop é a função Var, que associa a cada fórmula ϕ o conjunto das variáveis proposicionais que ocorrem na fórmula. Usaremos o śımbolo ℘(X) para denotar o conjunto das partes do conjunto X, isto é, ℘(X) = {Y : Y ⊆ X}. Definição 2.1.19. Definimos a função Var : Prop→ ℘(V) como segue: 1. Var(p) = {p} se p ∈ V; 2. Var(ϕ ∨ ψ) = Var(ϕ) ∪Var(ψ); 25 3. Var(¬ϕ) = Var(ϕ). Claramente a função Var está bem definida, usando o Teorema 2.1.15. Basta tomar S = ℘(V), H(p) = {p} para todo p ∈ V, H¬(X) = X e H∨(X,Y ) = X ∪ Y para todo X,Y ⊆ V. Observação 2.1.20. Novamente a função Var pode ser definida em toda linguagem L(C), substituindo a segunda e a terceira cláusulas da definição acima pela mais geral: Var(c(ϕ1, . . . , ϕn)) = n⋃ i=1 Var(ϕi). Em particular, Var(c) = ∅ se c ∈ C0. A noção de subfórmula de uma fórmula também pode ser definida indu- tivamente: Definição 2.1.21. Definimos a função conjunto de subfórmulas como sendo a função SF : Prop→ ℘(Prop) tal que: 1. SF(ϕ) = {ϕ}, se ϕ é atômica; 2. SF(ϕ ∨ ψ) = SF(ϕ) ∪ SF(ψ) ∪ {ϕ ∨ ψ}; 3. SF(¬ϕ) = SF(ϕ) ∪ {¬ϕ}. É posśıvel provar, por indução na complexidade da fórmula ϕ, que SF(ϕ) está bem definida (deixamos como exerćıcio para o leitor). Os elemen- tos de SF(ϕ) são fórmulas, chamadas subfórmulas de ϕ. A partir desta função podemos definir a função conjunto de subfórmulas estritas da maneira seguinte: SFE : Prop→ ℘(Prop), SFE(ϕ) = SF(ϕ)− {ϕ} (a diferença entre o conjunto X e o conjunto Y será denotada por X − Y ). Os elementos de SFE(ϕ) são chamados de subfórmulas estritas de ϕ. Novamente, as funções SF e SFE existem em toda linguagem L(C), portanto poderemos falar em subfórmula e em subfórmula estrita de uma dada fórmula em qualquer linguagem. Exemplo 2.1.22. p2, p3, p10, ¬p2, ¬p3, (p10 ∨¬p3) e (p10 ∨¬p3)∨¬p2 são todas as subfórmulas de (p10 ∨ ¬p3) ∨ ¬p2. 4 26 2.2 Semântica da LPC 2.2.1 Semântica dos conectivos Na definição da linguagem da LPC (isto é, na definição do conjunto Prop) t́ınhamos como conectivos lógicos apenas os operadores ∨ e ¬. Observe que estes conectivos não têm nenhum significado: são apenas śımbolos, portanto eles não têm o sentido usual de “ou” e “não”. Para que isso aconteça, inter- pretaremos os conectivos ∨ e ¬ utilizando funções (chamadas de funções de verdade), que envolvem os valores de verdade 1 (“verdadeiro”) e 0 (“falso”). Seja 2 o conjunto 2 = {0, 1} dos valores de verdade. Definimos funções − : 2→ 2 e t : 22 → 2 através das seguintes tabelas (adotaremos eventual- mente as mesmas convenções de notação infixa da Seção 2.1 com relação aos operadores binários, escrevendo o operador entre os argumentos): p q p t q 1 1 1 1 0 1 0 1 1 0 0 0 p −p 1 0 0 1 A partir dáı, podemos definir indutivamente o valor de verdade 1 ou 0 de uma proposição a partir do valor de suas componentes atômicas. For- malmente, definimos uma função valoração v : Prop→ 2 como segue: Definição 2.2.1. Uma função v : Prop → 2 é uma valoração (clássica) se satisfaz o seguinte: 1. v(ϕ ∨ ψ) = t(v(ϕ), v(ψ)); 2. v(¬ϕ) = −(v(ϕ)). Observação 2.2.2. Note que sempre é posśıvel definir valorações, por causa do Teorema 2.1.15. Com efeito, basta considerar uma função v0 : V → 2 arbitrária. Usando o Teorema 2.1.15 e as funções ∨ e ¬ definidas pelas tabelas-verdade acima, temos que existe uma única valoração v : Prop → 2 estendendo v0, isto é, tal que v(p) = v0(p) para toda variável proposicional p. A partir desta observação vemos que uma valoração é determinada pelos valores que ela toma nas variáveis proposicionais, isto é: 29 Proposição 2.2.3. Se v e v′ são duas valorações que coincidem em V (ou seja, tais que v(p) = v′(p) para toda p ∈ V) então v(ϕ) = v′(ϕ) para toda ϕ ∈ Prop, portanto v = v′. Demonstração: Imediata, usando o Teorema 2.1.15. Graças à Proposição 2.2.3 vemos que, para definir uma valoração, basta dar uma função v0 : V → 2. Por outro lado, podemos refinar este resultado, mostrando que o valor de verdade v(ϕ) dado a uma fórmula ϕ por uma valoração v depende apenas dos valores de verdade v(p) das variáveis p que ocorrem em ϕ. Proposição 2.2.4. Seja ϕ uma fórmula. Se v e v′ são duas valorações tais que v(p) = v′(p) para toda p ∈ Var(ϕ) então v(ϕ) = v′(ϕ). Demonstração: Por indução na complexidade n = l(ϕ). Se n = 1 então ϕ ∈ V e o resultado vale trivialmente. Suponha que, dado n ≥ 1, o resultado vale para toda sentença ϕ tal que l(ϕ) ≤ n, e seja ϕ tal que l(ϕ) = n+ 1. Temos dois casos para analisar: Caso 1: ϕ = ¬ψ. Dado que Var(ψ) = Var(ϕ) então v e v′ coincidem em todas as variáveis de ψ, sendo que l(ψ) = n. Portanto, v(ψ) = v′(ψ), donde v(¬ψ) = −(v(ψ)) = −(v′(ψ)) = v′(¬ψ). Caso 2: ϕ = (ψ ∨ γ). Dado que Var(ψ) ⊆ Var(ϕ) então v e v′ coincidem em todas as variáveis de ψ, sendo que l(ψ) ≤ n. Portanto, v(ψ) = v′(ψ). Analogamente provamos que v(γ) = v′(γ) e então v(ψ∨γ) = t(v(ψ), v(γ)) = t(v′(ψ), v′(γ)) = v′(ψ ∨ γ). Isto conclui a demonstração. Observação 2.2.5. Podemos caracterizar as valorações da maneira seguinte: uma valoração é uma função v : Prop→ 2 satisfazendo o seguinte: 1. v(ϕ ∨ ψ) = { 1 se v(ϕ) = 1 ou v(ψ) = 1 0 caso contrário 2. v(¬ϕ) = { 1 se v(ϕ) = 0 0 se v(ϕ) = 1 As definições semânticas (isto é, através de tabelas-verdade) da negação e da disjunção correspondem com as nossas intuições: dadas duas proposições P e Q (na linguagem natural), então a proposição composta “P ou Q” deve ser verdadeira se uma delas (ou as duas) são verdadeiras, e deve ser falsa se as duas componentes P e Q são falsas. Isto é descrito pela função de 30 verdade t definida acima. Por outro lado, a proposição “não P” (ou “não é o caso que P” ) é verdadeira se P é falsa, e vice-versa. Este comportamento é representado pela tabela da função − definida acima. É claro que existem outros conectivos na linguagem natural que podem ser modelados (de maneira simplista) através de tabelas-verdade. Os conec- tivos que analisaremos semanticamente a seguir são os que correspondem com a assinatura proposicional C2 (veja Exemplo 2.1.6). A conjunção u : 22 → 2 e a implicação material A: 22 → 2 são definidas através das seguintes tabelas-verdade: p q p u q 1 1 1 1 0 0 0 1 0 0 0 0 p q p A q 1 1 1 1 0 0 0 1 1 0 0 1 Observe que a tabela da conjunção coincide com as nossas intuições com relação à conjunção de duas proposições: a conjunção “P e Q” é verdadeira apenas no caso em que ambas componentes, P e Q, o são. Por outro lado, a implicação material é mais complicada de justificar. Em prinćıpio, pode-se pensar que a noção de implicação esta relacionada com a noção de causa- efeito: dizer que “P implica Q” sugere que P é uma causa para Q. Esta leitura surge, por exemplo, quando são enunciadas leis ou regras da forma “Se P , então Q” (por exemplo, na f́ısica). Esta leitura pressupõe portanto uma relação entre os antecedente P e o consequente Q. A interpretação que é feita em lógica clássica da implicação é diferente: trata-se apenas da preservação da verdade. Assim, afirmar que “P implica Q” nada mais diz do que a verdade de P garante a verdade de Q. Para ser mais expĺıcito, uma implicação é verdadeira se, toda vez que o antecedente é verdadeiro, então o consequente também o é. Assim, uma frase do tipo ‘Roma é a capital de Itália implica que Brasil está situado na América do sul’ deve ser con- siderada verdadeira, do ponto de vista da lógica clássica (e no atual estado das coisas), dado que a verdade do antecedente é mantida no consequente. Em outras palavras, uma implicação material “P implica Q” é falsa (numa dada situação) quando o antecedente P é verdadeiro mas o consequente Q é falso. Nessa situação, não é o caso que a verdade de P foi preservada por Q. A definição de implicação impõe que um antecedente falso implique qualquer proposição (verdadeira ou falsa), uma vez que não é o caso que 31 Definição 2.2.7. Dizemos que duas fórmulas ϕ e ψ são semanticamente equivalentes, e o denotamos por ϕ ≡ ψ, se, para toda valoração v, v(ϕ) = v(ψ). A relação ≡ é, de fato, uma relação de equivalência, isto é, ela é reflexiva, simétrica e transitiva (estas e outras relações serão estudadas no Caṕıtulo XXX): • ϕ ≡ ϕ para toda ϕ (reflexiva); • ϕ ≡ ψ implica ψ ≡ ϕ, para toda ϕ,ψ (simétrica); • ϕ ≡ ψ e ψ ≡ γ implica ϕ ≡ γ, para toda ϕ,ψ, γ (transitiva). Exemplo 2.2.8. Temos que (ϕ ∨ ψ) ≡ (ψ ∨ ϕ) e ¬¬ϕ ≡ ϕ para toda ϕ,ψ. 4 O mais importante subconjunto de Prop é o daquelas proposições ϕ que são sempre verdadeiras para quaisquer valorações: Definição 2.2.9. Seja ϕ ∈ Prop. Dizemos que ϕ é uma tautologia se v(ϕ) = 1 para toda valoração v. As tautologias são verdades lógicas: são proposições tais que, indepen- dentemente do valor de verdade atribuido às suas componentes, recebem o valor 1 (verdadeiro). Uma maneira muito natural de determinar se uma proposição é uma tautologia é utilizando tabelas-verdade. Com efeito, a partir da Proposição 2.2.4, vemos que o valor de verdade de uma sentença ϕ depende exclusivamente dos valores atribúıdos às variáveis que ocorrem em ϕ. Portanto, basta analisar todas as posśıveis atribuições de valores de ver- dade 0 e 1 às variáveis que ocorrem em ϕ, combinando, para cada atribuição, os valores das variáveis (e posteriormente das sub-fórmulas) de ϕ de acordo com a função de verdade correspondente ao conectivo sendo utilizado. Exemplo 2.2.10. Utilizando a representação definida acima dos conectivos de C2 na assinatura C0, vemos que as sentenças p0 ∨ ¬p0, (p0 ∧ p1)⇒ p1 e p0 ⇒ (¬p0 ⇒ p1) são tautologias: p0 ¬p0 p0 ∨ ¬p0 1 0 1 0 1 1 p0 p1 p0 ∧ p1 (p0 ∧ p1)⇒ p1 1 1 1 1 1 0 0 1 0 1 0 1 0 0 0 1 34 p0 p1 ¬p0 ¬p0 ⇒ p1 p0 ⇒ (¬p0 ⇒ p1) 1 1 0 1 1 1 0 0 1 1 0 1 1 1 1 0 0 1 0 1 Por outro lado, as sentenças (p0 ∨ p1)⇒ p1 e ((p0 ⇒ p1)∧ p1)⇒ p0 não são tautologias: p0 p1 p0 ∨ p1 (p0 ∨ p1)⇒ p1 1 1 1 1 1 0 1 0 0 1 1 1 0 0 0 1 p0 p1 p0 ⇒ p1 (p0 ⇒ p1) ∧ p1 ((p0 ⇒ p1) ∧ p1)⇒ p0 1 1 1 1 1 1 0 0 0 1 0 1 1 1 0 0 0 1 0 1 No primeiro caso, qualquer valoração v tal que v(p0) = 1 e v(p1) = 0 produz v((p0 ∨ p1) ⇒ p1) = 0, portanto existem valorações que tornam a fórmula ϕ = (p0 ∨ p1) ⇒ p1 falsa, logo ϕ não é tautologia. Por outro lado, toda valoração v tal que v(p0) = 0 e v(p1) = 1 produz v(((p0 ⇒ p1)∧p1)⇒ p0) = 0, portanto esta sentença não é uma tautologia. Esta fórmula representa uma conhecida falácia, a falácia de afirmação do consequente. 4 Um dos problemas mais dif́ıceis que teremos que enfrentar é saber quando uma fórmula é uma tautologia. Além do método da tabela-verdade que acabamos de descrever (e que pode ser considerado um método sintético) 35 há também outros métodos de tipo anaĺıtico, como o Método de Redução ao Absurdo. Neste método partimos da suposição de que a fórmula ϕ a ser testada toma o valor 0 em alguma valoração v e, utilizando as propriedades das valorações, tentamos chegar a um absurdo. Por exemplo, suponhamos que queremos determinar se a fórmula γ = (ϕ ⇒ ψ) ⇒ (¬ψ ⇒ ¬ϕ) é tautologia. Supomos, por redução ao absurdo, que v(γ) = 0 para alguma valoração v; então: 1. (a) v(ϕ⇒ ψ) = 1, (b) v(¬ψ ⇒ ¬ϕ) = 0 2. v(¬ψ) = 1, v(¬ϕ) = 0 (de 1(b)) 3. v(ψ) = 0, v(ϕ) = 1 (de 2) 4. v(ϕ⇒ ψ) = 0 (de 3) Vemos que 4 contraria 1(a), absurdo. Em geral, uma fórmula com n componentes atômicos necessita uma tabela com 2n linhas para decidir se é ou não uma tautologia. Isto significa que se uma fórmula tem n+ 1 variáveis então devemos analisar 2n+1 = 2.2n linhas. Ou seja: acrescentar apenas uma variável implica em duplicar o esforço de testar a validade da fómula! Existiria uma maneira mais rápida de se testar tautologias? A resposta a tal questão coincide com a solução do problema P = NP , um dos mais dif́ıceis problemas da computação teórica. Pode-se demonstrar que a complexidade computacional de qualquer algoritmo se reduz a testar tautologias numa tabela-verdade. Dessa forma, se consegúıssemos provar que não existe uma maneira mais eficiente de testar todas as tautologias, ou se conseguirmos um tal método eficiente, teŕıamos resolvido um problema extremamente sofisticado. O conceito dual de tautologia é o de contradição: Definição 2.2.11. Seja ϕ ∈ Prop. Dizemos que ϕ é uma contradição se v(ϕ) = 0 para toda valoração v. As tautologias são falsidades lógicas: são proposições tais que, indepen- dentemente do valor de verdade atribúıdo às suas componentes, recebem o valor 0 (falso). Será que tem alguma relação (ou alguma maneira de relacionar) as tau- tologias e as contradições? A resposta é afirmativa: a relação de dualidade é realizada através da negação ¬, como mostra o seguinte resultado: 36 ϕij =  qj se qj recebe o valor 1 na linha Li ¬qj caso contrário Considere agora, para cada i = 1, . . . , k, a cláusula ϕi = n∧ j=1 ϕij . Final- mente, definimos ψ = k∨ i=1 ϕi. Resta provar que ϕ ≡ ψ (pois, claramente, ψ está em FND). Seja então v uma valoração tal que v(ϕ) = 1. Logo, v corresponde a uma das linhas, digamos Li, da tabela-verdade construida para ϕ. Por construção dos literais ϕij , temos que v(ϕ i j) = 1 para todo j = 1, . . . , n. Com efeito, se v(qj) = 1 então ϕij = qj , portanto v(ϕ i j) = 1. Por outro lado, se v(qj) = 0 então ϕij = ¬qj , portanto v(ϕij) = 1. Assim sendo, temos que v(ϕi) = 1, pois ϕi consiste da conjunção dos ϕij com j = 1, . . . , n. Portanto, v(ψ) = 1, pois ψ é uma disjunção de formulas, dentre elas ϕi, sendo que v(ϕi) = 1. Reciprocamente, suponha que v uma valoração tal que v(ψ) = 1. Pela definição da tabela da disjunção, debe existir ao menos um ı́ndice i tal que v(ϕi) = 1, portanto v(ϕij) = 1 para todo j = 1, . . . , n (pela definição da tabela da conjunção). Dai inferimos que o valor dado por v para as variáveis q1, . . . , qn coincide com o valor dado para elas na linha Li da tabela-verdade de ϕ, pela construção dos literais ϕij . Portanto o valor de ϕ (na linha Li) coincide com v(ϕ), pela Proposição 2.2.4. Logo, v(ϕ) = 1, pois Li é uma das linhas em que ϕ recebe o valor 1. Daqui ϕ ≡ ψ, concluindo a demonstração. Exemplo 2.2.16. Acharemos uma FND para ϕ = (p2 ∨ p3)⇒ (p1 ∧ p3). 39 p1 p2 p3 p2 ∨ p3 p1 ∧ p3 (p2 ∨ p3)⇒ (p1 ∧ p3) 1 1 1 1 1 1 1 1 0 1 0 0 1 0 1 1 1 1 1 0 0 0 0 1 0 1 1 1 0 0 0 1 0 1 0 0 0 0 1 1 0 0 0 0 0 0 0 1 L1 L2 L3 L4 Temos que as linhas relevantes são L1 (a primeira linha), L2 (a terceira), L3 (a quarta) e L4 (a oitava). Definimos, para cada uma delas, as seguintes cláusulas: 1. Para L1 : ϕ1 = p1 ∧ p2 ∧ p3; 2. Para L2 : ϕ2 = p1 ∧ ¬p2 ∧ p3; 3. Para L3 : ϕ3 = p1 ∧ ¬p2 ∧ ¬p3; 4. Para L4 : ϕ4 = ¬p1 ∧ ¬p2 ∧ ¬p3. Finalmente, definimos ψ = ∨4 i=1 ϕi como sendo uma FND para ϕ. 4 Existe uma outra forma normal para as fórmulas, dual da FND (no sentido de ser uma conjunção de disjunção de literais, em vez de ser uma disjunção de conjunção de literais como na FND). Esta forma normal chama- se de forma normal conjuntiva. Definição 2.2.17. (i) Uma cláusula dual é uma fórmula ϕ da forma ϕ = n∨ i=1 ψi onde cada ψi é um literal. (iii) Dizemos que uma fórmula ϕ está em forma normal conjuntiva (FNC) se ϕ é da forma ϕ = n∧ i=1 ϕi onde cada ϕi é uma cláusula dual (i = 1, . . . , n). 40 A partir da existência da FND para toda fórmula, podemos provar a existência da FNC para toda fórmula: Proposição 2.2.18. Toda fórmula de Prop2 admite uma forma normal con- juntiva. Isto é, existe uma fórmula ψ, nas mesmas variáveis que ϕ, tal que ψ está em FNC, e ϕ ≡ ψ. Mais ainda, existe um algoritmo para calcular uma FNC ψ para ϕ. A demonstração da Proposição 2.2.18 (a partir da Proposição 2.2.15) é deixada para o leitor como exerćıcio. 2.2.4 Conjuntos adequados de conectivos Observe que a FND associada a ϕ utiliza apenas as funções t, u e −. Isto significa que qualquer função de verdade f : 2n → 2 pode ser representada utilizando estas três funções: basta repetir o algoritmo descrito na prova da Proposição 2.2.15. Dado que as funções de verdade são representadas no ńıvel da linguagem por conectivos, podemos dizer que esta é uma pro- priedade de conectivos, ou seja: existem conectivos capazes de representar qualquer função de verdade. Definição 2.2.19. Um conjunto S de conectivos é dito um conjunto ade- quado de conectivos se as funções de verdade associadas a eles bastam para representar qualquer outra função de verdade. Com essa definição, o conjunto {¬,∨,∧} é adequado. Mais ainda, dado que a conjunção pode ser representada em termos de − e t através da equação pu q = −(−pt−q), vemos que {¬,∨} é um conjunto adequado de conectivos. Proposição 2.2.20. {¬,∨} é um conjunto adequado de conectivos. Demonstração: Dada uma função de verdade f(q1, . . . , qn), considere uma FND ψ = ∨n i=1 ϕi associada a f seguindo o algoritmo da demonstração da Proposição 2.2.15. Se substitúımos iteradamente em cada cláusula ϕi =∧n j=1 ϕ i j cada conjunção pela fórmula que utiliza apenas ∨ e ¬ que a rep- resenta (usando a equação p u q = −(−p t −q)), obteremos uma fórmula γi equivalente a ϕi, mas que utiliza apenas ∨ e ¬. Portanto, a disjunção∨n i=1 γi é uma fórmula que representa f , e que apenas utiliza os conectivos ¬ e ∨. 41 2.2.5 Conseqüência semântica A partir das definições dadas até agora, podemos finalmente definir for- malmente uma noção de inferência (ou de conseqüência) lógica. Dado que utilizaremos recursos semânticos para definir esta noção de conseqüência, diremos que trata-se de uma relação de conseqüência semântica. Definição 2.2.28. Seja Γ um conjunto de proposições em Prop, e seja ϕ ∈ Prop. Diremos que ϕ é conseqüência semântica de Γ, e o denotaremos Γ |= ϕ, se para toda valoracao v, temos o seguinte: se v(ψ) = 1 para todo ψ ∈ Γ então v(ϕ) = 1. Se Γ |= ϕ não vale, escrevemos Γ 6|= ϕ. Um caso particular interessante da definição anterior é quando Γ = ∅. Proposição 2.2.29. ∅ |= ϕ se e somente se ϕ é tautologia. Demonstração: Observe que ∅ |= ϕ sse, para toda valoração v, se v(ψ) = 1 para todo ψ ∈ ∅ então v(ϕ) = 1. Assumamos que ϕ é conseqüência semântica de ∅. Observe que v(ψ) = 1 para todo ψ ∈ ∅ sse para toda ψ, se ψ ∈ ∅ então v(ψ) = 1. Dado que é imposśıvel exibir uma sentença ψ tal que ψ ∈ ∅ e v(ψ) 6= 1 (sim- plesmente porque não tem sentenças no conjunto vazio) então é imposśıvel que a frase “se ψ ∈ ∅ então v(ψ) = 1” seja falsa para alguma sentença ψ. Portanto, para toda ψ, se ψ ∈ ∅ então v(ψ) = 1 ou, equivalentemente, “v(ψ) = 1 para todo ψ ∈ ∅” é verdadeira, para toda valoração v. Daqui, de “se v(ψ) = 1 para todo ψ ∈ ∅ então v(ϕ) = 1” inferimos que v(ϕ) = 1, e isto vale para toda valoração v. Isto é, ∅ |= ϕ implica que v(ϕ) = 1 para toda valoração v. Mas isto significa que ϕ é uma tautologia, pela Definição 2.2.9. A rećıproca é trivialmente verdadeira. 44 Escreveremos ψ1, ψ2, . . . , ψn |= ϕ para denotar {ψ1, ψ2, . . . , ψn} |= ϕ. Em particular, escreveremos ψ |= ϕ em lugar de {ψ} |= ϕ, e |= ϕ em lugar de ∅ |= ϕ. Utilizaremos também a seguinte notação: Γ, ϕ |= ψ e Γ,∆ |= ϕ denotarão Γ ∪ {ϕ} |= ψ e Γ ∪∆ |= ϕ, respectivamente. Observe que podemos definir noções de conseqüência semântica |=1 e |=2 sobre as linguagens Prop1 e Prop2 utilizando as valorações definidas na Definição 2.2.6, respectivamente. Porém, o fato de {∨,¬} ser adequado mostra que estas relações de conseqüência podem ser representadas por |=, utilizando as representações dos conectivos em função de {∨,¬} que vimos anteriormente. Este fato será usado a partir de agora sem menção expĺıcita. Exemplos 2.2.30. 1. ϕ,ψ |= ϕ ∧ ψ; 2. ϕ,ϕ⇒ ψ |= ψ; 3. ϕ,¬ϕ |= ψ, para ψ qualquer; 4. |= ϕ⇔ ¬¬ϕ. 4 As principais propriedades da relação de conseqüência semântica são as seguintes: Teorema 2.2.31. A relação de conseqüência |= satisfaz o seguinte: 1. ϕ |= ϕ (reflexividade); 2. Se |= ϕ então Γ |= ϕ; 3. Se ϕ ∈ Γ então Γ |= ϕ; 4. Se Γ |= ϕ e Γ ⊆ ∆ então ∆ |= ϕ; 5. Se Γ |= ϕ e ϕ |= ψ então Γ |= ψ (transitividade) 6. Se Γ |= ϕ e ∆, ϕ |= ψ então Γ,∆ |= ψ (corte); 7. Se Γ, ϕ |= ψ e Γ |= ϕ então Γ |= ψ; 8. |= ϕ see, para todo Γ 6= ∅, Γ |= ϕ; 9. Γ, ϕ |= ψ see Γ |= ϕ⇒ ψ (Teorema de Dedução, forma semântica); 45 10. Γ ∪ {ϕ1, . . . , ϕn} ` ϕ see Γ |= ϕ1 ⇒ (ϕ2 ⇒ (ϕn ⇒ ϕ) . . .); 11. Γ ∪ {ϕ1, . . . , ϕn} ` ϕ see Γ |= (ϕ1 ∧ . . . ∧ ϕn)⇒ ϕ. Demonstração: Provaremos somente (8), deixando o resto da prova como exerćıcio para o leitor: (→ ) Segue de (2). (← ) Se Γ |= ϕ para todo Γ 6= ∅ então, em particular, ¬ϕ |= ϕ. Se existir uma valoração v tal que v(ϕ) = 0 então v(¬ϕ) = 1, portanto v(ϕ) = 1, pela definição de |=, absurdo. Portanto v(ϕ) = 1 para toda valoração v, isto é, |= ϕ. É muitas vezes bastante conveniente substituir as partes atômicas de alguma fórmula por outras proposições. Por exemplo, se |= p⇒ ¬¬p (para p ∈ V), é claro que deve valer |= (ψ1 ∧ ψ2)⇒ ¬¬(ψ1 ∧ ψ2). Essa idéia é formalizada assim: escrevemos ϕ[ψ/p] para a proposição obtida trocando-se todas as ocorrências da variável p em ϕ por ψ. Definição 2.2.32. Dada uma variável proposicional p e uma proposição ψ, definimos por recursão uma função substituição de ψ em lugar de p como a função Subsψp : Prop→ Prop tal que: 1. Subsψp (q) = { q se q ∈ V e q 6= p; ψ se q ∈ V e q = p 2. Subsψp (ϕ1 ∨ ϕ2) = Subsψp (ϕ1) ∨ Subsψp (ϕ2); 3. Subsψp (¬ϕ1) = ¬Subsψp (ϕ1). Escreveremos ϕ[ψ/p] no lugar de Subsψp (ϕ). A partir do Teorema 2.1.15 prova-se imediatamente que a função Subsψp está bem definida, considerando S = Prop, H¬(ϕ) = ¬ϕ, H∨(ϕ1, ϕ2) = ϕ1 ∨ ϕ2, e H(q) = { q se q 6= p; ψ se q = p Provaremos a seguir uma importante propriedade da relação de con- seqüência semântica |=, a saber: o resultado de substituir componentes atômicos por partes semanticamente equivalentes produz fórmulas seman- ticamente equivalentes. Por exemplo, seja ψ1 = (p1 ∧ p2) e ψ2 = (¬(p1 ⇒ ¬p2)). Como ψ1 ≡ ψ2, então ϕ[ψ1/p] ≡ ϕ[ψ2/p] para qualquer fórmula ϕ. 46 Caṕıtulo 3 Axiomática e Completude 3.1 Métodos de Dedução O método de dedução (ou prova) mais antigo que se conhece está ligado às demonstrações em Geometria, expostas nos 13 volumes dos Elementos de Euclides. Baseia-se na idéia de que uma prova deve começar de pontos iniciais chamados axiomas, e proceder por um mecanismo de śıntese, gerando os teoremas através das regras de inferência. Esta forma de proceder foi chamada de método axiomático ou também método hilbertiano, devido ao lógico e matemático alemão David Hilbert que iniciou o estudo sistemático dos métodos de prova, sendo o precursor do que mais tarde viria a ser chamada de teoria da prova. Existe um método alternativo de demonstração, baseado na análise das fórmulas (ao contrário do método axiomático). Esse método, conhecido como método dos tableaux anaĺıticos, tem suas ráızes originariamente no estudo de Gerard Gentzen [6], disćıpulo de Hilbert, depois sistematizado nos trabalhos de Beth [1] e Hintikka [7]. Uma versão mais moderna é apresentada no livro de Smullyan [13], já considerado um clássico no asunto. De certa forma, este método pode ser visto como um jogo entre dois parceiros: para demonstrar uma certa fórmula, imaginamos que o primeiro jogador tenta falsificar a fórmula. Se ele não conseguir, então a fórmula não admite contra-exemplos, isto é, não pode ser falsificada. Dessa forma o método é também conhecido como método de prova por rejeição de todo contra-exemplo. O método anaĺıtico, além de extremamente elegante, é muito eficiente 49 do ponto de vista da heuŕıstica, isto é, do ponto de vista da descoberta das provas. Isto é muito importante para a prova automática de teoremas, pois é muito mais fácil programar uma máquina para analisar fórmulas que para gerar teoremas. De um certo modo, a própria linguagem PROLOG e a programação lógica em geral fazem uso de variantes do método anaĺıtico. Com relação a sua capacidade de provar teoremas, ambos os métodos (o método axiomático tradicional e o método anaĺıtico) são equivalentes. Isto significa que qualquer teorema que puder ser demonstrado num deles poderá sê-lo no outro. Vamos verificar que ambos têm suas vantagens e desvanta- gens: o método anaĺıtico é muito mais fácil de utilizar, mas é por outro lado muito mais dif́ıcil quando queremos provar propriedades dos métodos de prova. Começaremos estudando o método axiomático, e no Caṕıtulo 4 apre- sentaremos o método anaĺıtico em detalhes. 3.2 Sistemas Axiomáticos Fixada uma linguagem L(C), a idéia do método axiomático é definir demon- strações de fórmulas a partir de um conjunto dado de premissas. Estas demonstrações são seqüências finitas de fórmulas, cada uma delas sendo justificada pelas regras do sistema, terminando a seqüência com a fórmula que desejavamos demonstrar (caso tenhamos sucesso). As justificativas para colocar uma fórmula na seqüência são três: ou a fórmula é uma das premis- sas dadas ad hoc, ou trata-se de uma fórmula pertencente a um conjunto de fórmulas aceitas a priori pelo sistema (chamadas axiomas), ou ela pode ser obtida de fórmulas anteriores da seqüência por meio de uma relação entre fórmulas dada a priori no sistema; esta relação é uma regra de inferência do sistema. Formalmente: Definição 3.2.1. Seja C uma assinatura. (i) Uma regra de inferência1 sobre C é um conjunto R não vazio tal que R ⊆ {〈{ϕ1, . . . , ϕn}, ϕ〉 : {ϕ1, . . . , ϕn, ϕ} ⊆ L(C)} para algum n ∈ N. Em particular, se Γ = ∅ para todo 〈Γ, ϕ〉 ∈ R (isto é, se n = 0) então R é dita um axioma. (ii) Uma regra R é decid́ıvel se existe um algoritmo para determinar, para 1Estaremos apenas considerando regras de inferência finitárias, isto é, com finitas pre- missas. Existem lógicas com regras infinitárias, mas não serão tratadas neste texto. 50 todo par 〈Γ, ϕ〉, se 〈Γ, ϕ〉 ∈ R ou 〈Γ, ϕ〉 6∈ R.2 (iii) Uma regra R é esquemática se é da forma R = {〈{σ̂(ϕ1), . . . , σ̂(ϕn)}, σ̂(ϕ)〉 : σ é uma substituição} para algum par 〈{ϕ1, . . . , ϕn}, ϕ〉 fixo, chamado de gerador de R. Claramente, uma regra esquemática é decid́ıvel. Observe que uma regra esquemáticaR pode ser (e de fato, será) substitúıda pelo par 〈{ϕ1, . . . , ϕn}, ϕ〉 que a gera. Nesse caso, um par 〈{σ̂(ϕ1), . . . , σ̂(ϕn)}, σ̂(ϕ)〉 será dito uma instância de R; em particular, uma fórmula σ̂(ϕ) obtida por substituição de um axioma esquema 〈∅, ϕ〉 será dita uma instância do axioma. Frequente- mente escreveremos uma regra esquemática na forma ϕ1 . . . ϕn ϕ . Em particular, um axioma esquema 〈∅, ϕ〉 será escrito como ϕ. Definição 3.2.2. Um sistema axiomático S sobre C é um conjunto de regras de inferência sobre C decid́ıveis. Se toda regra de S é esquemática diremos que S é um sistema axiomático esquemático. Se o conjunto S é decid́ıvel então S é dito recursivamente axiomatizável. Definição 3.2.3. Seja S um sistema axiomático sobre uma assinatura C, e Γ∪{ϕ} ⊆ L(C). Uma prova em S de ϕ a partir de Γ é uma seqüência finita ϕ1 · · ·ϕn de fórmulas em L(C) tal que ϕn = ϕ e, para cada 1 ≤ i ≤ n, vale o seguinte: 1. ϕi ∈ Γ; ou 2. existe uma regra R ∈ S e um par 〈Υ, δ〉 ∈ R tal que δ = ϕi, e Υ ⊆ {ϕ1, . . . , ϕi−1}. Se existir uma prova em S de ϕ a partir de Γ escreveremos Γ `S ϕ e diremos que ϕ é uma conseqüência sintática de Γ. Se Γ `S ϕ não vale, escrevemos Γ 6`S ϕ. Se ∅ `S ϕ diremos que ϕ é um teorema de S, e escreveremos simplesmente `S ϕ. Se Γ `S ϕ então os elementos de Γ são chamados de hipóteses. 2Em geral, um conjunto X é decid́ıvel ou recursivo se existe um algoritmo para deter- minar se x ∈ X ou x 6∈ X. Os conceitos de conjuntos, relações e funções decid́ıveis (ou recursivos) serão rigorosamente definidos e analisados no Caṕıtulo XXX. 51 Caso 2: Existe uma substituição σ′ e um axioma ψ em S tal que ϕ = σ̂′(ψ). Considere a substituição σ′′ = σ̂ ◦ σ′. Logo σ̂(ϕ) = σ̂(σ̂′(ψ)) = (σ̂ ◦ σ̂′)(ψ) = σ̂′′(ψ) pelo Lemma 3.2.8. Daqui segue-se o resultado. Suponhamos que o resultado vale para toda ϕ provada em S a partir de Γ em n passos, e suponha que ϕ é provada em S a partir de Γ numa prova ϕ1 · · ·ϕn+1 de n + 1 passos. Então, temos dois casos para analisar a ocorrência de ϕ = ϕn+1 na prova acima: Caso 1: ϕ ∈ Γ ou ϕ = σ̂′(ψ) para algum axioma ψ de S.4 A demonstração é como acima. Caso 2: Existe uma regra 〈{δ1, . . . , δk}, δ〉 em S e uma substituição σ′ tal que σ̂′(δ) = ϕ e {σ̂′(δ1), . . . , σ̂′(δk)} ⊆ {ϕ1, . . . , ϕn}. Logo, para cada 1 ≤ i ≤ k existe 1 ≤ j(i) ≤ n tal que σ̂′(δi) = ϕj(i). Como antes, considerando a substituição σ′′ = σ̂ ◦ σ′ temos que σ̂′′(δi) = σ̂(σ̂′(δi)) (para i = 1, . . . , k). Usando este fato e a hipótese de indução temos que, para i = 1, . . . , k, σ̂(Γ) `S σ̂′′(δi), pois existe uma prova de σ̂′(δi) a partir de Γ de no máximo n passos (a saber, a prova ϕ1 · · ·ϕj(i) se σ̂′(δi) = ϕj(i), com 1 ≤ j(i) ≤ n). Além disso, da regra 〈{δ1, . . . , δk}, δ〉 de S e de σ̂(ϕ) = σ̂′′(δ) inferimos que σ̂′′(δ1), . . . , σ̂′′(δk) `S σ̂(ϕ). Pelo Teorema 3.2.6(e) obtemos σ̂(Γ) `S σ̂(ϕ) como desejado. Isto conclui a demonstração. Notação 3.2.10. Seguindo a prática usual, usaremos metavariáveis para expressar as regras de inferência esquemáticas em casos concretos (como, de fato, já fizemos ao exibir o exemplo de MP acima). Assim, substituire- mos as variáveis proposicionais que ocorrem na regra por metavariáveis que expressam fórmulas arbitrárias. Por exemplo, escreveremos MP ϕ ϕ⇒ ψ ψ no lugar de MP p0 p0 ⇒ p1 p1 . A partir de agora, os sistemas axiomáticos que definiremos serão es- quemáticos, portanto “sistema axiomático” significará “sistema axiomático esquemático”. Além disso, as regras esquemáticas de sistemas axiomáticos concretos serão formuladas utilizando metavariáveis no lugar de variáveis proposicionais. 4A Definição 3.2.3 de prova não impede escrever provas com n passos irrelevantes. 54 3.3 Uma axiomática para a LPC Nesta seção definiremos um sistema axiomático para a LPC usando, como mencionado anteriormente, a linguagem Prop gerada pelos conectivos {¬,∨}. Daqui em diante usaremos as abreviações para os conectivos ⇒, ∧ e ⇔ em função de C0 definidas no caṕıtulo anterior. Definição 3.3.1. O sistema axiomático PC para a LPC consiste dos seguintes axiomas e regras de inferência: (axioma) ¬ϕ ∨ ϕ (expansão) ϕ ϕ ∨ ψ (eliminação) ϕ ∨ ϕ ϕ (associatividade) ϕ ∨ (ψ ∨ γ) (ϕ ∨ ψ) ∨ γ (corte) ϕ ∨ ψ ¬ϕ ∨ γ ψ ∨ γ Denotaremos as regras anteriores por (exp), (elim), (assoc) e (corte), respectivamente. Uma longa lista de teoremas a respeito de teoremas é a seguinte: Teorema 3.3.2. ϕ,¬ϕ ∨ ψ `PC ψ. (Modus Ponens) Demonstração: 1. ϕ (hip.) 2. ϕ ∨ ψ (exp) 3. ¬ϕ ∨ ψ (hip.) 4. ψ ∨ ψ (corte) 5. ψ (elim) 55 Teorema 3.3.3. ϕ ∨ ψ `PC ψ ∨ ϕ. (Comutatividade) Demonstração: 1. ϕ ∨ ψ (hip.) 2. ¬ϕ ∨ ϕ (axioma) 3. ψ ∨ ϕ (corte) Teorema 3.3.4. γ ∨ (ϕ ∨ ϕ) `PC γ ∨ ϕ. Demonstração: 1. γ ∨ (ϕ ∨ ϕ) (hip.) 2. (γ ∨ ϕ) ∨ ϕ (assoc) 3. ϕ ∨ (γ ∨ ϕ) (3.3.3) 4. (ϕ ∨ (γ ∨ ϕ)) ∨ γ (exp) 5. γ ∨ (ϕ ∨ (γ ∨ ϕ)) (3.3.3) 6. (γ ∨ ϕ) ∨ (γ ∨ ϕ) (assoc) 7. γ ∨ ϕ (elim) Teorema 3.3.5. (ϕ ∨ ψ) ∨ γ `PC ϕ ∨ (ψ ∨ γ). Demonstração: 1. (ϕ ∨ ψ) ∨ γ (hip.) 2. γ ∨ (ϕ ∨ ψ) (3.3.3 em 1.) 3. (γ ∨ ϕ) ∨ ψ ((assoc) em 2.) 4. ψ ∨ (γ ∨ ϕ) (3.3.3 em 3.) 5. (ψ ∨ γ) ∨ ϕ ((assoc) em 4.) 6. ϕ ∨ (ψ ∨ γ) (3.3.3 em 5.) Teorema 3.3.6. ¬ϕ ∨ γ,¬ψ ∨ γ `PC ¬(ϕ ∨ ψ) ∨ γ. Demonstração: 1. ¬(ϕ ∨ ψ) ∨ (ϕ ∨ ψ) (axioma) 2. (ϕ ∨ ψ) ∨ ¬(ϕ ∨ ψ) (3.3.3) 3. ¬ϕ ∨ γ (hip.) 4. ϕ ∨ (ψ ∨ (¬(ϕ ∨ ψ)) (3.3.5 em 2.) 5. (ψ ∨ ¬(ϕ ∨ ψ)) ∨ γ ((corte) em 4., 3.) 6. ψ ∨ (¬(ϕ ∨ ψ) ∨ γ) (3.3.5 em 5.) 7. ¬ψ ∨ γ (hip.) 8. (¬(ϕ ∨ ψ) ∨ γ) ∨ γ ((corte) em 6., 7.) 9. ¬(ϕ ∨ ψ) ∨ (γ ∨ γ) (3.3.5 em 8.) 10. ¬(ϕ ∨ ψ) ∨ γ (3.3.4 em 9.) Teorema 3.3.7. ϕ ∨ (ψ ∨ γ) `PC ψ ∨ (γ ∨ ϕ). 56 Demonstração: (←) Óbvio, a partir de 3.3.2. (→) Suponha que ψ1ψ2 . . . ψn = ψ seja uma prova de ψ a partir de Γ∪{ϕ}. Mostraremos por indução em n que Γ `PC ϕ⇒ ψ. Se n = 1 então temos dois casos para analisar: Caso 1: Se ψ = σ̂(δ) para um axioma δ e uma substituição σ, ou ψ ∈ Γ. Então Γ `PC ψ e pela regra (exp) e o Teorema 3.3.3, Γ `PC ¬ϕ ∨ ψ, isto é, Γ `PC ϕ⇒ ψ. Caso 2: Se ψ = ϕ. então Γ `PC ϕ⇒ ϕ, pois `PC ϕ⇒ ϕ (usando o axioma ¬ϕ ∨ ϕ). Suponha que para toda prova ψ1ψ2 . . . ψn de ψ a partir de Γ∪{ϕ} em n passos temos que Γ `PC ϕ⇒ ψ, e considere uma prova ψ1ψ2 . . . ψn+1 de ψ a partir de Γ ∪ {ϕ} em n+ 1 passos. Pela hipótese de indução, inferimos que Γ `PC ϕ ⇒ ψi para 1 ≤ i ≤ n. No caso em que ψ = σ̂(δ) para um axioma δ e uma substituição σ, ou ψ ∈ Γ ∪ {ϕ}, a demonstração segue como no caso n = 1. Se ψ é obtido dos ψk anteriores através das regras de derivação, temos vários casos a considerar, dependendo da regra aplicada: (1) Se ψ foi obtido de ψk pela regra (exp), então ψ = δ ∨ γ, e ψk = δ. Como Γ `PC ϕ ⇒ δ, i.e., Γ `PC ¬ϕ ∨ δ então, usando (exp) e o Teorema 3.3.5, temos que Γ `PC ¬ϕ ∨ (δ ∨ γ), isto é, Γ `PC ϕ⇒ (δ ∨ γ). (2) Se ψ foi obtido de ψk pela regra (elim), então ψk = ψ ∨ ψ; a prova é similar ao caso anterior, mas agora usando o Teorema 3.3.4. (3) Se ψ foi obtido de ψk pela regra (assoc), então ψ = (δ ∨ γ) ∨ η, ψk = δ ∨ (γ ∨ η). De novo usamos os teoremas 3.3.2 a 3.3.11. (4) Se ψ foi obtido de ψk e ψj pela regra (corte), então ψ = γ∨η, ψk = δ∨γ, e ψj = ¬δ ∨ η. Por hipótese de indução, Γ `PC ϕ ⇒ (δ ∨ γ) e Γ `PC ϕ ⇒ (¬δ ∨ η). Aplicando os teoremas 3.3.2 a 3.3.11, obtemos: Γ `PC δ ∨ (¬ϕ∨ γ) e Γ `PC ¬δ ∨ (¬ϕ∨ η). Portanto segue Γ `PC (¬ϕ∨ γ)∨ (¬ϕ∨ η), aplicando (corte). Daqui, Γ `PC ¬ϕ ∨ (γ ∨ η) (usando 3.3.11(c)); isto é, Γ `PC ϕ ⇒ (γ ∨ η). Temos então em todos os casos Γ `PC ϕ⇒ ψ, o que completa a indução. Corolário 3.3.15. Γ ∪ {ϕ1, . . . , ϕn} `PC ψ se, e só se, Γ `PC ϕ1 ⇒ (ϕ2 ⇒ (. . .⇒ (ϕn ⇒ ψ) . . .)). Como aplicação imediata do Teorema da Dedução, obtemos o seguinte resultado útil sobre PC: Teorema 3.3.16. (a) Γ, ϕ `PC γ e Γ, ψ `PC γ implica Γ, ϕ ∨ ψ `PC γ. (b) Γ, ϕ `PC γ e Γ,¬ϕ `PC γ implica Γ `PC γ. 59 Demonstração: (a) Dado que Γ, ϕ `PC γ e Γ, ψ `PC γ então Γ `PC ¬ϕ ∨ γ e Γ `PC ¬ψ ∨ γ, pelo Teorema 3.3.14. Pelo Teorema 3.3.6 temos que ¬ϕ ∨ γ,¬ψ ∨ γ `PC ¬(ϕ ∨ ψ) ∨ γ, portanto inferimos que Γ `PC ¬(ϕ∨ψ)∨γ, pelo Teorema 3.2.6(e). Por outro lado, temos que ϕ ∨ ψ,¬(ϕ ∨ ψ) ∨ γ `PC γ pelo Teorema 3.3.2. Daqui Γ, ϕ ∨ ψ `PC γ, pelo Teorema 3.2.6(f). (b) Segue do item (a) e do fato de ¬ϕ ∨ ϕ ser um axioma de PC. 3.4 Completude e Compacidade Nesta seção provaremos dois teoremas important́ıssimos da lógica proposi- cional clássica: o teorema da Completude e o teorema da Compacidade. Como veremos a seguir, ambos resultados estão interrelacionados. Dado que as técnicas para provar estes resultados são interessantes per se, pois elas podem ser generalizadas para provar resultados análogos para outras lógicas (chamadas de não-clássicas), mostraremos duas provas diferentes (ou dois caminhos alternativos para chegar à prova) do Teorema da Com- pletude. Devemos destacar que existem duas noções de completude para um sistema lógico: a completude fraca e a completude forte. A completude fraca de um sistema S diz que |= ϕ implica `S ϕ, para toda fórmula ϕ; isto é, as tautologias (com relação a uma dada semântica) são teoremas de S. Por outro lado, a completude forte de S significa que Γ |= ϕ implica Γ `S ϕ, para todo conjunto de fórmulas Γ ∪ {ϕ}. As noções de correção fraca e forte são as rećıprocas das respectivas noções de completude: S é fracamente (fortemente, respectivamente) correto se `S ϕ (Γ `S ϕ, re- spectivamente) implica que |= ϕ (Γ |= ϕ, respectivamente). Claramente a completude forte de S implica a completude fraca de S, tomando Γ = ∅; o mesmo vale para a correção. No caso da completude, a rećıproca não é ne- cessariamente verdadeira (no caso que a relação de conseqüência semântica |= não seja compacta); assim, um sistema pode ser fracamente completo mas não fortemente completo. Dizemos que |= é compacta se satisfaz o seguinte: Γ |= ϕ sse existe um subconjunto finito Γ0 ⊆ Γ de Γ tal que Γ0 |= ϕ, para todo conjunto de fórmulas Γ∪ {ϕ}. Claramente, o Teorema da Completude Forte (junto com o Teorema da Correção Forte) implica o Teorema da Com- pacidade, pois a noção de conseqüência sintática é claramente finitária por definição (veja Teorema 3.2.6(g)). Por utro lado, a partir do Teorema da 60 Completude Fraca, do Teorema da Compacidade e do Teorema da Dedução obtemos facilmente o Teorema da Completude Forte. Primeiro provaremos o Teorema da Correção. Teorema 3.4.1. (Correção Fraca de PC) Se `PC ϕ então |= ϕ. Demonstração: Por indução no comprimento n de uma prova ϕ1 · · ·ϕn de ϕ em PC. Se n = 1 então ϕ é uma instância do axioma ¬p0 ∨ p0, portanto |= ϕ. Suponha o resultado válido para toda ϕ que admite uma prova de com- primento n, e seja ϕ um teorema demonstrado numa seqüência ϕ1 · · ·ϕn+1 de comprimento n + 1. Por hipótese de indução, cada ϕi (1 ≤ i ≤ n) é uma tautologia. Claramente, dada uma instância de uma regra de PC, se as premissas da instância da regra são tautologias então a conclusão também o é (deixamos esta simples verificação como exerćıcio para o leitor). Portanto ϕn+1, isto é, ϕ, é uma tautologia. Corolário 3.4.2. (Correção Forte de PC) Seja Γ∪ {ϕ} um conjunto de fórmulas de Prop. Se Γ `PC ϕ então Γ |= ϕ. Demonstração: Se Γ `PC ϕ então existe um subconjunto finito {ϕ1, . . . , ϕn} de Γ tal que {ϕ1, . . . , ϕn} `PC ϕ, pelo Teorema 3.2.6(g). Daqui, pelo Corolário 3.3.15, `PC ϕ1 ⇒ (ϕ2 ⇒ (. . . ⇒ (ϕn ⇒ ϕ) . . .)), e então |= ϕ1 ⇒ (ϕ2 ⇒ (. . . ⇒ (ϕn ⇒ ϕ) . . .)), pelo Teorema 3.4.1. Logo, pelo Teorema 2.2.31(10) inferimos que {ϕ1, . . . , ϕn} |= ϕ e então, pelo Teo- rema 2.2.31(4), obtemos que Γ |= ϕ. A primeira prova que daremos do Teorema da Completude Forte é direta, portanto tem como conseqüência imediata o Teorema da Compacidade. Esta prova é devida a Lindembaum-Asser. Para começar, introduzimos alguns conceitos e provamos alguns resultados técnicos prévios. Definição 3.4.3. Seja Γ ∪ {ϕ} um conjunto de fórmulas. Dizemos que Γ é ϕ-saturado (com relação a PC) se as duas condições seguintes são verificadas: 1. Γ 6`PC ϕ; 2. Se ψ 6∈ Γ então Γ, ψ `PC ϕ. Lema 3.4.4. Seja Γ um conjunto ϕ-saturado. Então Γ satisfaz o seguinte, para toda fórmula ψ e γ: (a) ψ ∈ Γ sse Γ `PC ψ; (b) (ψ ∨ γ) ∈ Γ sse ψ ∈ Γ ou γ ∈ Γ; 61 máximo um conjunto finito de sentenças ou, em outras palavras, conjuntos infinitos são desnecessários para a relação de conseqüência semântica (ob- serve que uma versão sintática deste resultado aparece no Teorema 3.2.6(g)). Corolário 3.4.8. (Teorema da Compacidade da LPC) Seja Γ ∪ {ϕ} um conjunto de fórmulas em Prop. Se Γ |= ϕ então existe um subconjunto finito Γ0 de Γ tal que Γ0 |= ϕ. Demonstração: Se Γ |= ϕ então Γ `PC ϕ, pelo Teorema 3.4.6. Daqui, existe um subconjunto finito Γ0 de Γ tal que Γ0 `PC ϕ, pelo Teorema 3.2.6(g). Logo, Γ0 |= ϕ pelo Corolário 3.4.2. É posśıvel dar uma outra formulação equivalente do teorema da compaci- dade, que às vezes resulta útil. Antes de dar uma formulação equivalente da compacidade semântica, precisamos de umas definições e resultados prévios. Definição 3.4.9. Dado um conjunto de fórmulas Γ ⊆ Prop, dizemos que Γ é satisfat́ıvel se existe uma valoração v : Prop → 2 tal que v(ψ) = 1 para toda ψ ∈ Γ. Caso contrário, isto é, se para toda valoração v existe uma fórmula ψ ∈ Γ tal que v(ψ) = 0, então dizemos que Γ é insatisfat́ıvel. Proposição 3.4.10. Seja Γ∪{ϕ} um conjunto de fórmulas em Prop. Então Γ |= ϕ sse Γ ∪ {¬ϕ} é insatisfat́ıvel. Demonstração: Suponha que Γ ∪ {¬ϕ} é satisfat́ıvel. Logo, existe uma valoração v tal que v(ψ) = 1 para toda ψ ∈ Γ, e v(¬ϕ) = 1. Logo, a valoração v é tal que v(ψ) = 1 para toda ψ ∈ Γ, e v(ϕ) = 0, portanto Γ 6|= ϕ. Ou seja: se Γ |= ϕ então Γ∪ {¬ϕ} é insatisfat́ıvel. Reciprocamente, suponha que Γ 6|= ϕ. Logo, existe alguma valoração v tal que v(ψ) = 1 para toda ψ ∈ Γ, e v(ϕ) = 0 (portanto v(¬ϕ) = 1). Logo, o conjunto Γ ∪ {¬ϕ} é satisfat́ıvel. Daqui: se Γ ∪ {¬ϕ} é insatisfat́ıvel então Γ |= ϕ. Proposição 3.4.11. São equivalentes: (a) Para todo subconjunto Γ ∪ {ϕ} de Prop: se Γ |= ϕ então existe um subconjunto finito Γ0 de Γ tal que Γ0 |= ϕ. (b) Para todo subconjunto Γ de Prop: se todo subconjunto finito de Γ é satisfat́ıvel, então Γ é satisfat́ıvel. Demonstração: (a)→ (b): Observe que (b) equivale à seguinte afirmação: 64 (b)′ Para todo subconjunto Γ de Prop: se Γ é insatisfat́ıvel então existe um subconjunto finito Γ0 de Γ tal que Γ0 é insatisfat́ıvel. Provaremos que (a) implica (b)′. Seja então Γ um conjunto insatisfat́ıvel; logo, Γ |= ¬(p0 ∨ ¬p0) (isto sai claramente da definição de conseqüência semântica). Usando (a) temos que Γ0 |= ¬(p0 ∨ ¬p0) para algum subcon- junto finito Γ0 de Γ, portanto Γ0 ∪ {¬¬(p0 ∨ ¬p0)} é insatisfat́ıvel, pela Proposição 3.4.10. Mas, dado que ¬¬(p0 ∨ ¬p0) é uma tautologia, então certamente Γ0 é insatisfat́ıvel, sendo que Γ0 é um subconjunto finito de Γ. Isto prova (b)′, portanto (b). (b)→ (a): Observe que, usando a Proposição 3.4.10, temos que (a) equivale ao seguinte: (a)′ Para todo subconjunto Γ ∪ {ϕ} de Prop: se Γ ∪ {¬ϕ} é insatisfat́ıvel, então existe um subconjunto finito Γ0 de Γ tal que Γ0∪{¬ϕ} é insatisfat́ıvel. Podemos ainda reescrever (a)′ da seguinte maneira equivalente: (a)′′ Para todo subconjunto Γ∪{ϕ} de Prop: se para todo subconjunto finito Γ0 de Γ temos que Γ0 ∪ {¬ϕ} é satisfat́ıvel, então Γ ∪ {¬ϕ} é satisfat́ıvel. Provaremos agora que (b) implica (a)′′. Suponha então que para todo sub- conjunto finito Γ0 de Γ temos que Γ0 ∪ {¬ϕ} é satisfat́ıvel, e seja ∆ = Γ ∪ {¬ϕ}. Seja ∆0 ⊆ ∆ finito, e considere Γ0 = ∆0 − {¬ϕ} (note que possivelmente ¬ϕ 6∈ ∆0). Então Γ0 é um subconjunto finito de Γ, portanto Γ0 ∪ {¬ϕ} é satisfat́ıvel, por hipótese. Dado que ∆0 ⊆ Γ0 ∪ {¬ϕ} (a igual- dade vale sse ¬ϕ ∈ ∆0) então inferimos que ∆0 é satisfat́ıvel, e isto vale para todo subconjunto finito ∆0 de ∆. Usando (b) inferimos que ∆ é satisfat́ıvel. Isto prova (a)′′, portanto (a). Daremos agora uma segunda prova construtiva de completude (fraca) do sistema PC (a primeira, não explicitada aqui, é um caso particular da prova da completude forte, para Γ = ∅), baseando-se numa prova proposta por Kálmar em 1935. Lema 3.4.12. Seja ϕ uma fórmula, e q1, . . . , qn as variáveis proposicionais que ocorrem em ϕ. Seja v uma valoração qualquer. Para 1 ≤ i ≤ n defini- mos q?i = { qi se v(qi) = 1 ¬qi se v(qi) = 0 65 e seja ∆ϕ = {q?1, q?2, . . . , q?n}. Então: (i) Se v(ϕ) = 1 então ∆ϕ `PC ϕ, e (ii) Se v(ϕ) = 0 então ∆ϕ `PC ¬ϕ. Demonstração: Por indução na complexidade n de ϕ. Se n = 1 então ϕ é q1, portanto ∆ϕ = {q1} ou ∆ϕ = {¬q1}, e o problema se reduz a mostrar que q1 `PC q1 ou ¬q1 `PC ¬q1, o que é trivialmente verdadeiro. Suponha o resultado válido para toda ϕ com l(ϕ) ≤ n para certo n ≥ 1, e seja ϕ tal que l(ϕ) = n+ 1. Temos dois casos: (1) Se ϕ é ¬ψ. Note que ∆ϕ = ∆ψ. Suponha que v(ϕ) = 1. Então v(ψ) = 0 e por hipótese de indução ∆ψ `PC ¬ψ, isto é, ∆ϕ `PC ϕ. No caso de ter v(ϕ) = 0 então v(ψ) = 1 e pela hipótese de indução ∆ψ `PC ψ. Como ψ `PC ¬¬ψ concluimos que ∆ϕ `PC ¬¬ψ, pelo Teorema 3.2.6(e). (2) Se ϕ é ψ ∨ γ. Então ∆ψ ⊆ ∆ϕ e ∆γ ⊆ ∆ϕ. Suponhamos que v(ϕ) = 1. Então v(ψ) = 1 ou v(γ) = 1. No primeiro caso, pela hipótese de indução, ∆ψ `PC ψ, e dáı ∆ϕ `PC ψ ∨ γ pela regra (exp) e pelo Teorema 3.2.6(d). O segundo caso é análogo. Suponhamos agora que v(ϕ) = 0. Então v(ψ) = v(γ) = 0, e pela hipótese de indução, ∆ψ `PC ¬ψ e ∆γ `PC ¬γ. Em conseqüência, pela regra (exp) e pelo Teorema 3.2.6(d) temos: ∆ϕ `PC ¬ψ ∨ ¬(ψ ∨ γ) e ∆ϕ `PC ¬γ ∨ ¬(ψ ∨ γ). Pelo Teorema 3.3.6, ∆ϕ `PC ¬(ψ ∨ γ) ∨ ¬(ψ ∨ γ) e então ∆ϕ `PC ¬(ψ ∨ γ), pela regra (elim). Teorema 3.4.13. (Completude Fraca de PC) Seja ϕ uma fórmula em Prop. Logo, temos que: se |= ϕ então `PC ϕ. Demonstração: Seja ϕ uma tautologia; então v(ϕ) = 1 para toda valoração v. Seja Var(ϕ) = {q1, . . . , qn} o conjunto das variáveis proposicionais que ocorrem em ϕ. Considere duas valorações v1 e v2 tais que v1 atribui 1 a todas as variáveis proposicionais de ϕ e v2 atribui 1 a todas, exceto a qn, isto é, v2(qn) = 0. Pelo lema anterior, temos: {q1, q2, . . . , qn} `PC ϕ e {q1, q2, . . . ,¬qn} `PC ϕ. Pelo Teorema 3.3.16(b) obtemos (∗) {q1, q2, . . . , qn−1} `PC ϕ. 66 Pode-se também demonstrar que o sistema CR é equivalente ao sistema PC (e a todos os outros) no sentido seguinte: `cr {ϕ1, . . . , ϕn} sse `PC∨n i=1 ϕi. O sistema CR é muito interessante pela seguinte razão: nele a Regra do Corte pode ser eliminada. A primeira situação desse tipo foi demon- strada por G. Gentzen, num teorema conhecido como Hauptsatz (veja o Teo- rema 4.3.4), com conseqüências profundas para os fundamentos da matemática. Finalizamos esta seção mencionando um teorema importante (e sur- preendente) da lógica proposicional, o Teorema da Interpolação de Craig: Teorema 3.5.3. (Teorema da Interpolação de Craig) Sejam ϕ1, ϕ2 ∈ Prop tais que ϕ1 não é contradição e ϕ2 não é tautologia. Se |= ϕ1 ⇒ ϕ2, existe ϕ ∈ Prop tal que Var(ϕ) ⊆ Var(ϕ1) ∩ Var(ϕ2), |= ϕ1 ⇒ ϕ e |= ϕ⇒ ϕ2. (A prova de este teorema é deixada como exerćıcio para o leitor.) O que este teorema afirma é que entre cada duas fórmulas separadas por implicação tais que a implicação é um teorema, sempre se pode interpolar outra fórmula ϕ de modo a se obter dois novos teoremas. É interessante observar que uma propriedade semelhante ocorre com os números racionais: entre cada dois racionais pode-se colocar mais um; esta propriedade é chamada densidade. De certa forma, podemos pensar que os teoremas da lógica proposicional formam um conjunto denso. 3.6 Axiomáticas não completas Finalizamos este caṕıtulo mostrando duas axiomatizações não completas da LPC. Estes dois exemplos servirão para mostrar duas coisas: (1) os cuidados que devemos tomar ao tentar axiomatizar uma determinada lógica (no caso, a LPC); e (2) uma técnica que pode ser utilizada para provar que um sistema é incompleto ou, mas geralmente, para provar que uma determinada fórmula não é demonstrável num dado sistema axiomático. Portanto, esta técnica serve também para provar a independência dos axiomas de uma dada ax- iomática, isto é: para provar que o sistema obtido de eliminar um dos seus axiomas não consegue provar o axioma eliminado. Nesta seção , “Completude” e “Correção” referem-se a “Completude Fraca” e “Correção Fraca”, respectivamente. Definição 3.6.1. Considere a assinatura proposicional C4 dada por C40 = {⊥}, C42 = {∨,⇒} e C4n = ∅ nos outros casos. O sistema axiomático P escrito na linguagem L(C4) consiste dos seguintes axiomas e regras de inferência: 69 (Ax1) (ϕ ∨ ϕ)⇒ ϕ (Ax2) ϕ⇒ (ψ ∨ ϕ) (Ax3) (ϕ⇒ ψ)⇒ ((γ ∨ ϕ)⇒ (ψ ∨ γ)) (MP) ϕ ϕ⇒ ψ ψ Definição 3.6.2. Uma valoração para P é uma função v : L(C4) → 2 tal que: 1. v(⊥) = 0; 2. v(ϕ ∨ ψ) = t(v(ϕ), v(ψ)); 3. v(ϕ⇒ ψ) = A(v(ϕ), v(ψ)), onde t : 22 → 2 e A: 22 → 2 são as funções de verdade clássicas (veja Subseção 2.2.1). Observe que a semântica de P coincide com a semântica clássica para os conectivos {⊥,∨,⇒} (um conjunto adequado), portanto as tautologias de P (nesta linguagem e nas linguagens Prop, Prop1 e Prop2, se usarmos as abreviações usuais) são as clássicas. Proposição 3.6.3. O sistema P é correto com relação às suas valorações. Demonstração: Imediata: os axiomas são tautologias clássicas, e a regra (MP) preserva validade: se as premissas são verdadeiras, então a conclusão é também verdadeira. Porém, podemos observar que o sistema P não é completo com relação à sua semântica clássica: Proposição 3.6.4. O sistema P não é completo com relação às suas val- orações. Demonstração: Basta provar que existe uma tautologia (com relação às suas valorações, ou seja, uma tautologia clássica na linguagem L(C4)) que não é demonstrável em P. Considere a fórmula ϕ = (⊥ ⇒ p0). Claramente ϕ é uma tautologia. Provaremos que ϕ não é demonstrável em P usando a 70 técnica seguinte: exibiremos uma semântica alternativa para P que valide seus axiomas e suas regras de inferência (portanto, P será correto para essa semântica alternativa). Porém, ϕ não será uma tautologia com relação a essa semântica, portanto não poderá ser um teorema de P. Considere então a seguinte semântica para P: as valorações são funções como na Definição 3.6.2, mas agora v(⊥) = 1 para toda v. Dado que ⊥ não aparece explicitamente nos axiomas e nas regras de P, vemos que P é correto com relação a esta nova semântica. Mas, claramente, ϕ não é tautologia com relação a esta semântica, pois para qualquer valoração v tal que v(p0) = 0 temos que v(ϕ) = 0. Portanto ϕ não pode ser um teorema de P, pela correção de P com relação a esta semântica. Um motivo óbvio na falha de P para axiomatizar a LPC é a ausência de axiomas e regras governando o śımbolo primitivo ⊥ da linguagem de P. Um fato intuitivo básico com relação à axiomatização de sistemas lógicos é que deveriamos colocar regras e axiomas para cada conectivo declarado na assinatura, caso contrário nos vemos expostos a fenómenos de incompletude como o que acabamos de apresentar. Mas as coisas não são tão fáceis, e mesmo colocando axiomas que repre- sentam as inferências básicas de uma lógica intuitivamente suficientes para gerá-la, podemos ter surpressas. Mostraremos a seguir uma extensão de P acrescentando alguns axiomas para a constante ⊥ e para a negação derivada ¬ϕ := (ϕ ⇒ ⊥), que ainda resultará ser incompleta. A prova de incom- pletude é análoga à prova da Proposição 3.6.4, mas agora utilizaremos uma semântica trivalente, isto é, com três valores de verdade. Definição 3.6.5. O sistema P+ definido sobre L(C4) é a extensão de P obtida pelo acréscimo dos seguintes axiomas a P (onde ¬ϕ denota ϕ⇒ ⊥): (Ax4) ⊥ ⇒ ϕ (Ax5) ϕ⇒ (¬ϕ⇒ ψ) (Ax6) ¬¬ϕ⇒ ϕ (Ax7) ϕ⇒ ¬¬ϕ (Ax8) ¬ϕ ∨ ϕ 71 (b) Se Γ, ψ |= ϕ então Γ |= c(ψ,ϕ); (c) Se Γ `S c(ψ,ϕ) então Γ, ψ `S ϕ; (d) Se |= ϕ então `S ϕ. (i) Prove que S satisfaz a completude forte: se Γ |= ϕ então Γ `S ϕ. (ii) Enuncie condições análogas para provar a correção forte de S a partir da correção fraca de S. Usando essas condições, demonstre a correção forte de S a partir da correção fraca de S. 4. Mostre que os axiomas do sistema M são tautologias, e que a regra de Modus Ponens preserva tautologias. Prove a seguir o Teorema da Correção Fraca de M. 5. Usando o sistema M prove, para cada fórmula ϕ, ψ e γ, o seguinte: (a) ` ϕ⇒ ϕ (b) ` (¬ϕ⇒ ϕ)⇒ ϕ (c) ϕ⇒ ψ,ψ ⇒ γ ` ϕ⇒ γ (d) ϕ⇒ (ψ ⇒ γ) ` ψ ⇒ (ϕ⇒ γ) (e) ` (ϕ⇒ ψ)⇔ (¬ψ ⇒ ¬ϕ) (f) ` ¬¬ψ ⇔ ψ (g) ` ϕ⇒ (¬ψ ⇒ ¬(ϕ⇒ ψ)) (h) ` (ϕ⇒ ψ)⇒ ((¬ϕ⇒ ψ)⇒ ψ) (i) ` ϕ⇒ (ϕ ∨ ψ) (j) ` (ϕ ∧ ψ)⇒ ϕ (k) ` ϕ⇒ (ψ ⇒ (ϕ ∧ ψ)) 6. Mostre que os sistemas PC e CR são equivalentes. 7. Mostre que no sistema PC todos os axiomas e regras são independentes (i.e., retirando-se algum axioma ou regra o sistema não é mais com- pleto). Sugestão: use tabelas trivalentes “esdrúxulas” que modelem todas as regras menos uma delas. 74 8. Considere o sistema axiomático M1 escrito na linguagem Prop1, for- mado pelos seguintes axiomas e regras de inferência: (Axioma 1) ϕ⇒ (ψ ⇒ ϕ) (Axioma 2) (ϕ⇒ (ψ ⇒ γ))⇒ ((ϕ⇒ ψ)⇒ (ϕ⇒ γ)) (Axioma 3) ¬¬ϕ⇒ ϕ (Modus Ponens) ϕ ϕ⇒ ψ ψ Provar que M1 é correto com relação à semântica de valorações clássicas, mas não é completo. Sugestão: use tabelas trivalentes que validem os axiomas e a regra de inferência de M1, mas que não validem a fórmula ϕ⇒ ¬¬ϕ. 9. A partir das axiomas do sistema PC prove as seguintes propriedades da relação de conseqüência sintática (a relação de conseqüência que satisfaz estas propriedades é uma simplificação do Método de Dedução Natural que estudaremos no Caṕıtulo 4): Regras de introdução de conectivos: (a) Se Γ, ϕ ` ψ então Γ ` ϕ⇒ ψ (b) ϕ,ψ ` ϕ ∧ ψ (c) ϕ ` ϕ ∨ ψ e ψ ` ϕ ∨ ψ (d) Se Γ, ϕ ` ψ e Γ, ϕ ` ¬ψ então Γ ` ¬ϕ Regras de eliminação de conectivos: (a) ϕ,ϕ⇒ ψ ` ψ (b) ϕ ∧ ψ ` ϕ e ϕ ∧ ψ ` ψ (c) Se Γ, ϕ ` γ e Γ, ψ ` γ então Γ, ϕ ∨ ψ ` γ (d) ¬¬ϕ ` ϕ 10. Um operador de conseqüência de Tarski é uma operação entre conjun- tos de fórmulas Cn : ℘(L(C)) → ℘(L(C)) satisfazendo as seguintes propriedades: (a) X ⊆ Cn(X); (b) X ⊆ Y implica Cn(X) ⊆ Cn(Y ); (c) Cn(Cn(X)) = Cn(X). 75 Mostre que Cn(Γ) = {ϕ ∈ L(C) : Γ `S ϕ} é um operador de con- seqüência, para todo sistema axiomático S. (O leitor interessado no estudo da lógica através de operadores de conseqüência pode consul- tar o livro [14].) 11. Demonstre o Teorema da Eliminação do corte para CR. Sugestão: use indução na complexidade das demonstrações. Suponha que a regra (Corte), na forma Γ, ϕ Γ,¬ϕ Γ , foi a última a ser usada numa demonstração. Mostre então, por indução na complexidade de ϕ, que (Corte) pode ser eliminada: (i) Para ϕ atômico, conclua que ϕ ∈ Γ e ¬ϕ ∈ Γ logo (Corte) é desnecessária. (ii) Para ϕ da forma ¬ψ, use a hipótese de indução. (iii) Para ϕ da forma ϕ0 ∨ ϕ1 mostre que se `cr Γ,¬(ϕ0 ∨ ϕ1) então `cr Γ,¬ϕ0 e `cr Γ,¬ϕ1. A partir dáı, use a hipótese de indução. 12. Prove o Teorema da Interpolação 3.5.3. Sugestão: Mostre que cada item a seguir é válido e que o procedimento resolve o problema: (a) Pelas hipóteses do teorema, temos que Var(ϕ1) ∩ Var(ϕ2) 6= ∅ (use a Proposição 2.2.4). (b) Tome Γ = {ψ : Var(ψ) ⊆ Var(ϕ1) ∩ Var(ϕ2) e |= ϕ1 ⇒ ψ}. Então Γ é consistente. (c) Temos que Γ |= ϕ2 (use o fato que, se Γ 6|= ϕ2 então Γ ∪ {¬ϕ2} é consistente, e dáı derive uma contradição a partir das hipóteses). (d) Existe Γ0 finito contido em Γ tal que Γ0 |= ϕ2. (e) ϕ = ∧ Γ0 (i.e., a conjunção dos elementos do conjunto finito Γ0) satisfaz a conclusão do teorema. 13. Prove a Proposição 3.6.8. 76 duas maneiras diferentes: aplicá-la com relação a ϕ ∨ ψ ou com relação a γ′ ∨ δ′. Também podemos aplicar a regra R¬∨ com relação a ¬(γ ∨ δ). Seja C = {Σ1,Σ2, . . . ,Σn} uma configuração. O resultado da aplicação de uma regra de análise a C é uma nova configuração C′ = (C − {Σi}) ∪ {∆i1 ,∆i2} (i1 e i2 possivelmente iguais) onde {∆i1 ,∆i2} é o resultado da aplicação de alguma regra de análise a Σi (para algum i ≤ n). Um tablô é uma seqüência {Cn}n∈N (possivelmente estacionária) de con- figurações tal que Cn+1 = Cn ou Cn+1 é obtida de Cn por aplicação de alguma regra de análise, para todo n ∈ N. Um tablô para um conjunto Σ é um tablô {Cn}n∈N tal que C1 = {Σ}. Um conjunto de fórmulas Σ é fechado se existe uma fórmula ϕ tal que ϕ e ¬ϕ pertencem a Σ; uma configuração é fechada se todos seus elementos o forem, e um tablô {Cn}n∈N é fechado se existe n ∈ N tal que Cm = Cn para todo m ≥ n, e Cn é fechada. O caso não-fechado (em qualquer dos itens acima) é dito aberto. Finalmente, dizemos que um tablô está terminado (ou é completo) se uma das três possibilidades acontece: 1. o tablô é fechado; ou 2. o tablô e aberto, não estacionário (isto é, para todo n existe m > n tal que Cm 6= Cn; ou 3. o tablô é aberto, estacionário (isto é, existe n tal que, para todo m > n, Cm = Cn), e não é posśıvel aplicar uma regra na configuração Cn.2 Observe que, se Σ é um conjunto finito de fórmulas, então todo tablô terminado para Σ é finito, isto é, deve terminar (aberto ou fechado) em finitos passos, sendo sempre estacionário. No caso da lógica de primeira ordem, veremos que nem sempre este é o caso. Para facilidade de notação, podemos denotar tablôs utilizando árvores. Introduzimos a seguir os conceitos relativos a árvores. Definição 4.1.2. Uma árvore (enraizada) é uma estrutura A = 〈|A|,R〉 tal que |A| é um conjunto não vazio, e R ⊆ |A|× |A| é uma relação satisfazendo as propriedades seguintes: 1. Existe um único r ∈ |A| tal que (a) não existe x ∈ |A| tal que xRr,3 2Isto significa que os elementos abertos de Cn são conjuntos de literais. 3Se 〈x, y〉 ∈ R escreveremos xRy. 79 (b) se y ∈ |A|, y 6= r, então existe um único z ∈ |A| tal que zRy. 2. R não possui ciclos, isto é, não existem x1, . . . , xn em |A| tais que x1Rx2R · · ·RxnRx1. 3. R não possui descensos infinitos, isto é, não existe uma sequência {xn}n∈N em |A| tal que · · ·xnRxn−1R · · ·Rx2Rx1. Os elementos de |A| são chamados de nós, e o nó r da primeira cláusula é chamado de raiz. Se xRy diremos que y é um sucessor de x, e x é o predecessor de y. Um nó sem sucessores é dito um nó terminal. Uma árvore é finitamente gerada se cada nó tem finitos sucessores. Se cada nó tem no máximo dois sucessores, a árvore é dita diádica. Uma árvore é representada da maneira seguinte: • ~~ ~~ ~~ ~ @@ @@ @@ @ UUUU UUUU UUUU UUUU UUUU • • ~~ ~~ ~~ ~ @@ @@ @@ @ • • • ~~ ~~ ~~ ~ @@ @@ @@ @ • • • • • Definição 4.1.3. Seja A = 〈|A|,R〉 uma árvore com nó raiz r. 1. Uma seqüência finita x1 · · ·xn em |A| é um ramo finito de A se x1 = r, xn é terminal e xiRxi+1 para todo 1 ≤ i ≤ n− 1. 2. Uma seqüência infinita {xn}n∈N em |A| é um ramo infinito de A se x1 = r e xiRxi+1 para todo i ≥ 1. 3. Um ramo de A é um ramo finito ou infinito de A. 80 Observação 4.1.4. Um tablô pode ser representado por árvores diádicas. Assim, cada nó é um conjunto de fórmulas, e as regras de análise produzem sucessores da maneira seguinte: (R∨) produz dois sucessores, Γ, ϕ ∨ ψ uu uu uu uu u II II II II I Γ, ϕ Γ, ψ enquanto que (R¬∨) e (R¬¬) produzem um único sucessor, respectivamente. Γ,¬(ϕ ∨ ψ) Γ,¬ϕ,¬ψ Γ,¬¬ϕ Γ, ϕ É fácil ver que existe uma correspondência biuńıvoca entre seqüências de árvores constrúıdas de acordo com as regras de análise e tablôs. (i) Dado um tablô C1C2 · · ·Cn · · · definimos uma seqüência de árvores A1A2 · · · An · · · da maneira seguinte: 1. A1 é a árvore com apenas um nó (raiz) Σ, se C1 = {Σ}. Note que os elementos da configuração C1 são os nós terminais da árvore A1. 2. Suponha que a árvore An foi constrúıda a partir da configuração Cn tal que os nós terminais de An são exatamente os elementos de Cn. (a) Se Cn+1 é obtido de Cn substituindo um elemento Σ′ de Cn pelo elemento ∆ (resultado da aplicação da regra (R¬∨) ou (R¬¬)) então definimos a árvore An+1 como sendo a árvore An com o acréscimo do nó ∆ como sucessor de Σ′. Note que os elementos da configuração Cn+1 são os nós terminais da árvore An+1. (b) Se Cn+1 é obtido de Cn substituindo um elemento Σ′ de Cn pelos elementos ∆1,∆2 (resultado da aplicação da regra (R∨)) então definimos a árvore An+1 como sendo a árvore An com o acréscimo dos nós ∆1 e ∆2 como sucessores de Σ′. Note que os elementos da configuração Cn+1 são os nós terminais da árvore An+1. 81 (a) ϕ `T ϕ (b) Se `T ϕ então Γ `T ϕ (c) Se ϕ ∈ Γ então Γ `T ϕ (d) Se Γ `T ϕ e Γ ⊆ ∆ então ∆ `T ϕ (e) Γ `T ϕ see existe Γ0 ⊆ Γ, Γ0 finito, tal que Γ0 `T ϕ Demonstração: (a) Existe um tablô fechado para {ϕ,¬ϕ}, esquematizado como uma árvore de um só nó: {ϕ,¬ϕ}. (b) Se existe um tablô fechado para {¬ϕ}, então existe um tablô fechado para Γ ∪ {¬ϕ} (basta acrescentar Γ a cada nó da árvore de {¬ϕ}). (c) Idem (a). (d) Idem (b). (e) Se existe um tablô fechado para Γ ∪ {¬ϕ}, este tablô consiste numa árvore finita, onde as regras foram aplicadas um número finito de vezes. Basta selecionar as fórmulas nas quais as regras se aplicaram e temos um conjunto Γ0 finito tal que Γ0 ⊆ Γ e Γ0 `T ϕ. A rećıproca usa a parte (d). Daremos a seguir alguns exemplos de deduções anaĺıticas, utilizando árvores para visualizar melhor as deduções. Denotamos os ramos fechados por ∗. Exemplo 4.1.7. `T ϕ ⇒ (ψ ⇒ ϕ). Iniciamos uma árvore com ¬(ϕ ⇒ (ψ ⇒ ϕ)) e mostramos que se produz um tablô fechado. ¬(¬ϕ ∨ (¬ψ ∨ ϕ)) ¬¬ϕ,¬(¬ψ ∨ ϕ) ¬¬ϕ,¬¬ψ,¬ϕ ∗ (o ramo fecha em virtude da ocorrência de ¬¬ϕ e ¬ϕ. 4 84 Exemplo 4.1.8. ϕ ∨ ψ,¬ψ `T ϕ. ϕ ∨ ψ,¬ψ,¬ϕ nnn nnn nnn nnn PPP PPP PPP PPP ϕ,¬ψ,¬ϕ ψ,¬ψ,¬ϕ ∗ ∗ 4 Exemplo 4.1.9. ϕ⇒ ψ,ϕ⇒ ¬ψ `T ¬ϕ. ¬ϕ ∨ ψ,¬ϕ ∨ ¬ψ,¬¬ϕ kkkk kkkk kkkk kkk SSSS SSSS SSSS SS ¬ϕ,¬ϕ ∨ ¬ψ,¬¬ϕ ψ,¬ϕ ∨ ¬ψ,¬¬ϕ kkkk kkkk kkkk kk PPP PPP PPP PPP ∗ ψ,¬ϕ,¬¬ϕ ψ,¬ψ,¬¬ϕ ∗ ∗ 4 Note que não demonstramos todas as propriedades do Teorema 3.2.6; por exemplo, para demonstrar que se Γ `T ϕ e ϕ `T ψ então Γ `T ψ precisamos provar uma propriedade mais forte da relação `T , a saber, o análogo para tablôs da regra de modus ponens. Na verdade, precisamos provar uma espécie de contraparte do famoso teorema de Eliminação do Corte de Gentzen (veja o Teorema 4.3.4), para que possamos introduzir a regra de corte no sistema anaĺıtico: Existem tablôs fechados para Γ, ϕ e Γ,¬ϕ see existe um tablô fechado para Γ. Após a introdução desta propriedade, poderemos provar a completude do método anaĺıtico e sua equivalência com o método hilbertiano. A demon- stração deste teorema não é simples, e será feita na próxima subseção. Finalizamos esta subseção com o estudo de regras derivadas. 85 Definição 4.1.10. Seja Γ ⊆ Prop. Dizemos que Γ é T -inconsistente se existe um tablô fechado para Γ. Definição 4.1.11. Uma regra derivada é uma regra anaĺıtica de um dos seguintes tipos. a) uma regra derivada tipo bifurcação consiste de dois pares da forma 〈Γ ∪ {ϕ},Γ ∪ {ϕ1}〉 e 〈Γ ∪ {ϕ},Γ ∪ {ϕ2}〉 tais que Γ é finito, e: 1. ϕ1 e ϕ2 (não necessariamente distintas) são subfórmulas de complexi- dade estritamente menor do que a complexidade de ϕ, e 2. Γ ∪ {ϕ,¬ϕ1,¬ϕ2} é T -inconsistente. Denotamos uma regra derivada desse tipo por Γ, ϕ Γ, ϕ1| Γ, ϕ2 se ϕ1 6= ϕ2, e Γ, ϕ Γ, ϕ1 caso contrário. b) Uma regra derivada do tipo linear é um par da forma 〈Γ∪{ϕ},Γ∪{ϕ1, ϕ2}〉 onde Γ é finito, e: 1. ϕ1 e ϕ2 (não necessariamente distintas) são subfórmulas de complexi- dade estritamente menor do que a complexidade de ϕ, e 2. Γ ∪ {ϕ,¬ϕ1} e Γ ∪ {ϕ,¬ϕ2} são T -inconsistentes. Denotamos uma regra desse tipo por Γ, ϕ Γ, ϕ1, ϕ2 se ϕ1 6= ϕ2, e Γ, ϕ Γ, ϕ1 caso contrário. Exemplo 4.1.12. As seguintes são regras derivadas: 1. Todas as regras do sistema PC. Por exemplo p0 ∨ p0 p0 é uma regra derivada pois {p0 ∨ p0} ∪ {¬p0} é T -inconsistente; de fato, p0 ∨ p0,¬p0 ooo ooo ooo oo OOO OOO OOO OO p0,¬p0 p0,¬p0 ∗ ∗ 86 Γ,¬(¬ψ ∨ ψ) Γ,¬¬ψ,¬ψ ∗ Caso 2: Se ϕ ∈ Γ. Então Γ ∪ {¬ϕ} é claramente T -inconsistente. Suponha o resultado válido para toda fórmula que admite uma prova em PC a partir de Γ em n passos, e seja ϕ1 · · ·ϕn+1 = ϕ uma prova em PC de ϕ a partir de Γ. Pela hipótese de indução, Γ `T ϕi para todo i ≤ n. Vamos mostrar que Γ `T ϕ. Devemos analisar um a um todos os casos que permitiram colocar ϕn+1 (isto é, ϕ) na seqüência. (a) Se ϕ é uma instância do axioma de PC, ou ϕ ∈ Γ. A prova é como acima. (b) Se ϕ foi obtido de ϕi (para algum 1 ≤ i ≤ n) pela regra de expansão (exp). Logo ϕ = ϕi ∨ ψ para alguma ψ. Por hipótese de indução Γ,¬ϕi é T -inconsistente; logo temos que Γ,¬ϕi,¬ψ é T -inconsistente. Dáı conclui- se que existe um tablô fechado para Γ,¬(ϕi ∨ ψ), bastando aplicar a regra (R¬∨) em primeiro lugar obtendo Γ,¬ϕi,¬ψ , e depois desenvolver um tablô fechado para esse conjunto. (c) Se ϕ foi obtido de ϕi (para algum 1 ≤ i ≤ n) pela regra de elim- inação (elim). Então ϕi = ϕ ∨ ϕ. Por hipótese de indução Γ,¬(ϕ ∨ ϕ) é T -inconsistente, e pela regra (R¬∨) Γ,¬ϕ é T -inconsistente. (d) Se ϕ é obtido pela regra (assoc), a prova é análoga. (e) Se ϕ é obtido de ϕi = ψ ∨ γ, ϕj = ¬ψ ∨ δ (para algum i, j ≤ n) pela regra de corte, tal que ϕ = γ ∨ δ. Por hipótese de indução Γ,¬(ψ ∨ γ) e Γ,¬(¬ψ ∨ δ) são T -inconsistentes, logo Γ,¬ψ,¬γ e Γ,¬¬ψ,¬δ são T - inconsistentes. Daqui obtemos que Γ,¬ψ,¬γ,¬δ e Γ,¬¬ψ,¬γ,¬δ são T - inconsistentes. Pelo Teorema 4.1.13, Γ,¬γ,¬δ é T -inconsistente, portanto Γ,¬(γ ∨ δ) é T -inconsistente. Para completar a prova da equivalência do método anaĺıtico com o método hilbertiano, precisamos de um resultado prévio. Definição 4.1.15. Uma configuração C = {Γ1, . . . ,Γn} é satisfat́ıvel se algum Γi foi satisfat́ıvel. Lema 4.1.16. Se ∆ é T -inconsistente então ∆ não é satisfat́ıvel (isto é, não existe uma valoração v tal que v(δ) = 1 para toda δ ∈ ∆). 89 Demonstração: Provaremos primeiro o seguinte Fato: Se C = {Γ1, . . . ,Γn} é uma configuração satisfat́ıvel, e C′ obtêm-se de C por aplicação de alguma regra de tablô, então C′ é satisfat́ıvel. Com efeito, C′ = C′′∪{∆1,∆2}, com C′′ = C−{Γi} (para algum 1 ≤ i ≤ n) e {∆1,∆2} é o resultado de aplicar uma regra anaĺıtica a Γi (possivelmente ∆1 = ∆2). Seja v uma valoração que satisfaz algum elemento Γj de C. Se Γj pertence a C′′ então v satisfaz C′. Caso contrário, v satisfaz Γi. Temos três casos para analisar, correspondentes às três regras anaĺıticas: Caso 1: Se Γi é Γ, ϕ ∨ ψ. Então ∆1 = Γ, ϕ e ∆2 = Γ, ψ. Neste caso, dado que v(ϕ ∨ ψ) = 1 então v(ϕ) = 1 (em cujo caso v satisfaz ∆1) ou v(ψ) = 1 (em cujo caso v satisfaz ∆2). Em ambos os casos temos que v satisfaz C′. Caso 2: Se Γi é Γ,¬(ϕ ∨ ψ). Então ∆1 = ∆2 = Γ,¬ϕ,¬ψ. Dado que v(¬(ϕ ∨ ψ)) = 1 então v(ϕ ∨ ψ) = 0, logo v(ϕ) = v(ψ) = 0 e então v(¬ϕ) = v(¬ψ) = 1. Dado que v(γ) = 1 para todo γ ∈ Γ (pois v satisfaz Γi) então obtemos que v satisfaz ∆1, logo v satisfaz C′. Caso 3: Se Γi é Γ,¬¬ϕ. Então ∆1 = ∆2 = Γ, ϕ. Como antes, vemos que v satisfaz ∆1, portanto v satisfaz C′. Isto prova o Fato. Suponhamos então que ∆ é T -inconsistente. Portanto existe um tablô fechado C1C2 · · ·Cn para ∆. Logo, C1 = {∆} e Ci+1 é obtido de Ci aplicando alguma regra de tablô (1 ≤ i ≤ n− 1). Se ∆ fosse satisfat́ıvel então C1 seria satisfat́ıvel, portanto, pelo Fato, cada configuração do tablô fechado para ∆ (inclúındo Cn) seria satisfat́ıvel, contradição. Isto mostra que ∆ é insa- tisfat́ıvel. Teorema 4.1.17. Para todo Γ ∪ {ϕ} ⊆ Prop, se Γ `T ϕ então Γ `PC ϕ. Demonstração: Se Γ `T ϕ então Γ ∪ {¬ϕ} é T -inconsistente. Logo, pelo lema anterior, Γ ∪ {¬ϕ} é insatisfat́ıvel. Pela Proposição 3.4.10 temos que Γ |= ϕ, portanto Γ `PC ϕ, pelo Teorema 3.4.6 de completude forte de PC. Obtemos finalmente a equivalência desejada entre tablôs e o sistema axiomático PC. Teorema 4.1.18. (Equivalência entre `PC e `T ) Seja Γ ∪ {ϕ} ⊆ Prop. Então Γ `PC ϕ see Γ `T ϕ. A partir deste resultado, observamos que todas as propriedades de `PC são herdadas por `T . Finalizamos esta seção observando que o método de tablôs nos fornece uma ferramenta para obter modelos de conjuntos satisfat́ıveis. Com efeito, basta apenas observar os elementos abertos da configuração final de um 90 tablô terminado para um conjunto satisfat́ıvel Σ, obtendo facilmente todos os modelos de Σ. Começaremos pelo seguinte lema, cuja prova deixamos como exerćıcio para o leitor: Lema 4.1.19. Seja C′ uma configuração obtida da configuração C aplicando uma regra de análise. Logo, se C′ é satisfat́ıvel por uma valoração v então C é também satisfat́ıvel pela valoração v. Vamos descrever a seguir um método para obter todos os modelos de um conjunto de fórmulas finito satisfat́ıvel Σ a partir de um tablô terminado para Σ. Seja C1C2 · · ·Cn um tablô aberto terminado para Σ. Considere agora Cn = {Σ1, . . . ,Σk}. Como foi observado anteriormente, dado que o tablô está terminado, então Σi = {li1, . . . , liri}, sendo que cada l i j é um literal para cada j = 1, . . . , ri e i = 1, . . . , k. Mais ainda, algum Σi deve ser aberto, porque o tablô é aberto. Sem perda de generalidade, suponhamos que Σ1, . . . ,Σs, com s ≤ k, são os ramos abertos de Cn. Veremos que cada Σi representa uma valoração v̄i que satisfaz Σ (i = 1, . . . , s). Mais ainda, toda valoração que satisfaz Σ é da forma v̄i para algum 1 ≤ i ≤ s. Fixemos 1 ≤ i ≤ s, e seja Pi o conjunto de variáveis proposicionais que ocorrem em Σi. Definimos uma função vi : Pi → 2 tal que vi(p) = 1 se p ∈ Σi, e vi(p) = 0 se ¬p ∈ Σi. Dado que Σi é aberto, a função está bem definida. Seja v̄i uma valoração obtida de vi definindo valores arbitrários para cada variável proposicional p que não pertence a Pi. Logo v̄i satisfaz Σi, portanto satisfaz Cn. Por indução em n e pelo Lema 4.1.19, provamos que v̄i satisfaz Σ. Logo, cada Σi nos fornece um modelo (aliás, vários modelos, um para cada extensão v̄i de vi) de Σ (i = 1, . . . , s). Veremos agora que todo modelo v de Σ é da forma v̄i para algum 1 ≤ i ≤ s. Para isso definimos, para cada 1 ≤ i ≤ s, a fórmula ψi = ¬ ri∨ j=1 ¬lij (lembre da notação estabelecida em 2.2.13). Observe que ψi representa toda valoração v̄i, no sentido seguinte: para cada valoração v, v(ψi) = 1 sse v coincide com vi em Pi sse v = v̄i (para alguma posśıvel extensão v̄i de vi). Considere ψ = s∨ i=1 ψi. Logo, para cada valoração v, v(ψ) = 1 sse existe 1 ≤ i ≤ s tal que v = v̄i (para alguma posśıvel extensão v̄i de vi). Provaremos agora que Σ |= ψ. Para isso, pelo Teorema 4.1.17 (e pela correção de PC) basta provar que existe um tablô fechado para Σ,¬ψ. Para isso, considere o tablô {C′i}ni=1, onde C′i é a configuração obtida de Ci acrescentando ¬ψ como elemento de cada elemento de Ci (i = 1, . . . , n). Isto é, C′i = {∆ ∪ {¬ψ} : ∆ ∈ Ci} 91 importante destes sistemas é que cada derivação pode ser levada a uma derivação em Forma Normal, na qual não existem passos redundantes. Este teorema é equivalente ao conhecido teorema Hauptsatz (o teorema de Eli- minação do Corte) estabelecido por Gentzen para o cálculo de sequentes. Os sistemas de dedução natural formam a base de uma importante área da lógica simbólica denominada Teoria da prova (Proof Theory). Nesta breve exposição apenas apresentaremos um sistema de dedução natural para a lógica proposicional clássica, explicaremos seu uso e ilustraremos o método com alguns exemplos. Recomendamos para o leitor interessado no tema a leitura do livro Natural Deduction de D. Prawitz ([11]), que transformou-se num clássico da área. Definição 4.2.1. Considere a assinatura C5 tal que C50 = {⊥}, C52 = {∨,∧,⇒} e C5n = ∅ nos outros casos. Denotaremos o conjunto L(C5) por Sent. O sistema DN de dedução natural para a lógica proposicional clássica consiste das seguintes regras (como sempre, ¬ϕ denota a fórmula ϕ⇒ ⊥): (∧I) ϕ ψ ϕ ∧ ψ (∧E1) ϕ ∧ ψ ϕ (∧E2) ϕ ∧ ψ ψ (∨I1) ϕ ϕ ∨ ψ (∨I2) ψ ϕ ∨ ψ (∨E) ϕ ∨ ψ [ϕ] γ [ψ] γ γ (⇒I) [ϕ] ψ ϕ⇒ ψ (⇒E) ϕ ϕ⇒ ψ ψ (⊥1) ⊥ ϕ (⊥2) [¬ϕ] ⊥ ϕ Temos as seguintes restrições nas regras de ⊥: na regras (⊥1) e (⊥2) a fórmula ϕ é diferente de ⊥ e, na regra (⊥2), a fórmula ϕ não é da forma ¬γ. 94 As restrições nas regras de ⊥ são inessenciais, e foram colocadas ape- nas para simplificar o estudo do sistema. Cada regra consiste de premis- sas (a parte de cima da barra) e de uma conclusão (a parte de baixo da barra). Partindo de um conjunto Γ de hipóteses, deduzimos conseqüências das fórmulas de Γ utilizando as regras, aplicando a seguir as regras nas conclusões, obtendo uma árvore invertida em que os nós terminais são as hipóteses utilizadas, e o nó raiz é a fórmula demonstrada. A notação [ϕ] ψ utilizada nas regras (∨E), (⇒I) e (⊥2) significa que estamos supondo a existência de uma derivação de ψ a partir de ϕ como uma de suas hipóteses. Nesse caso, após a aplicação da regra que utiliza [ϕ] ψ entre suas premissas, algumas ocorrências (todas, algumas, nenhuma) da premissa ϕ podem ser eliminadas como hipóteses. Assim, o resultado (a conclusão da regra) não vai mais depender da premissa ϕ, caso todas as ocorrências de ϕ como premissa tenham sido eliminadas. Isto reflete a ideia do Teorema da Dedução: se Γ, ϕ ` ψ (ψ depende de Γ, ϕ) então Γ ` ϕ⇒ ψ (ϕ ⇒ ψ depende de Γ). Vamos analisar dois exemplos para esclarecer o método: Exemplos 4.2.2. (1) Provaremos que (ϕ∨ψ)⇒ γ é deduzido em DN a partir do conjunto de hipóteses {ϕ⇒ γ, ψ ⇒ γ}. Primeiro de tudo, a seguinte derivação ϕ⇒ γ ϕ γ mostra que γ é deduzido em DN a partir de {ϕ ⇒ γ, ϕ}. Analogamente provamos que γ é deduzido em DN a partir de {ψ ⇒ γ, ψ}. Juntando estas duas derivações com a hipótese adicional ϕ∨ψ inferimos, aplicando a regra (∨E), a fórmula γ, podendo descarregar as hipóteses ϕ e ψ: ϕ⇒ γ [ϕ] γ ψ ⇒ γ [ψ] γ ϕ ∨ ψ γ Isto significa que γ é derivável em DN a partir de {ϕ ⇒ γ, ψ ⇒ γ, ϕ ∨ ψ}. Finalmente, aplicando a regra (⇒I) podemos descarregar a hipótese ϕ ∨ ψ, 95 obtendo uma derivação de (ϕ∨ψ)⇒ γ em DN a partir de {ϕ⇒ γ, ψ ⇒ γ}. ϕ⇒ γ [ϕ]1 γ ψ ⇒ γ [ψ]1 γ [ϕ ∨ ψ]2 γ (ϕ ∨ ψ)⇒ γ 2 1 Os números (1 e 2) foram colocados para individualizar a regra pela qual foram descarregadas as hipóteses. Assim, na aplicação da regra 1 foram descarregadas as hipóteses marcadas com 1, e na aplicação da regra 2 foi descarregada a hipótese marcada com 2. (2) Provaremos que γ ⇒ (ϕ ∧ ψ) é deduzido em DN a partir da hipótese (γ ⇒ ϕ) ∧ (γ ⇒ ψ). A seguinte derivação em DN prova esse fato: [γ]1 (γ ⇒ ϕ) ∧ (γ ⇒ ψ) γ ⇒ ϕ ϕ [γ]1 (γ ⇒ ϕ) ∧ (γ ⇒ ψ) γ ⇒ ψ ψ ϕ ∧ ψ γ ⇒ (ϕ ∧ ψ) 1 (3) Provaremos que em DN ϕ é derivável a partir de ¬¬ϕ, e vice-versa. Considere as seguintes derivações (lembrando que ¬¬ϕ é ¬ϕ⇒ ⊥): ¬¬ϕ [¬ϕ]1 ⊥ ϕ 1 ϕ [¬ϕ]1 ⊥ ¬¬ϕ 1 (4) Provaremos que em DN a fórmula ¬ϕ ∨ ϕ é um teorema. Considere a seguinte derivação (lembrando que ¬ϕ é ϕ⇒ ⊥): [ϕ]1 ¬ϕ ∨ ϕ [¬(¬ϕ ∨ ϕ)]2 ⊥ ¬ϕ ¬ϕ ∨ ϕ 1 [¬(¬ϕ ∨ ϕ)]2 ⊥ ¬ϕ ∨ ϕ 2 Na derivação acima, o número 1 indica uma aplicação da regra (⇒I), en- quanto que o número 2 indica uma aplicação da regra (⊥2). 4 O sistema DN é correto e completo para a semântica da lógica proposi- cional clássica. Isto é: 96