Lógica e aplicações: Matemática, Ciência da Computação e Filosofia

(Versão Preliminar - Capítulos 1 a 3)

W.A. Carnielli^{1}, M.E. Coniglio^{1} e R. Bianconi^{2}

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

\begin{matrix}c \\ ◯ \end{matrix} Todos os direitos reservados

(Comentários e sugestões são muito bem-vindos)

16 de março de 2004

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 de LPC . . . . . . . . . . . . . . . . . . . 24 2.1.4 Exercícios . . . . . . . . . . . . . . . . . . . . . . . . . 27

2.2 Semântica de LPC . . . . . . . . . . . . . . . . . . . . . . . . 28 2.2.1 Semântica dos conectivos . . . . . . . . . . . . . . . . 28 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 . . . . . . . . . . . . . . . . . 43 2.2.6 Exercícios . . . . . . . . . . . . . . . . . . . . . . . . . 48

3 Axiomática e Completude 49 3.1 Métodos de Dedução . . . . . . . . . . . . . . . . . . . . . . . 49 3.2 Sistemas Axiomáticos . . . . . . . . . . . . . . . . . . . . . . 50 3.3 Uma axiomática para LPC . . . . . . . . . . . . . . . . . . . . 55 3.4 Completude e Compacidade . . . . . . . . . . . . . . . . . . . 60 3.5 Outras Axiomáticas . . . . . . . . . . . . . . . . . . . . . . . 67 3.6 Axiomáticas não completas . . . . . . . . . . . . . . . . . . . 70 3.7 Exercícios . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74 3.8 Notas Bibliográficas . . . . . . . . . . . . . . . . . . . . . . . 77

Capítulo 1

Histórico e Paradoxos

1.1 Os Paradoxos Lógicos e o Infinito

O infinito tem sido historicamente a maior fonte de problemas nas ciências formais (matemática, lógica e mais modernamente nas ciências da computação), sendo os dilemas colocados pelo infinito conhecidos desde a antiguidade. Esta questão tem preocupado os filósofos e os matemáticos a tal ponto que o grande matemático alemão David Hilbert em seu conhecido discurso Über das Unendliche (“Sobre o Infinito”) proferido na cidade de Münster em 1925, chegou a afirmar que “... é portanto o problema do infinito, no sentido acima indicado, que temos que resolver de uma vez por todas”.

Hilbert sabia que a presença do infinito ameaça a consistência dos sistemas matemáticos (embora não seja a única causa possível de problemas de fundamentos), e dedicou sua vida a tentar provar que o uso do infinito poderia ser eliminado de uma vez por todas da matemática, dentro do chamado “Programa de Hilbert”. Como se sabe, Hilbert não teve sucesso, tendo sido suas pretensões derrotadas pelos Teoremas de Gödel, demonstrados por Kurt Gödel na década de 30.

O infinito é incompreensível à consciência humana, primeiro porque não existe como entidade física (não há no universo nenhum exemplo de alguma classe infinita, e de fato parece ser impossível existir, pelas leis da física e da moderna cosmologia). O infinito só existe na imaginação dos cientistas, que precisam dele basicamente para elaborar teorias com generalidade suficiente para que possam ser interessantes. Por exemplo, se queremos uma teoria simples que possa se referir à aritmética, não podemos supor que exista um último número natural N, pois as operações elementares com valores menores que N claramente ultrapassam N (o resultado do produto de números menores que N pode ser maior que N). Dessa forma, somos obrigados 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 contrapõ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 ℕ dos números naturais (o qual, em termos de ordem, 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 esa distinção: se assumimos que o infinito atual é possível, o paradoxo se resolve (como discutiremos 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 usado neste livro (ver Seção XXX) 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 alemão 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 propriedades e de problemas que ilustram de maneira simples o caráter paradoxal 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 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 ↦ 1

4 ↦ 2

6 ↦ 3

⋮

2n ↦ n

⋮

podemos fazer o conjunto dos pares ocupar todo o conjunto dos naturais. Como é possí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 caracterí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 \frac{a}{b} e \frac{c}{d} existe sempre outro, que é sua média aritmética:

\frac{a.d + b.c}{b.d}

e portanto entre dois racionais há infinitos outros.

Georg Cantor mostrou por um artifício muito simples que, embora realmente entre cada dois racionais hajam infinitos outros, basta contarmos os racionais de uma maneira diferente da usual (por “usual” entendemos a ordem dos números reais, vistos como pontos de uma reta) para que possamos nos convencer que há precisamente tantos racionais quanto números naturais. Para isso, estabeleceremos uma enumeração dos números racionais positivos (maiores que zero), e a partir daí, é possível (por um argumento análogo àquele da prova da similaridade entre os pares e os naturais) provar a enumerabilidade dos racionais:

\xymatrix{1/1 \ar[r] & 1/2 \ar[dl] & 1/3 \ar[r] & 1/4 \ar[dl] & 1/5 & … \\ 2/1 \ar[d] & 2/2 \ar[ur] & 2/3 \ar[dl] & 2/4 \ar[ur] & 2/5 & … \\ 3/1 \ar[ur] & 3/2 \ar[dl] & 3/3 \ar[ur] & 3/4 & 3/5 & … \\ 4/1 \ar[d] & 4/2 \ar[ur] & 4/3 & 4/4 & 4/5 & … \\ 5/1 \ar[ur] & 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 enumeráveis. Se assim o fosse, os reais no intervalo fechado [0, 1] tambem seriam. 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 …:

Ordem Real
1  0,  a_{11} a_{12} a_{13} a_{14} … a_{1n} …
2  0,  a_{21} a_{22} a_{23} a_{24} … a_{2n} …
3  0,  a_{31} a_{32} a_{33} a_{34} … a_{3n} …
4  0,  a_{41} a_{42} a_{43} a_{44} … a_{4n} …
⋮  ⋮
m  0,  a_{m1} a_{m2} a_{m3} a_{m4} … a_{mn} …
⋮  ⋮

onde cada a_{ij} representa um dígito entre 0 e 9.

Vamos construir um outro número real d em [0, 1] que não pertence a esta lista: para cada dígito a_{ij} considere o dígito ā_{ij} = a_{ij} + 1 (definindo, no caso em que a_{ij} = 9, o dígito ā_{ij} = 0). Definimos então d como:

d = 0, ā_{11} ā_{22} ā_{33} … ā_{nn} …

Observando que ā_{ij} ≠ a_{ij}, é claro que d não está na lista, pois difere de um dígito de cada um dos outros da lista. Com efeito, d difere do primeiro número da lista (ao menos) no primeiro dígito, do segundo número da lista (ao menos) no segundo dígito e, em geral, do n-ésimo número da lista (ao menos) no n-ésimo dígito. Portanto d, um número real entre 0 e 1, difere de todos os números da lista acima, o que é um absurdo, pois havíamos suposto que lista era completa. Assim se prova que não podemos enumerar os reais, que constituem então um conjunto infinito maior (isto é, com mais elementos) que os naturais e racionais.

Chamamos o infinito dos reais de “infinito não enumerável”.

Cantor provou que estes são apenas os primeiros de uma quantidade infinita de infinitos, mostrando basicamente que o conjunto das partes de um conjunto infinito de uma dada ordem produz um conjunto infinito de ordem superior.

Mencionamos finalmente que o método usado na demonstração acima da não-enumerabilidade do intervalo real [0, 1] é chamado de método diagonal de Cantor (observe que o número d é construído modificando a diagonal da matriz infinita definida acima), e é utilizado frequentemente na área da Computabilidade, com as modificações necessárias em cada caso.

1.2.3 O Hotel de Hilbert

Outra brincadeira folclórica é o chamado “Hotel de Hilbert”: existe um certo hotel, com um número infinito e enumerável de quartos

Q_{1}, Q_{2}, Q_{3}, … Q_{n}, …

Por sorte do proprietário, os quartos estão todos lotados. No meio da noite chega mais um hóspede sem reserva. O gerente simplesmente pede a cada hóspede que se mude para o quarto da direita, liberando o quarto Q_{1} para o viajante inesperado.

Na outra noite chegam dois novos hóspedes, e o gerente pede agora a cada hóspede que se mude dois quartos à direita, liberando os quartos Q_{1} e Q_{2}, e assim por diante. Uma noite porém chega um ônibus de excursão (bastante grande) trazendo infinitos novos hóspedes sem reserva.

O gerente agora pede a cada hóspede que se mude para o quarto cujo número seja o dobro do seu (de Q_{n} para Q_{2n}), liberando espaço para todos.

Assim ele continua recebendo quantos hóspedes novos quizer, até que uma noite (hóspedes inesperados sempre chegam à noite) estaciona um ônibus da Cia. Real de Turismo, e ele se apavora. Por quê?

1.2.4 O Lema de König

O Lema de König é uma forma (válida somente para conjuntos enumeráveis) do chamado Axioma da Escolha, que propõe que todo conjunto pode ser bem-ordenado (isto é, ordenado de forma que quaisquer de seus subconjuntos tenha um primeiro elemento com relação a esta ordem).

O Lema de König afirma que^{1}

Toda árvore infinita, que seja finitamente gerada (isto é, tal que cada ramo tenha um número finito de descendentes) possui pelo menos um ramo infinito.

Damos a seguir duas aplicações interessantes do Lema de König :

1. O Problema da Descendência Se a vida na Terra não se acabar, existe uma pessoa que vai ter infinitos descendentes.

1Os conceitos formais de árvore, ramo, descendente, nós e nós sucessores serão definidos posteriormente neste livro.

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á possí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 confundida 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 epí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 do pensamento, está ligado, como veremos, a um dos teoremas mais profundos 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 abolíssemos a auto referência não eliminarí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 sentencas 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, solucionar ou controlar os já existentes. Este problema é, em muitos casos, insolú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 círculos viciosos. A análise dos paradoxos serve como motivação ao estudo 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 próprio lógico inglês Bertrand Russell) que propõe que certos enunciados paradoxais deixem de ser considerados como enunciados propriamente ditos; 2. a segunda (a partir de idéias devidas ao lógico polonês Alfred Tars-

ki) 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 linguísticos que não são regulares fazem parte da metalinguagem.

Costuma-se ainda fazer distinção, na literatura, entre paradoxos e antinomias : 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 linguagem natural (isto é, em português corrente); como exercí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 introduzida uma linguagem formal, muito mais simples que a linguagem natural, mas também muito mais exata, e que com base nesta linguagem sejam formuladas 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) Considere 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 autodescritivos os adjetivos “polissílabo”, “escrito”, e não-autodescritivos os adjetivos “monossílabo”, “verbal”, etc. O adjetivo “não-autodescriti-vo” é autodescritivo ou não-autodescritivo?

5. Qual é “o menor número inteiro que não se pode expressar com menos de quinze palavras” ? (conte quantas palavras expressam este número).

6. Qual é o menor número inteiro que não se menciona de nenhuma maneira nestas notas? Existe tal número?

7. Se não existe, estas notas mencionam todos os números inteiros?

8. Analise a seguinte prova da existência de Deus: escreva “Esta sentença é falsa ou Deus existe”. Se a sentença toda for falsa, as duas partes separadas por “ou” são falsas, portanto a parte “Esta sentença é falsa” é falsa, e a sentença toda é verdadeira, impossível.

Portanto a sentença toda é verdadeira, e uma de suas partes é verdadeira. É claro que a primeira parte não pode ser verdadeira (pois isto contraria nossa hipótese), logo a segunda parte deve ser verdadeira, isto é, Deus existe.

9. Um crocodilo raptou um bebê de sua mãe e prometeu devolvê-lo se a mãe respondesse corretamente “sim” ou “não” à questão : “Vou comer o bebê?”. O que a mãe respondeu e o que fez o crocodilo?

10. Um juiz determinou que uma testemunha respondesse “sim” ou “não” à questão “Sua próxima palavra será não?” Qual é a resposta da testemunha?

11. (Dilema do Enforcado) Os prisioneiros de um certo reino são sempre decapitados ou enforcados. Um prisioneiro conseguiu o privilégio de formular uma afirmação; se fosse falsa, ele seria enforcado, e se verdadeira, decapitado. Qual afirmação o prisioneiro poderia formular para não ser executado?

12. (Paradoxo de Protágoras) Um jovem advogado fez o seguinte trato com seu mestre, Protágoras: ele só pagaria pela sua instrução se conseguisse vencer o primeiro caso. Como ele nunca aceitava nenhum caso, Protágoras o acionou, e ele teve que se defender. Quem ganha a causa?

13. Construa um supermicrocomputador que seja:

a) facílimo de carregar; b) econômico e simples de construir; c) infalível e universal; d) cujo sistema operacional seja tão simples que qualquer criança o opere.

(Sugestão: uma moeda, escrita “sim” de uma lado e “não” do outro. Faça qualquer pergunta à máquina, e em seguida uma nova pergunta apropriada.)

14. (Paradoxo do Livro sem Fim) Sobre uma mesa há um livro. Sua primeira página é bem espessa. A espessura da segunda é metade da da primeira, e assim por diante. O livro cumpre duas condições: primeiro, que cada página é seguida por uma sucessora cuja espessura é metade da anterior; e segundo, que cada página é separada da primeira por um número finito de páginas. Este livro tem última página?

15. (Paradoxo do Enforcado) Um juiz sentenciou um réu à morte pela forca, impondo a seguinte condição: que o réu seria enforcado de surpresa (isto é, sem poder saber em que dia), entre segunda e sexta feira da próxima semana, ao meio dia. Aconteceu a execução?

16. (Paradoxo do Ovo Inesperado) Imagine que voce tem duas caixas à sua frente, numeradas de 1 a 2. Você vira as costas e um amigo esconde um ovo em uma delas. Ele pede que você as abra na ordem, e garante que você vai encontrar um ovo inesperado. É claro que o ovo não pode estar na caixa 2 (pois não seria inesperado), e portanto essa caixa está fora. Só pode estar na 1. Você vai abrindo as caixas e encontra o ovo na caixa 2. Ele estava certo, mas onde está seu erro de raciocínio?

17. (Paradoxo da Confirmação de Hempel) Suponha que um cientista queira provar que todo papagaio é verde. Essa afirmação equivale logicamente a “tudo que não é verde não é papagaio” e portanto todos os exemplos que confirmam a segunda sentença, confirmam a primeira. Um gato preto e branco não é verde, e não é papagaio, e portanto confirma que todo papagaio é verde. Onde está o erro?

18. Os seguintes paradoxos são devidos ao lógico Jean Buridanus (de seu livro Sophismata, do século XIV). Vamos admitir algumas hipóteses que parecem bastante razoáveis:

• se sabemos alguma coisa, então acreditamos nisso;

• se acreditamos que alguma coisa é verdadeira, então acreditamos nessa coisa;

• se alguma coisa é falsa, então não pode fazer parte de nosso conhecimento.

Analise agora as sentenças abaixo, conhecidas como Paradoxos do conhecimento:

(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”. É possí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, desafiando 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 exercí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 organizado 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 curiosas; muitas outras podem estar perdidas na floresta, esperando ser descobertas. Dessas, este livro não vai tratar, mas esperamos que você pelo menos compreenda onde estão os limites do jardim da lógica.

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 raciocí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 raciocí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 argumentos 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 sentenças interrogativas, temporais, modais, etc. De nosso ponto de vista, a lógica se interessa pelo raciocínio matemático tradicional, e para tal fim as sentenças declarativas são suficientes.

A rigor, podemos considerar também as sentenças performativas, usadas 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, a qual denotaremos por LPC.

Mais tarde aumentaremos nossa linguagem para levar em conta as propriedades 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 decomponíveis em sentenças mais simples) e, num segundo estágio, especificar como as sentenças mais complexas são construídas a partir dessas utilizando conectivos. Os conectivos são funções que conectam 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 = {C_{n}}_{n∈ℕ} tal que cada C_{n} é um conjunto, sendo que C_{n} ∩ C_{m} = ∅ se n ≠ m. Os elementos do conjunto C_{n} são chamados de conectivos n-ários. Em particular, os elementos de C_{0} são chamados de constantes.

A ideia da construção de linguagens formais proposicionais é a seguinte: partindo de um conjunto infinito fixado V = {p_{n} : n ∈ ℕ} de símbolos, chamados de variáveis proposicionais, ou de fórmulas (ou proposições, ou sentenças) atômicas, construir as fórmulas mais complexas utilizando os conectivos de uma assinatura C, junto com alguns símbolos auxiliares (parênteses e vírgulas^{1}). Essa linguagem dependerá da assinatura C (desde que o conjunto V e os símbolos auxiliares permanecerão fixados ao longo do estudo). Devemos destacar que, na maioria dos exemplos prácticos, uma assinatura C consiste de um número finito de conectivos. nesses casos, existirá um n ∈ ℕ tal que C_{m} = ∅ para todo m ≥ n.

Consideraremos três símbolos auxiliares: ‘(’ e ‘)’ (parênteses esquerdo e direito, respectivamente) e ‘,’ (vírgula). Seja Aux o conjunto formado pelos símbolos auxiliares. Assumimos que V ∩ Aux = ∅. Para evitar confusões, assumiremos também que as assinaturas C consideradas satisfazem: C_{n} ∩ V = ∅ = C_{n} ∩ Aux para todo n ∈ ℕ. Dada uma assinatura C, e assumindo os conjuntos V e Aux, podemos considerar as expressões formadas com estes símbolos. Formalmente:

Definição 2.1.2. Seja C uma assinatura.

1. Definimos o domínio |C| de C como sendo o conjunto

|C| = ⋃{C_{n} : n ∈ ℕ}.

2. Seja D_{C} = |C| ∪ V ∪ Aux. Uma expressão sobre C é uma seqüência finita de símbolos ξ = s_{1} ⋯ s_{n} tal que s_{i} ∈ D_{C} para i = 1, …, n. O conjunto de todas as expressões sobre C é denotado por E_{C}.

Na definição acima, ⋃ F denota a união do conjunto de conjuntos F, isto é,

⋃ F = {x : x ∈ X para algum X ∈ F}.

O objetivo da definição de linguagens formais é reconhecer (ou isolar), dentre as expressões possíveis sobre uma dada assinatura, certas expressões que “fazem sentido”: as fórmulas. O conjunto das fórmulas constitue a linguagem gerada pela assinatura. Neste ponto, é útil estabelecer um paralelo com as linguagens naturais, em particular com a lingua portuguesa. A partir de símbolos dados (as letras do alfabeto, com ou sem acentos e craces) podemos concatenar esses símbolo para construir expressões, tais como ‘osspêpqtà’ ou ‘cerâmica’. Das duas expressões, apenas estaremos interessados na segunda, porque forma uma palavra (com sentido). E usando as palavras, estaremos interessados nas frases ou sentenças declarativas, isto é, seqüências finitas de palavras das quais faz sentido afirmar que são verdadeiras ou falsas, tais como ‘Roma é a capital de Itália’ ou ‘dois mais dois é cinco’. Obviamente estas seqüências de palavras (frases) devem ser construídas seguindo certas regras gramaticais específicas (no caso, da lingua portuguesa). As regras gramaticais das linguagens formais proposicionais são dadas apenas pela combinação das proposições básicas (atômicas) utilizando os conectivos dados de maneira iterada. Definimos então o seguinte:

1O uso destes símbolos auxiliares é apenas para fins de facilitar a individualizção das componentes de uma fórmula, sendo, de fato, prescindíveis.

Definição 2.1.3. Seja C = {C_{n}}_{n∈ℕ} uma assinatura. A linguagem gerada por C é o conjunto L(C) definido como sendo o menor dos subconjuntos X de E_{C} que satisfazem as seguintes propriedades:

1. V ⊆ X;

2. se n ∈ ℕ, c ∈ C_{n} e φ_{1}, …, φ_{n} ∈ X então c(φ_{1}, …, φ_{n}) ∈ X (em particular, C_{0} ⊆ X).

Os elementos de L(C) são chamados de fórmulas ou sentenças ou proposições sobre C. Da Definição 2.1.3 deduzimos o seguinte:

(i) L(C) satisfaz as propriedades 1 e 2 da Definição 2.1.3;

(ii) Se X ⊆ E_{C} satisfaz 1 e 2 da Definição 2.1.3 então L(C) ⊆ X.

A seguir exemplificaremos as definições introduzidas até agora, definindo três assinaturas especiais que utilizaremos ao longo deste livro, para analisar a lógica proposicional clássica.

Exemplo 2.1.4. A assinatura C^{0} consiste dos seguintes conectivos:

• C_{1}^{0} = {¬} (negação);

• C_{2}^{0} = {∨} (disjunção);

• C_{n}^{0} = ∅ se n ≠ 1, n ≠ 2.

Temos que |C^{0}| = {¬, ∨}. As seqüências de símbolos )) ∨ ¬¬,)p_{1}p_{345}(∨ e ∨(p_{1}, p_{2}) são expressões de C^{0} (apenas a segunda “faz sentido”). Porém a expressão p_{1}p_{3}(⇒ ♠) não é uma expressão sobre C^{0}, porque contém os símbolos ⇒ e ♠ que não pertencem a D_{C^{0}}. Por outro lado, ∨(p_{1}, ¬(p_{2})) e ¬(¬(∨(p_{23}, p_{1}))) são fórmulas sobre C^{0}. O conjunto L(C^{0}) das fórmulas sobre C^{0} será chamado de Prop. Por simplicidade, escreveremos ¬φ e (φ ∨ ψ) no lugar de ¬(φ) e ∨(φ, ψ), respectivamente. Freqüentemente economizaremos parênteses, omitindo os mais externos. Assim, escrevemos φ ∨ ψ ao invés de (φ ∨ ψ) quando a leitura não for comprometida.

Exemplo 2.1.5. A assinatura C^{1} consiste dos seguintes conectivos:

• C_{1}^{1} = {¬} (negação);

• C_{2}^{1} = {⇒} (implicação);

• C_{n}^{1} = ∅ se n ≠ 1, n ≠ 2.

Temos que |C^{1}| = {¬, ⇒}. É fácil ver que as expressões ¬(⇒(p_{3}, p_{7})) e ⇒(p_{0}, ⇒(¬(p_{0}), p_{1})) são fórmulas sobre C^{1}. O conjunto L(C^{1}) das fórmulas sobre C^{1} será chamado de Prop_{1}. Como antes, escreveremos ¬φ e (φ ⇒ ψ) no lugar de ¬(φ) e ⇒(φ, ψ), respectivamente. Também omitiremos freqüentemente parênteses, quando não houver risco de confusão. Assim, as duas fórmulas acima podem ser escritas como ¬(p_{3} ⇒ p_{7}) e p_{0} ⇒ (¬p_{0} ⇒ p_{1}).

Exemplo 2.1.6. A assinatura C^{2} consiste dos seguintes conectivos:

• C_{1}^{2} = {¬} (negação);

• C_{2}^{2} = {∨, ∧, ⇒} (disjunção, conjunção e implicação);

• C_{n}^{2} = ∅ se n ≠ 1, n ≠ 2.

Temos que |C^{2}| = {¬, ∨, ∧, ⇒}. Assumindo as mesmas convenções dos dois exemplos anteriores, as expressões p_{0} ⇒ p_{0}, p_{4} ⇒ (p_{4} ∨ p_{5}) e ¬p_{6} ⇒ (p_{3} ∨(p_{3} ∧p5)) são fórmulas sobre C^{2}. O conjunto L(C^{2}) das fórmulas sobre C^{2} será chamado de Prop_{2}.

O leitor perspicaz poderia perguntar-se se é sempre possí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 ⊆ E_{C} : 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}.

Dado que o próprio E_{C} satisfaz as propriedades 1 e 2 da Definição 2.1.3, então o conjunto de todos os subconjuntos de E_{C} satisfazendo essas propriedades é 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 E_{C} 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

F_{C}(X) = {c(φ_{1}, …, φ_{n}) : n ∈ ℕ, c ∈ C_{n} e φ_{1}, …, φ_{n} ∈ X} ∪ X.

Defina agora, para cada n ∈ ℕ e para cada conjunto X, o seguinte conjunto: F_{C}^{0}(X) = X, e F_{C}^{n+1} = F_{C}(F_{C}^{n}(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) = ⋃{F_{C}^{n}(V) : 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 meta-variá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. Usaremos letras gregas minúsculas (com ou sem índices) como meta-variáveis de fórmulas. Reservamos p_{0}, p_{1}, p_{2}, … para denotar as variáveis proposicionais 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 aritmé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 símbolos (i.e., o comprimento da proposição), o número de parênteses, etc.

O teorema a seguir demonstra que de fato as propriedades das proposições podem ser provadas pelo processo indutivo. Este teorema é muito importante porque muitas propriedades da lógica (na verdade, poderiamos dizer que a maioria) são provadas através deste processo indutivo.

Introduzimos a seguinte notação (semi)formal: P (φ) denota que a sentença φ satisfaz a propriedade P (note que P (φ) é um enunciado da metalinguagem, que pode portanto ser verdadeiro ou falso). Por exemplo, P (φ) poderia ser o enunciado “a sentença φ tem tantos parênteses esquerdos quantos 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 ∈ ℕ, c ∈ C_{n} e φ_{1}, …, φ_{n} ∈ L(C), se φ_{i} ∈ X (para i = 1, …, n) então c(φ_{1}, …, φ_{n}) ∈ X.

Então concluimos que X = L(C).

Demonstração: Por definição temos que X ⊆ L(C). Desde 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 daí 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 ∈ ℕ, c ∈ C_{n} e φ_{1}, …, φ_{n} ∈ L(C), se P (φ_{i}) vale (para i = 1, …, n) então P (c(φ_{1}, …, φ_{n})) vale.

Então concluimos 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 características das linguagens L(C). Um resultado importante a ser provado é com relação à unicidade da escrita das fórmulas: se c(φ_{1}, …, φ_{n}) = d(ψ_{1}, …, ψ_{m}) então c = d (logo n = m) e φ_{i} = ψ_{i} para todo i = 1, …, n. Para isso precisamos provar alguns resultados prévios:

Proposição 2.1.10. Para toda fórmula φ ∈ L(C), o número de parênteses esquerdos ‘(’ é o mesmo que o número de parênteses direitos ‘)’.

Demonstração: Seja pe(φ) o número de parênteses esquerdos da fórmula φ, e seja pd(φ) o número de parênteses esquerdos da fórmula φ. Observe que os valores pe(φ) e pd(φ) de φ sempre podem ser calculados, pois trata-se apenas de contar certos símbolos numa seqüência finita de símbolos. Considere agora o conjunto

X = {φ ∈ L(C) : pe(φ) = pd(φ)}.

Claramente V ⊆ X, pois pe(p) = pd(p) = 0 para toda p ∈ V. Dados φ_{1}, …, φ_{n} ∈ X e c ∈ C_{n} então pe(φ_{i}) = pd(φ_{i}) para todo i = 1, …, n. Logo

pe(c(φ_{1}, …, φ_{n})) = 1 + ∑_{i=1}^{n} pe(φ_{i}) = 1 + ∑_{i=1}^{n} pd(φ_{i}) = pd(c(φ_{1}, …, φ_{n})),

portanto c(φ_{1}, …, φ_{n}) ∈ X. Pelo Teorema 2.1.8 obtemos que X = L(C).

Note que na prova acima não utilizamos a unicidade da escrita das

fórmulas: na equação pe(c(φ_{1}, …, φ_{n})) = 1 + ∑_{i=1}^{n} pe(φ_{i}) estamos apenas

utilizando uma maneira possível de calcular o valor pe(φ) para a fórmula φ = c(φ_{1}, …, φ_{n}), independentemente da maneira específica de construir φ.

Dada uma expressão ξ = s_{1} ⋯ s_{n} sobre C (veja Definição 2.1.2), definimos um segmento inicial de ξ como sendo uma expressão ξ′ = s_{1} ⋯ s_{m}, com m < n.

Assim, p_{3}(∨p_{2} e p_{3}( são segmentos iniciais de p_{3}(∨p_{2}((p_{4}. O caso interssante é quando consideramos segmentos iniciais de fórmulas: eles deixam de ser fórmulas, como mostra o seguinte resultado técnico.

Lema 2.1.11. Seja φ uma fórmula, e ξ um segmento inicial de φ. Então ξ ∉ L(C).

A demonstração deste lema é imediata a partir da Proposição 2.1.10, e é deixada como exercício para o leitor. Finalmente podemos provar a unicidade da escrita das fórmulas:

Proposição 2.1.12. Sejam c ∈ C_{n}, d ∈ C_{m}, e φ_{1}, …, φ_{n}, ψ_{1}, …, ψ_{m} ∈ L(C). Se c(φ_{1}, …, φ_{n}) = d(ψ_{1}, …, ψ_{m}) então c = d, n = m e φ_{i} = ψ_{i} para i = 1, …, n.

Demonstração: De c(φ_{1}, …, φ_{n}) = d(ψ_{1}, …, ψ_{m}) (igualdade como seqüências finitas de símbolos) inferimos imediatamente que c = d, portanto n = m (lembre que C_{n} ∩ C_{m} = ∅ se n ≠ m). Considere agora as seqüências finitas de símbolos φ_{1} e ψ_{1}. Se φ_{1} e ψ_{1} tem o mesmo comprimento então elas coincidem, pois c(φ_{1}, …, φ_{n}) = d(ψ_{1}, …, ψ_{m}). Caso contrário, uma das fórmulas deve ser um segmento inicial da outra. Mas isto é impossível, por causa do Lema 2.1.11. Daqui inferimos que as duas fórmulas têm o mesmo comprimento e então φ_{1} = ψ_{1}. O mesmo argumento pode ser usado para provar que φ_{i} = ψ_{i} para i = 2, …, n.

Corolário 2.1.13. Seja φ ∈ L(C). Então vale uma e só uma das seguintes afirmações:

1. φ ∈ V ∪ C_{0};

2. existe um único n ≥ 1, um único c ∈ C_{n} e únicas φ_{1}, …, φ_{n} ∈ L(C) tais que φ = c(φ_{1}, …, φ_{n}).

O Corolário 2.1.13 será utilizado daqui em diante sem menção explícita. Podemos também por um processo indutivo (conhecido como definição por recursão) definir propriedades quaisquer a respeito de proposições. Em particular, temos um método para definir funções com domínio L(C).

Notação 2.1.14. A partir de agora usaremos a seguinte notação usual: uma função f do conjunto X no conjunto Y será denotada por f : X → Y, e dado um conjunto X e um número natural n, então X^{n} denotará o conjunto de todas as n-uplas formadas por elementos de X. Por convenção, X^{0} é o conjunto unitário {∗}.

Teorema 2.1.15. Seja S um conjunto. Suponha que, para cada n ∈ ℕ e para c ∈ C_{n}, existe uma função H_{c} : S^{n} → S (em particular, existe um elemento H_{c} de S para cada constante c ∈ C_{0}). Seja H : V → S uma função. Então existe uma única função f : L(C) → S satisfazendo o seguinte:

1. f(p) = H(p) para toda p ∈ V;

2. f(c(φ_{1}, …, φ_{n})) = H_{c}(f(φ_{1}), …, f(φ_{n})) para todo n ∈ ℕ, c ∈ C_{n} e φ_{1}, …, φ_{n} ∈ L(C). Em particular, f(c) = H_{c} se c ∈ C_{0}.

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 ∈ C_{n} e φ_{1}, …, φ_{n} ∈ X. Dado que existe um único valor s_{i} = 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})) = H_{c}(s_{1}, …, s_{n}).

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 de LPC

Os resultados apresentados até agora são gerais, e valem para qualquer linguagem 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 C^{0}, C^{1} e C^{2}, descritas nos exemplos 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). Então definimos o seguinte:

Definição 2.1.16. A função grau é a função g : Prop→ ℕ definida como segue:

1. g(φ) = 0, se φ é atômica;

2. g(φ ∨ ψ) = Max{g(φ), g(ψ)} + 1;

3. g(¬φ) = g(φ) + 1.

A partir do Teorema 2.1.15 é imediato que a função g está bem definida, considerando S = ℕ, H(p) = 0 para todo p ∈ V, H_{¬}(x) = x + 1 para todo x ∈ ℕ, 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→ ℕ 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 = ℕ, H(p) = 1 para todo p ∈ V, H_{¬}(x) = x + 1 para todo x ∈ ℕ, 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 ∪ C_{0};

2. g(c(φ_{1}, …, φ_{n})) = Max{g(φ_{1}), …, g(φ_{n})} + 1. Para l definimos

1. l(φ) = 1, se φ ∈ V ∪ C_{0};

2. l(c(φ_{1}, …, φ_{n})) = 1 + ∑_{i=1}^{n} 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 sí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(ψ);

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})) = ⋃_{i=1}^{n} Var(φ_{i}).

Em particular, Var(c) = ∅ se c ∈ C_{0}.

A noção de subfórmula de uma fórmula também pode ser definida indutivamente:

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(φ) ∪ {¬φ}.

É possível provar, por indução na complexidade da fórmula φ, que SF(φ) está bem definida (deixamos como exercício para o leitor). Os elementos 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. p_{2}, p_{3}, p_{10}, ¬p_{2}, ¬p_{3}, (p_{10} ∨ ¬p_{3}) e (p_{10} ∨ ¬p_{3}) ∨ ¬p_{2} são todas as subfórmulas de (p_{10} ∨ ¬p_{3}) ∨ ¬p_{2}.

Apresentamos finalmente um resultado adicional que fundamenta as definições por recursão. A definição a seguir é uma maneira de explicitar indutivamente os passos na construção de uma proposição (ou sentença, ou fórmula):

Definição 2.1.23. Seja ξ uma expressão sobre a assinatura C^{0}. Uma seqüência finita de expressões ξ_{1} … ξ_{n} é chamada seqüência de formação de ξ se ξ_{n} = ξ e, para cada 1 ≤ i ≤ n:

1. ξ_{i} é uma variável proposicional, ou

2. existem j, k < i tais que ξ_{i} = ξ_{j} ∨ ξ_{k}, ou

3. existe j < i tal que ξ_{i} = ¬ξ_{j}.

Dizemos que ξ é uma fórmula bem-formada se possui uma seqüência de formação.

Teorema 2.1.24. Prop é o conjunto de todas as fórmulas bem-formadas.

Demonstração: Seja S o conjunto de todas as fórmulas bem-formadas. Dado que S ⊆ E_{C^{0}} satisfaz 1 e 2 da Definição 2.1.3 então Prop ⊆ S

Por outro lado, suponha que ξ tem seqüência de formação ξ_{1} … ξ_{n} = ξ. Vamos mostrar por indução em n que ξ ∈ Prop.

(i) n = 1. Nesse caso, ξ_{1} = ξ, e ξ_{1} é forçosamente uma fórmula atômica, logo ξ ∈ Prop. (ii) Suponha que para m < n, o resultado vale, isto é, toda expressão que admite uma seqüência de formação com comprimento m < n está em Prop, para um dado n ≥ 1.

Nesse caso, ξ_{n} = ξ_{i} ∨ ξ_{j} (ou ξ_{n} = ¬ξ_{i}), i, j < n. Então ξ_{i}, ξ_{j} ∈ Prop, e por construção de Prop, ξ_{n} ∈ Prop.

Claramente, a Definição 2.1.23 pode ser dada em qualquer linguagem L(C), e o Teorema 2.1.24 também vale em todo L(C).

Exemplos 2.1.25.

1. p_{1} p_{2} p_{3} ¬p_{3} (p_{1} ∨ p_{2}) (¬p_{3} ∨ (p_{1} ∨ p_{2})) é uma seqüência de formação de (¬p_{3} ∨ (p_{1} ∨ p_{2})).

2. p_{2} p_{3} p_{4} (p_{2} ∨ p_{3}) ¬p_{3} é uma seqüência de formação de ¬p_{3}.

3. p_{3} ¬p_{3} é outra seqüência de formação de ¬p_{3} (esta direta, a outra indireta).

2.1.4 Exercícios

1. Seja C^{2} a asinatura definida no Exemplo 2.1.6. Para cada conjunto finito X, denotamos o seu número de elementos por \overline{X}. Considere as funções l, nc e Var definidas como segue:

• l(φ) = complexidade da fórmula φ (como na Observação 2.1.18);

• nc(φ) = número de conectivos que ocorrem na fórmula φ; • Var(φ) = conjunto das variáveis proposicionais que ocorrem em

φ (como na Observação 2.1.20).

Provar que l(φ) = nc(φ) + \overline{Var(φ)}.

2. Considere novamente a assinatura C^{2}. Provar o seguinte:

(a) As expressões ‘∨(p_{4}, ¬(∧(p_{4}, p_{0})))’, ‘⇒ (¬(¬(¬(p_{5}))), ⇒ (p_{2}, p_{2}))’ e ‘¬(⇒ (∨(¬(p_{4}), p_{3}), ∧(p_{1}, p_{0})))’ são fórmulas bem-formadas.

(b) As expressões ‘p_{1}()() ⇒’, ‘⇒ (p_{1}, p_{1}, ¬(p_{2}))’ e ‘∨(p_{4}, ¬(∧(p_{4}, p_{0}))’ não são fórmulas bem-formadas.

3. Provar o Lema 2.1.11: Se φ ∈ L(C) e ξ é segmento inicial de φ então ξ ∉ L(C).

4. Provar o seguinte: Se φ ∈ L(C) e ξ é segmento inicial de φ de comprimento ≥ 2 então pe(ξ) > pd(ξ). (Aqui, estamos estendendo as funções pe e pd que contam os parênteses esquerdos e direitos, respetivamente, para o conjunto E_{C} das expressões sobre C.)

5. Completar a prova do Teorema 2.1.15.

6. Provar por indução na complexidade de φ ∈ L(C) que SF(φ) sempre pode ser calculado em qualquer assinatura C (generalizando a Definição 2.1.21).

7. Generalize a Definição 2.1.23 e prove o análogo do Teorema 2.1.24 para uma linguagem L(C) arbitrária.

2.2 Semântica de LPC

2.2.1 Semântica dos conectivos

Na definição da linguagem de LPC (isto é, na definição do conjunto Prop) tínhamos como conectivos lógicos apenas os operadores ∨ e ¬. Observe que estes conectivos não tem nenhum significado: são apenas símbolos, portanto eles não têm o sentido usual de “ou” e “não”. Para que isso aconteça, interpretaremos 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 ∨ : 2^{2} → 2 através das seguintes tabelas (adotaremos eventualmente 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):

\begin{matrix}p & q & p ∨ q \\ 1 & 1 & 1 \\ 1 & 0 & 1 \\ 0 & 1 & 1 \\ 0 & 0 & 0 \end{matrix}  \begin{matrix}p & ¬p \\ 1 & 0 \\ 0 & 1 \end{matrix}

A rigor, deveríamos usar outros símbolos (que não os próprios) para as funções de verdade que interpretarão ∨ e ¬, mas para simplificar utilizamos na tabela-verdade os mesmos operadores da linguagem.

A partir daí, podemos definir indutivamente o valor de verdade 1 ou 0 de uma proposição a partir do valor de suas componentes atômicas. Formalmente, 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(φ ∨ ψ) = ∨(v(φ), v(ψ));

2. v(¬φ) = ¬(v(φ)).

Observação 2.2.2. Note que sempre é possível definir valorações, por causa do Teorema 2.1.15. Com efeito, basta considerar uma função v_{0} : 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 v_{0}, isto é, tal que v(p) = v_{0}(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 é:

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 v_{0} : 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(ψ∨γ) = ∨(v(ψ), v(γ)) = ∨(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(φ ∨ ψ) = \{ \begin{matrix}1 se v(φ) = 1 ou v(ψ) = 1 \\ 0 caso contrário \end{matrix}

2. v(¬φ) = \{ \begin{matrix}1 se v(φ) = 0 \\ 0 se v(φ) = 1 \end{matrix}

As definições semânticas (isto é, através de tabelas-verdade) da negação e da conjunçã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 verdade ∨ 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 conectivos que analisaremos semanticamente a seguir são os que correspondem com a assinatura proposicional C^{2} (veja Exemplo 2.1.6).

A conjunção ∧ : 2^{2} → 2 e a implicação material ⇒: 2^{2} → 2 são definidas através das seguintes tabelas-verdade:

\begin{matrix}p & q & p ∧ q \\ 1 & 1 & 1 \\ 1 & 0 & 0 \\ 0 & 1 & 0 \\ 0 & 0 & 0 \end{matrix}  \begin{matrix}p & q & p ⇒ q \\ 1 & 1 & 1 \\ 1 & 0 & 0 \\ 0 & 1 & 1 \\ 0 & 0 & 1 \end{matrix}

Como antes, deveríamos usar símbolos diferentes daqueles de C^{2} para interpretá-los, mas acreditamos que este abuso de notação não causará maiores inconvenientes.

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 princípio, pode-se pensar que a noção de implicação esta relacionada com a noção de causaefeito: 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 explí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 considerada 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 o antecedente foi verdadeiro e o consequente foi falso. Isto tem como conseqüência que, partindo de premissas falsas, não é mais possível raciocinar utilizando lógica clássica, pois qualquer conclusão pode ser tirada a partir daí. Existem muitas outras lógicas (chamadas de não-clássicas) desenvolvidas principalmente a partir do século XX, em que são definidas noções de implicação diferentes da implicação material, por exemplo, as implicações relevantes e as implicações contrafatuais.

Existem outros dois conectivos binários clássicos dignos de mencionar: a disjunção exclusiva ⊻ : 2^{2} → 2 e o bicondicional ⇔: 2^{2} → 2. As tabelas destes conectivos são as seguintes:

\begin{matrix}p & q & p ⊻ q \\ 1 & 1 & 0 \\ 1 & 0 & 1 \\ 0 & 1 & 1 \\ 0 & 0 & 0 \end{matrix}  \begin{matrix}p & q & p ⇔ q \\ 1 & 1 & 1 \\ 1 & 0 & 0 \\ 0 & 1 & 0 \\ 0 & 0 & 1 \end{matrix}

A idéia por trás destes conectivos é a seguinte: ⊻ representa uma disjunção exclusiva, isto é, um tipo de disjunção “P ou Q” da linguagem natural que é verdadeira se exatamente uma das proposições P, Q é verdadeira. Por exemplo, o sentido esperado da frase “Iremos ao cinema ou ao teatro” é o de ser verdadeiro quando formos ao cinema ou ao teatro, mas não ambas coisas. Por outro lado, o bicondicional reflete que as sentenças envolvidas são equivalentes, no sentido que elas têm o mesmo valor de verdade: ou ambas são verdadeiras, ou ambas são falsas. Estes conectivos não foram incluídos na assinatura C^{2} por causa de que eles podem ser expresos em termos dos outros conectivos. Com efeito, a função ⊻(p, q) pode ser calculada pela função f(p, q) = ∧(∨(p, q), ¬(∧(p, q))), enquanto que ⇔(p, q) pode ser calculada como g(p, q) = ∧(⇒(p, q), ⇒(q, p)):

\begin{matrix}p & q & p ∨ q & p ∧ q & ¬(p ∧ q) & f(p, q) \\ 1 & 1 & 1 & 1 & 0 & 0 \\ 1 & 0 & 1 & 0 & 1 & 1 \\ 0 & 1 & 1 & 0 & 1 & 1 \\ 0 & 0 & 0 & 0 & 1 & 0 \end{matrix}  \begin{matrix}p & q & p ⇒ q & q ⇒ p & g(p, q) \\ 1 & 1 & 1 & 1 & 1 \\ 1 & 0 & 0 & 1 & 0 \\ 0 & 1 & 1 & 0 & 0 \\ 0 & 0 & 1 & 1 & 1 \end{matrix}

Note que f(p, q) expressa que alguma das sentenças p, q deve ser verdadeira, mas não podem ser ambas verdadeiras. A função g(p, q) expressa que se p é verdadeiro então q também o é, e vice-versa.

O fenómeno de poder expressar certas funções de verdade em termos de outras é frequente: assim, a implicação material e a conjunção podem ser expressas em termos da disjunção e da negação como segue: h(p, q) = ∨(¬(p), q) e k(p, q) = ¬(∨(¬(p), ¬(q))), respectivamente.

\begin{matrix}p & q & ¬p & ¬p ∨ q \\ 1 & 1 & 0 & 1 \\ 1 & 0 & 0 & 0 \\ 0 & 1 & 1 & 1 \\ 0 & 0 & 1 & 1 \end{matrix}  \begin{matrix}p & q & ¬p & ¬q & ¬p ∨ ¬q & ¬(¬p ∨ ¬q) \\ 1 & 1 & 0 & 0 & 0 & 1 \\ 1 & 0 & 0 & 1 & 1 & 0 \\ 0 & 1 & 1 & 0 & 1 & 0 \\ 0 & 0 & 1 & 1 & 1 & 0 \end{matrix}

O fato de poder expressar as funções ⇒ e ∧ (e, a posteriori, as funções ⊻ e ⇔) em termos das funções ∨ e ¬ justifica a escolha da assinatura C^{0} para representar a lógica proposicional clássica LPC. Voltaremos depois (na Subseção 2.2.4) sobre a questão da definibilidade de funções de verdade em termos de outras funções.

Finalmente, observemos que podemos estender (ou modificar) a Definição 2.2.1 de valoração para as asinaturas C^{2} e C^{1}:

Definição 2.2.6. (i) Uma função v : Prop_{1} → 2 é uma valoração se satisfaz o seguinte:

1. v(φ ⇒ ψ) = ⇒(v(φ), v(ψ));

2. v(¬φ) = ¬(v(φ)).

(ii) Uma função v : Prop_{2} → 2 é uma valoração se satisfaz o seguinte:

1. v(φ ∨ ψ) = ∨(v(φ), v(ψ));

2. v(φ ∧ ψ) = ∧(v(φ), v(ψ));

3. v(φ ⇒ ψ) = ⇒(v(φ), v(ψ));

4. v(¬φ) = ¬(v(φ)).

2.2.2 Tautologias, contradições e contingências

Se as proposições são avaliadas através de valorações, é natural analisar as proposições sob a perspectiva das valorações. O primeiro paso é identificar duas proposições que tomam o mesmo valor em toda valoração.

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 Capítulo XXX):

• φ ≡ φ para toda φ (reflexiva);

• φ ≡ ψ implica ψ ≡ φ, para toda φ, ψ (simétrica);

• φ ≡ ψ e ψ ≡ γ implica φ ≡ γ, para toda φ, ψ, γ (transitiva).

Exemplo 2.2.8. Temos que (φ ∨ ψ) ≡ (ψ ∨ φ) e ¬¬φ ≡ φ para toda φ, ψ.

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, independentemente 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 atribuídos às variáveis que ocorrem em φ. Portanto, basta analisar todas as possíveis atribuições de valores de verdade 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 C^{2} na assinatura C^{0}, vemos que as sentenças p_{0} ∨ ¬p_{0}, (p_{0} ∧ p_{1}) ⇒ p_{1} e p_{0} ⇒ (¬p_{0} ⇒ p_{1}) são tautologias:

\begin{matrix}p_{0} & ¬p_{0} & p_{0} ∨ ¬p_{0} \\ 1 & 0 & 1 \\ 0 & 1 & 1 \end{matrix}  \begin{matrix}p_{0} & p_{1} & p_{0} ∧ p_{1} & (p_{0} ∧ p_{1}) ⇒ p_{1} \\ 1 & 1 & 1 & 1 \\ 1 & 0 & 0 & 1 \\ 0 & 1 & 0 & 1 \\ 0 & 0 & 0 & 1 \end{matrix}

\begin{matrix}p_{0} & p_{1} & ¬p_{0} & ¬p_{0} ⇒ p_{1} & p_{0} ⇒ (¬p_{0} ⇒ p_{1}) \\ 1 & 1 & 0 & 1 & 1 \\ 1 & 0 & 0 & 1 & 1 \\ 0 & 1 & 1 & 1 & 1 \\ 0 & 0 & 1 & 0 & 1 \end{matrix}

Por outro lado, as sentenças (p_{0} ∨ p_{1}) ⇒ p_{1} e ((p_{0} ⇒ p_{1}) ∧ p_{1}) ⇒ p_{0} não são tautologias:

\begin{matrix}p_{0} & p_{1} & p_{0} ∨ p_{1} & (p_{0} ∨ p_{1}) ⇒ p_{1} \\ 1 & 1 & 1 & 1 \\ 1 & 0 & 1 & 0 \\ 0 & 1 & 1 & 1 \\ 0 & 0 & 0 & 1 \end{matrix}

\begin{matrix}p_{0} & p_{1} & p_{0} ⇒ p_{1} & (p_{0} ⇒ p_{1}) ∧ p_{1} & ((p_{0} ⇒ p_{1}) ∧ p_{1}) ⇒ p_{0} \\ 1 & 1 & 1 & 1 & 1 \\ 1 & 0 & 0 & 0 & 1 \\ 0 & 1 & 1 & 1 & 0 \\ 0 & 0 & 1 & 0 & 1 \end{matrix}

No primeiro caso, qualquer valoração v tal que v(p_{0}) = 1 e v(p_{1}) = 0 produz v((p_{0} ∨ p_{1}) ⇒ p_{1}) = 0, portanto existem valorações que tornam a fórmula φ = (p_{0} ∨ p_{1}) ⇒ p_{1} falsa, logo φ não é tautologia. Por outro lado, toda valoração v tal que v(p_{0}) = 0 e v(p_{1}) = 1 produz v(((p_{0} ⇒ p_{1})∧p_{1}) ⇒ p_{0}) = 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.

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) há também outros métodos de tipo analí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 2^{n} 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 2^{n+1} = 2.2^{n} 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 conseguíssemos provar que não existe uma maneira mais eficiente de testar todas as tautologias, ou se conseguirmos um tal método eficiente, terí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 falsedades lógicas: são proposições tais que, independentemente do valor de verdade atribuido às suas componentes, recebem o valor 0 (falso).

Será que tem alguma relação (ou alguma maneira de relacionar) as tautologias e as contradições? A resposta é afirmativa: a relação de dualidade é realizada através da negação ¬, como mostra o seguinte resultado:

Proposição 2.2.12. (i) φ é tautologia sse ¬φ é contradição. (ii) φ é contradição sse ¬φ é tautologia. (iii) Se φ é tautologia então existe uma contradição ψ tal que φ ≡ ¬ψ. (iv) Se φ é contradição então existe uma tautologia ψ tal que φ ≡ ¬ψ.

Demonstração: Somente provaremos o item (iii), deixando o resto como exercício para o leitor. (iii) Seja φ uma tautologia. Então ψ = ¬φ é uma contradição, pelo item (i).

Mas ¬ψ = ¬¬φ e ¬¬φ ≡ φ, pelo Exemplo 2.2.8. Daqui φ ≡ ¬ψ, sendo que ψ é uma contradição.

Vemos que existem dois tipos importantes de proposições: as sempre verdadeiras (tautologias) e as sempre falsas (contradições). Evidentemente, nem toda proposição é de um destes tipos: por exemplo, p_{1} ∨ p_{2} ou p_{4} são proposições que tomam ambos valores, verdadeiro e falso, em diferentes valorações: basta considerar uma valoração v tal que v(p_{1}) = v(p_{4}) = 1 para obter v(p_{1} ∨ p_{2}) = v(p_{4}) = 1. Por outro lado, uma valoração v′ tal que v′(p_{1}) = v′(p_{2}) = v′(p_{4}) = 0 produz v(p_{1} ∨ p_{2}) = v(p_{4}) = 0. Sentenças deste tipo (que não são nem tautologias nem contradições) são chamadas de contingências, dado que elas são contingentes: dependendo da situação (do valor dado para as suas componentes atômicas), elas recebem ora o valor verdadeiro, ora o valor falso. Evidentemente uma proposição φ pertence a uma e só uma das três classes: tautologias, contradições, contingências.

2.2.3 Formas normais

Consideraremos nesta subseção a linguagem proposicional definida a partir da assinatura C^{2}. Nas fórmulas de Prop_{2} podem occorrer, portanto, os conectivos ¬, ∨, ∧ e ⇒. Veremos nesta subseção que é possível ‘padronizar’ as fórmulas de Prop_{2}, obtendo a partir delas outras fórmulas escritas numa forma padrão (chamada de forma normal), que resultam ser semanticamente equivalentes às fórmulas originais.

Antes de passar às definições, introduzimos a seguinte notação:

Notação 2.2.13. Sejam φ_{1}, …, φ_{n} fórmulas. Por

⋁_{i=1}^{n} φ_{i} e por ⋀_{i=1}^{n} φ_{i}

entendemos qualquer fórmula obtida pela disjunção (conjunção, respectivamente) das fórmulas φ_{1}, …, φ_{n}. Isto é, não interessa a ordem e a organização dos parênteses na construção da disjunção (conjunção, respectivamente).

Por convenção ⋁_{i=1}^{1} φ_{i} = ⋀_{i=1}^{1} φ_{i} = φ_{1}.

Por exemplo, ⋁_{i=1}^{3} φ_{i} pode representar indistintamente φ_{1} ∨ (φ_{3} ∨ φ_{2}) ou

(φ_{2} ∨ φ_{1}) ∨ φ_{3}.

Definição 2.2.14. (i) Um literal é uma fórmula da forma p (com p ∈ V) ou ¬p (com p ∈ V). (ii) Uma cláusula é uma fórmula φ da forma

φ = ⋀_{i=1}^{n} ψ_{i}

onde cada ψ_{i} é um literal e n ≥ 1. (iii) Dizemos que uma fórmula φ está em forma normal disjuntiva (FND) se φ é da forma

φ = ⋁_{i=1}^{n} φ_{i}

onde cada φ_{i} é uma cláusula (i = 1, …, n) e n ≥ 1.

Por exemplo, φ_{1} = p_{1} ∧ ¬p_{1}, φ_{2} = (p_{1} ∧ ¬p_{2}) ∧ ¬p_{7} e φ_{3} = p_{6} são cláusulas. Portanto, φ_{1} ∨ φ_{2} ∨ φ_{3} é uma fórmula em forma normal.

Proposição 2.2.15. Toda fórmula de Prop_{2} admite uma forma normal disjuntiva. Isto é, existe uma fórmula ψ, nas mesmas variáveis que φ, tal que ψ está em FND, e φ ≡ ψ. Mais ainda, existe um algoritmo para calcular uma FND ψ para φ.

Demonstração: Suponhamos que q_{1}, … q_{n} são exatamente todas as variáveis proposicionais que ocorrem em φ. Formalmente, deve existir um número i_{j} ∈ ℕ tal que q_{j} = p_{i_{j}}, para cada j = 1, …, n. Construimos a tabela-verdade de φ utilizando apenas as variáveis q_{1}, … q_{n}. Se φ é uma contradição, definimos ψ = ⋁_{j=1}^{n}(q_{j} ∧ ¬q_{j}). Claramente ψ está em FND e é uma contradição, portanto φ ≡ ψ. Se φ não é uma contradição, dentre as 2^{n} linhas da tabela-verdade, escolha apenas as linhas em que φ recebe o valor 1 (deve existir ao menos uma, porque φ não é contradição). Chamemos de L_{1}, …, L_{k} as linhas em que φ vale 1 (note que 1 ≤ k ≤ 2^{n}). Para cada linha L_{i}, defina os seguintes literais:

φ_{j}^{i} = \{ \begin{matrix}q_{j} se q_{j} recebe o valor 1 na linha L_{i} \\ ¬q_{j} caso contrário \end{matrix}

Considere agora, para cada i = 1, …, k, a cláusula φ_{i} = ⋀_{j=1}^{n} φ_{j}^{i}. Final-

mente, definimos ψ = ⋁_{i=1}^{k} φ_{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 L_{i}, da tabela-verdade construida para φ. Por construção dos literais φ_{j}^{i}, temos que v(φ_{j}^{i}) = 1 para todo j = 1, …, n. Com efeito, se v(q_{j}) = 1 então φ_{j}^{i} = q_{j}, portanto v(φ_{j}^{i}) = 1. Por outro lado, se v(q_{j}) = 0 então φ_{j}^{i} = ¬q_{j}, portanto v(φ_{j}^{i}) = 1. Assim sendo, temos que v(φ_{i}) = 1, pois φ_{i} consiste da conjunção dos φ_{j}^{i} 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(φ_{j}^{i}) = 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 q_{1}, …, q_{n} coincide com o valor dado para elas na linha L_{i} da tabela-verdade de φ, pela construção dos literais φ_{j}^{i}. Portanto o valor de φ (na linha L_{i}) coincide com v(φ), pela Proposição 2.2.4. Logo, v(φ) = 1, pois L_{i} é uma das linhas em que φ recebe o valor 1. Daqui φ ≡ ψ, concluindo a demonstração.

Exemplo 2.2.16. Acharemos uma FND para φ = (p_{2} ∨ p_{3}) ⇒ (p_{1} ∧ p_{3}).

\begin{matrix}p_{1} & p_{2} & p_{3} & p_{2} ∨ p_{3} & p_{1} ∧ p_{3} & (p_{2} ∨ p_{3}) ⇒ (p_{1} ∧ p_{3}) \\ 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 \end{matrix} \begin{matrix}L_{1} \\ L_{2} \\ L_{3} \\ L_{4} \end{matrix}

Temos que as linhas relevantes são L_{1} (a primeira linha), L_{2} (a terceira), L_{3} (a quarta) e L_{4} (a oitava). Definimos, para cada uma delas, as seguintes cláusulas:

1. Para L_{1} : φ_{1} = p_{1} ∧ p_{2} ∧ p_{3};

2. Para L_{2} : φ_{2} = p_{1} ∧ ¬p_{2} ∧ p_{3};

3. Para L_{3} : φ_{3} = p_{1} ∧ ¬p_{2} ∧ ¬p_{3};

4. Para L_{4} : φ_{4} = ¬p_{1} ∧ ¬p_{2} ∧ ¬p_{3}.

Finalmente, definimos ψ = ⋁_{i=1}^{4} φ_{i} como sendo uma FND para φ.

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 chamase de forma normal conjuntiva.

Definição 2.2.17. (i) Uma cláusula dual é uma fórmula φ da forma

φ = ⋁_{i=1}^{n} ψ_{i}

onde cada ψ_{i} é um literal. (iii) Dizemos que uma fórmula φ está em forma normal conjuntiva (FNC) se φ é da forma

φ = ⋀_{i=1}^{n} φ_{i}

onde cada φ_{i} é uma cláusula dual (i = 1, …, n).

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 Prop_{2} admite uma forma normal conjuntiva. 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 exercício.

2.2.4 Conjuntos adequados de conectivos

Observe que a FND associada a φ utiliza apenas as funções ∨, ∧ e ¬. Isto significa que qualquer função de verdade f : 2^{n} → 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 nível da linguagem por conectivos, podemos dizer que esta é uma propriedade 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 adequado 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 ∨ através da equação p ∧ q = ¬(¬p ∨ ¬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(q_{1}, …, q_{n}), considere uma FND ψ = ⋁_{i=1}^{n} φ_{i} associada a f seguindo o algoritmo da demonstração da Proposição 2.2.15. Se substituímos iteradamente em cada cláusula φ_{i} = ⋀_{j=1}^{n} φ_{j}^{i} cada conjunção pela fórmula que utiliza apenas ∨ e ¬ que a representa (usando a equação p ∧ q = ¬(¬p ∨ ¬q)), obteremos uma fórmula γ_{i} equivalente a φ_{i}, mas que utiliza apenas ∨ e ¬. Portanto, a disjunção ⋁_{i=1}^{n} γ_{i} é uma fórmula que representa f, e que apenas utiliza os conectivos ¬ e ∨.

É fácil provar que a disjunção pode ser representada utilizando ∧ e ¬ através da equação p ∨ q = ¬(¬p ∧ ¬q). Assim, de maneira análoga à prova da Proposição 2.2.20, podemos provar o seguinte:

Proposição 2.2.21. {¬, ∧} é um conjunto adequado de conectivos.

Por outro lado, da equação p ∨ q = ¬p ⇒ q e da Proposição 2.2.20 obtemos imediatamente o seguinte:

Proposição 2.2.22. {¬, ⇒} é um conjunto adequado de conectivos.

Consideremos agora uma constante ⊥ tal que v(⊥) = 0 para toda valoração v. Isto é, ⊥ : 2^{0} → 2 é dada por ⊥(∗) = 0 (lembrando que 2^{0} = {∗}). Então ¬p = p ⇒ ⊥ (confira!), logo obtemos o seguinte:

Proposição 2.2.23. {⊥, ⇒} é um conjunto adequado de conectivos.

Por outro lado, provaremos o seguinte:

Proposição 2.2.24. {¬, ⇔} e {∨, ∧} não são conjuntos adequados de conectivos.

Demonstração: Seja φ(p, q) uma função de verdade de dois argumentos p e q construída utilizando apenas as funções ¬ e ⇔. Por indução na complexidade de φ (considerada como fórmula) pode ser provado que φ é tautologia, ou contradição, ou os quatro valores possíveis das quatro linhas da tabelaverdade de φ consistem exatamente de dois valores 0 e dois valores 1. Dessa maneira, vemos que não é possível definir a tabela da disjunção (os quatro valores da sua tabela consistem de três valores 1 e um valor 0) nem a da conjunção (os quatro valores da sua tabela consistem de três valores 0 e um valor 1). Portanto {¬, ⇔} não é adequado.

Seja agora ψ(p) uma função de um argumento p que utiliza apenas as funções ∨ e ∧ na sua composição. É fácil ver que ψ recebe o valor 1 se p = 1, portanto não é possível reproduzir com estas funções a negação ¬. Daqui, {∨, ∧} não é adequado.

É interessante observar que os conectivos {∨, ¬} podem ser definidos a partir de um único conectivo chamado conectivo de Sheffer ou NAND, definido como segue: (p NAND q) = 1 see p e q não são simultaneamente 1:

\begin{matrix}p & q & p NAND q \\ 1 & 1 & 0 \\ 1 & 0 & 1 \\ 0 & 1 & 1 \\ 0 & 0 & 1 \end{matrix}

Podemos definir p ∨ q e ¬p como:

• ¬p = (p NAND p);

• p ∨ q = ((p NAND p) NAND (q NAND q)).

Desta maneira, obtemos imediatamente o seguinte:

Proposição 2.2.25. O conjunto { NAND } é adequado.

Similarmente, definimos um conectivo NOR dado por: (p NOR q) = 0 see p e q não são simultaneamente 0:

\begin{matrix}p & q & p NOR q \\ 1 & 1 & 0 \\ 1 & 0 & 0 \\ 0 & 1 & 0 \\ 0 & 0 & 1 \end{matrix}

Agora podemos definir p ∧ q e ¬p como:

• ¬p = (p NOR p);

• p ∧ q = ((p NOR p) NOR (q NOR q)).

Portanto, inferimos imediatamente o seguinte: Proposição 2.2.26. O conjunto { NOR } é adequado.

É possível provar o seguinte (veja [Mendelson]): Proposição 2.2.27. NAND e NOR são os únicos conectivos adequados.

2.2.5 Conseqüência semântica

A partir das definições dadas até agora, podemos finalmente definir formalmente 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 Γ |̸= φ.

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 é impossível exibir uma sentença ψ tal que ψ ∈ ∅ e v(ψ) ≠ 1 (simplesmente porque não tem sentenças no conjunto vazio) então é impossí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 recíproca é trivialmente verdadeira.

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 Prop_{1} e Prop_{2} 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 explícita.

Exemplos 2.2.30.

1. φ, ψ ⊧ φ ∧ ψ;

2. φ, φ ⇒ ψ ⊧ ψ; 3. φ, ¬φ ⊧ ψ, para ψ qualquer;

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 Γ ≠ ∅, Γ ⊧ φ;

9. Γ, φ ⊧ ψ see Γ ⊧ φ ⇒ ψ (Teorema de Dedução, forma semântica);

10. Γ ∪ {φ_{1}, …, φ_{n}} ⊢ φ see Γ ⊧ φ_{1} ⇒ (φ_{2} ⇒ (φ_{n} ⇒ φ) …);

11. Γ ∪ {φ_{1}, …, φ_{n}} ⊢ φ see Γ ⊧ (φ_{1} ∧ … ∧ φ_{n}) ⇒ φ. Demonstração: Provaremos somente (8), deixando o resto da prova como exercício para o leitor: (→ ) Segue de (2). (← ) Se Γ ⊧ φ para todo Γ ≠ ∅ 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) = \{ \begin{matrix}q se q ∈ V e q ≠ p; \\ ψ se q ∈ V e q = p \end{matrix}

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) = \{ \begin{matrix}q se q ≠ p; \\ ψ se q = p \end{matrix}

Provaremos a seguir uma importante propriedade da relação de conseqüência semântica ⊧, a saber: o resultado de substituir componentes atômicos por partes semanticamente equivalentes produz fórmulas semanticamente equivalentes. Por exemplo, seja ψ_{1} = (p_{1} ∧ p_{2}) e ψ_{2} = (¬(p_{1} ⇒ ¬p_{2})). Como ψ_{1} ≡ ψ_{2}, então φ[ψ_{1}/p] ≡ φ[ψ_{2}/p] para qualquer fórmula φ.

Teorema 2.2.33. (Teorema da Substituição, versão 1) Sejam ψ_{1}, ψ_{2} ∈ Prop. Se ψ_{1} ≡ ψ_{2} então φ[ψ_{1}/p] ≡ φ[ψ_{2}/p] para toda φ ∈ Prop e para toda p ∈ V.

Demonstração: Por indução em l(φ).

i) Se φ é atômica: se φ ≠ p, então φ[ψ_{1}/p] = φ = φ[ψ_{2}/p] e o resultado vale trivialmente. Se φ = p então φ[ψ_{1}/p] = ψ_{1} e φ[ψ_{2}/p] = ψ_{2} e o resultado vale por hipótese. ii) Se φ = φ_{1} ∨ φ_{2}: pela hipótese de indução φ_{1}[ψ_{1}/p] ≡ φ_{1}[ψ_{2}/p], e φ_{2}[ψ_{1}/p] ≡ φ_{2}[ψ_{2}/p]. Dado que (φ_{1} ∨ φ_{2})[ψ_{i}/p] = φ_{1}[ψ_{i}/p] ∨ φ_{2}[ψ_{i}/p] (para i = 1, 2), temos que, para toda valoração v,

v((φ_{1} ∨ φ_{2})[ψ_{1}/p]) = v(φ_{1}[ψ_{1}/p] ∨ φ_{2}[ψ_{1}/p])
= ∨(v(φ_{1}[ψ_{1}/p]), v(φ_{2}[ψ_{1}/p]))
= ∨(v(φ_{1}[ψ_{2}/p]), v(φ_{2}[ψ_{2}/p]))
= v(φ_{1}[ψ_{2}/p] ∨ φ_{2}[ψ_{2}/p]) = v((φ_{1} ∨ φ_{2})[ψ_{2}/p])

portanto vale o resultado. iii) Para o caso φ = ¬φ_{1} o argumento é análogo.

As funções Subs_{p}^{ψ} são casos particulares de um tipo de (extensão de) funções definidas por recursão, denominadas de substituições.

Definição 2.2.34. Uma substituição numa assinatura C é uma função σ : V → L(C)

Proposição 2.2.35. Toda substituição σ admite uma única extensão σ̂ : L(C) → L(C) tal que:

1. σ̂(p) = σ(p) se p ∈ V;

2. σ̂(c(φ_{1}, …, φ_{n})) = c(σ̂(φ_{1}), …, σ̂(φ_{n})) se c ∈ C_{n} e φ_{1}, …, φ_{n} ∈ L(C).

Demonstração: Imediata, a partir do Teorema 2.1.15.

Frequentemente escreveremos σ no lugar de σ̂, por simplicidade. Observe que Subs_{p}^{ψ} nada mais é do que σ̂ para a substituição σ tal que σ(p) = ψ e σ(q) = q se q ≠ p. As substituições serão utilizadas, entre outras coisas, para definir regras de inferência esquemáticas, nos próximos capítulos.

Dadas q_{1}, …, q_{n} ∈ V tal que q_{i} ≠ q_{j} (se i ≠ j), então as funções Subs_{p}^{ψ} podem ser generalizadas para as funções Subs_{q_{1}...q_{n}}^{ψ_{1}...ψ_{n}}, tal que Subs_{q_{1}...q_{n}}^{ψ_{1}...ψ_{n}}(φ) (denotado por φ[ψ_{1}/q_{1}, ⋯, ψ_{n}/q_{n}]) é a fórmula obtida de substituir simultaneamente a variável q_{i} pela fórmula ψ_{i} em φ. Note que, em geral, φ[ψ_{1}/q_{1}, ⋯, ψ_{n}/q_{n}] ≠ φ[ψ_{1}/q_{1}][ψ_{2}/q_{2}] ⋯ [ψ_{n}/q_{n}] (por isso destacamos que a substituição é simultânea, em contraste com a substituição iterada). Por exemplo, (p_{1} ∨ p_{2})[p_{2}/p_{1}, ψ/p_{2}] = (p_{2} ∨ ψ) enquanto que

(p_{1} ∨ p_{2})[p_{2}/p_{1}][ψ/p_{2}] = (p_{2} ∨ p_{2})[ψ/p_{2}] = (ψ ∨ ψ).

Note que, se σ é a substituição tal que σ(q_{i}) = ψ_{i} (para i = 1, …, n) e σ(p) = p caso contrário, então Subs_{q_{1}...q_{n}}^{ψ_{1}...ψ_{n}} = σ̂. Deixamos para o leitor a prova do seguinte resultado:

Teorema 2.2.36. (Teorema da Substituição, versão 2) Sejam ψ_{1}, …, ψ_{n}, φ_{1}, …, φ_{n} ∈ Prop. Se ψ_{i} ≡ φ_{i} (i = 1, …, n) então φ[ψ_{1}/q_{1}, ⋯, ψ_{n}/q_{n}] ≡ φ[φ_{1}/q_{1}, ⋯, φ_{n}/q_{n}] para toda φ ∈ Prop e para todas q_{1}, …, q_{n} ∈ V tais que q_{i} ≠ q_{j} (se i ≠ j).

2.2.6 Exercícios

1. Completar a prova da Proposição 2.2.12.

2. Provar que φ ≡ ψ sse φ ⇔ ψ é tautologia.

3. Usando tabelas de verdade provar que as seguintes fórmulas sao tautologias:

(a) (φ ⇒ ψ) ⇒ (¬ψ ⇒ ¬φ)

(b) (φ ∧ (ψ ∨ γ)) ⇔ ((φ ∧ ψ) ∨ (φ ∧ γ))

4. A partir da existência da FND para toda fórmula, provar a Proposição 2.2.18 (da existência de FNC para toda fórmula).

5. Construa uma função de verdade arbitrária dependendo de três argumentos (p, q, r). Ache a FNF e a FNC dessa função de verdade.

6. Completar a prova do Teorema 2.2.31.

7. Conferir os Exemplos 2.2.30.

8. Provar que {¬φ ⇒ (ψ ∨ γ), ¬ψ, δ ∧ ζ, γ ⇒ ¬δ} ⊧ φ.

9. Provar a Proposição 2.2.35.

10. Provar o Teorema 2.2.36.

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 sí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 analíticos, tem suas raízes originariamente no estudo de Gerard Gentzen [Gentzen], discípulo de Hilbert, depois sistematizado nos trabalhos de Beth [Beth] e Hintikka [Hintikka]. Uma versão mais moderna é apresentada no livro de Smullyan [Smullyan], 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 analítico, além de extremamente elegante, é muito eficiente do ponto de vista da heurí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 analítico.

Com relação a sua capacidade de provar teoremas, ambos os métodos (o método axiomático tradicional e o método analítico) são equivalentes. Isto significa que qualquer teorema que puder ser demonstrado num deles poderá se-lo no outro. Vamos verificar que ambos têm suas vantagens e desvantagens: o método analí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 Capítulo 4 apresentaremos o método analítico em detalhes.

3.2 Sistemas Axiomáticos

Fixada uma linguagem L(C), a idéia do método axiomático é definir demonstraçõ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 premissas 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; essa relação é uma regra de inferência do sistema. Formalmente:

Definição 3.2.1. Seja C uma assinatura.

(i) Uma regra de inferência^{1} sobre C é um conjunto R não vazio tal que

R ⊆ {⟨{φ_{1}, …, φ_{n}}, φ⟩ : {φ_{1}, …, φ_{n}, φ} ⊆ L(C)}

para algum 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 todo par ⟨Γ, φ⟩, se ⟨Γ, φ⟩ ∈ R ou ⟨Γ, φ⟩ ∉ R.^{2} (iii) Uma regra R é esquemática se é da forma

1Estaremos apenas considerando regras de inferência finitárias, isto é, com finitas premissas. Existem lógicas com regras infinitárias, mas não serão tratadas neste texto.

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ática R pode ser (e de fato, será) substituí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. Frequentemente escreveremos uma regra esquemática na forma

\frac{φ_{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 Γ ⊬_{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 determinar se x ∈ X ou x ∉ X. Os conceitos de conjuntos, relações e funções decidíveis (ou recursivos) serão rigorosamente definidos e analisados no Capítulo XXX.

As convenções de notação da Subseção 2.2.5 para ⊧ serão adotadas também para ⊢_{s}. Assim, ψ_{1}, ψ_{2}, …, ψ_{n} ⊢_{s} φ (em particular, ψ ⊢_{s} φ) denotará {ψ_{1}, ψ_{2}, …, ψ_{n}} ⊢_{s} φ; e Γ, φ ⊢_{s} ψ e Γ, Δ ⊢_{s} φ denotarão Γ∪{φ} ⊢_{s} ψ e Γ ∪ Δ ⊢_{s} φ, respectivamente.

Observações 3.2.4.

(1) No caso de S ser esquemático, a cláusula 2 da Definição 3.2.3 pode ser escrita como segue:

2. existe uma regra ⟨{δ_{1}, …, δ_{n}}, δ⟩ ∈ S e uma substituição σ tal que σ̂(δ) = φ_{i}, e {σ̂(δ_{1}), …, σ̂(δ_{n})} ⊆ {φ_{1}, …, φ_{i−1}}.

(2) Suponha que S é recursivamente axiomatizável. Embora exista um algoritmo para determinar se uma dada fórmula é ou não uma regra de inferência (em particular, um axioma), e embora existam algoritmos para determinar se é possível aplicar ou não uma regra de inferência, não existe em geral um algoritmo para decidir se uma dada fórmula é ou não um teorema. Os sistemas onde existe um tal algoritmo chamam-se de decidíveis.

(3) A maioria dos sistemas axiomáticos conhecidos são esquemáticos, portanto os axiomas e as regras de inferência são dadas como esquemas. Por exemplo, a conhecida regra de inferência Modus Ponens (MP)

MP \frac{φ φ ⇒ ψ}{ψ}

nada mas é do que uma regra esquemática gerada por ⟨{p_{0}, p_{0} ⇒ p_{1}}, p_{1}⟩.

A partir das definições anteriores, podemos provar o seguinte (meta)teorema sobre sistemas axiomáticos:

Teorema 3.2.5. Se φ_{1}, …, φ_{n} ⊢_{s} φ e ⊢_{s} φ_{i} (i = 1, …, n) então ⊢_{s} φ.

Demonstração: Considere uma prova em S

φ_{1} ⋯ φ_{n}ψ_{1} ⋯ ψ_{m}(= φ)

de φ a partir de {φ_{1}, …, φ_{n}} (note que sempre podemos colocar todas as hipóteses juntas no início de uma prova). Substituindo cada hipótese^{3} φ_{i} por uma prova de φ_{i} em S, obteremos uma nova seqüência finita de fórmulas em L(C) que constitue uma prova de φ sem usar hipóteses, isto é, φ é um teorema de S.

3Poderia acontecer que alguma φ_{i} coincida com alguma ψ_{j}, mas não estaremos interssados em substituir essas ocorrências adicionais de φ_{i}.

Algumas propriedades da relação de consequência sintática são as seguintes, cuja prova deixamos como exercício para o leitor.

Teorema 3.2.6. Valem as seguintes afirmações:

(a) φ ⊢ φ (reflexividade)

(b) Se ⊢ φ então Γ ⊢ φ

(c) Se φ ∈ Γ então Γ ⊢ φ

(d) Se Γ ⊢ φ e Γ ⊆ Δ então Δ ⊢ φ

(e) Se Γ ⊢ φ_{i} (i = 1, …, n) e φ_{1}, …, φ_{n} ⊢ ψ então Γ ⊢ ψ (transitividade)

(f) Se Γ ⊢ φ e Δ, φ ⊢ ψ então Γ, Δ ⊢ ψ

(g) Γ ⊢ φ se e só se existe Δ ⊆ Γ (Δ finito) tal que Δ ⊢ φ (compacidade)

(h) Se Γ, φ ⊢ ψ e Γ ⊢ φ então Γ ⊢ ψ

Uma propriedade desejável dos sistemas axiomáticos é a estruturalidade.

Definição 3.2.7. Um sistema axiomático S é estrutural se satisfaz o seguinte, para todo Γ ∪ {φ} ⊆ L(C):

Γ ⊢_{s} φ implica que σ̂(Γ) ⊢_{s} σ̂(φ) para toda substituição σ.

Provaremos que os sistemas axiomáticos esquemáticos são estruturais. Previamente, estabeleceremos um útil lema técnico.

Lema 3.2.8. Sejam σ e σ′ duas substituições. Considere a substituição

σ̂ ∘ σ′. Então { \atop σ̂ ∘ σ′} = σ̂ ∘ σ̂′.

Demonstração: Por indução na complexidade da fórmula φ de L(C), provase que

{ \atop σ̂ ∘ σ′}(φ) = (σ̂ ∘ σ̂′)(φ).

Deixamos os detalhes da prova como exercício para o leitor.

Teorema 3.2.9. Se S é esquemático então S é estrutural.

Demonstração: Suponha que Γ ⊢_{s} φ, e seja σ uma substituição. Por indução no comprimento n de uma prova de φ em S a partir de Γ provaremos que σ̂(Γ) ⊢_{s} σ̂(φ). Se n = 1 então temos dois casos para analisar: Caso 1: φ ∈ Γ. Sendo assim, então σ̂(φ) ∈ σ̂(Γ) e vale o resultado.

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}}. 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} se σ̂′(δ_{i}) = φ_{j}, com 1 ≤ j ≤ 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, substituiremos as variáveis proposicionais que ocorrem na regra por metavariáveis que expressam fórmulas arbitrárias. Por exemplo, escreveremos

MP \frac{φ φ ⇒ ψ}{ψ}  no lugar de  MP \frac{p_{0} p_{0} ⇒ p_{1}}{p_{1}} .

A partir de agora, os sistemas axiomáticos que definiremos serão esquemá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 de prova não impede escrever provas com n passos irrelevantes.

3.3 Uma axiomática para LPC

Nesta seção definiremos um sistema axiomático para 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 C^{0} definidas no capítulo anterior.

Definição 3.3.1. O sistema axiomático PC para LPC consiste dos seguintes axiomas e regras de inferência:

(axioma)  ¬φ ∨ φ

(expansão)  \frac{φ}{φ ∨ ψ}

(eliminação)  \frac{φ ∨ φ}{φ}

(associatividade) \frac{φ ∨ (ψ ∨ γ)}{(φ ∨ ψ) ∨ γ}

(corte)  \frac{φ ∨ ψ ¬φ ∨ γ}{ψ ∨ γ}

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)

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} ψ ∨ (γ ∨ φ).

Demonstração:

1. φ ∨ (ψ ∨ γ) (hip.)

2. (ψ ∨ γ) ∨ φ (3.3.3)

3. ψ ∨ (γ ∨ φ) (3.3.5)

Teorema 3.3.8. φ ∨ (ψ ∨ γ) ⊢_{pc} γ ∨ (φ ∨ ψ).

Demonstração:

1. φ ∨ (ψ ∨ γ) (hip.)

2. ψ ∨ (γ ∨ φ) (3.3.6)

3. γ ∨ (φ ∨ ψ) (3.3.6)

Teorema 3.3.9. ⊢_{pc} ¬(φ ∨ ψ) ∨ (ψ ∨ φ).

Demonstração:

1. ¬φ ∨ φ (axioma)

2. φ ∨ ¬φ (3.3.3)

3. (φ ∨ ¬φ) ∨ ψ (exp)

4. ψ ∨ (φ ∨ ¬φ) (3.3.3)

5. ¬φ ∨ (ψ ∨ φ) (3.3.7)

6. ¬ψ ∨ (ψ ∨ φ) ((axioma), (exp), 3.3.5)

7. ¬(φ ∨ ψ) ∨ (ψ ∨ φ) (de 5. e 6., 3.3.6)

Teorema 3.3.10. φ ∨ (ψ ∨ γ) ⊢_{pc} φ ∨ (γ ∨ ψ).

Demonstração:

1. φ ∨ (ψ ∨ γ) (hip.)

2. (ψ ∨ γ) ∨ φ (3.3.3)

3. ¬(ψ ∨ γ) ∨ (γ ∨ ψ) (3.3.9)

4. φ ∨ (γ ∨ ψ) (de 2. e 3., (corte))

Teorema 3.3.11. Seja π : {φ, ψ, γ} → {φ, ψ, γ} uma permutação. Então: (a) φ ∨ (ψ ∨ γ) ⊢_{pc} π(φ) ∨ (π(ψ) ∨ π(γ))

(b) φ ∨ (ψ ∨ γ) ⊢_{pc} (π(φ) ∨ π(ψ)) ∨ π(γ) .

(c) (φ ∨ ψ) ∨ (φ ∨ γ) ⊢_{pc} φ ∨ (ψ ∨ γ).

Demonstração: Partes (a) e (b) seguem por aplicação direta de 3.3.6, 3.3.7, 3.3.8 e da regra (assoc). Para a parte (c) :

1. (φ ∨ ψ) ∨ (φ ∨ γ) (hip.)

2. φ ∨ (ψ ∨ (φ ∨ γ)) (3.3.5 em 1.)

3. φ ∨ ((φ ∨ γ) ∨ ψ) (3.3.10 em 2.)

4. ¬φ ∨ (φ ∨ γ) ((axioma), (exp) e 3.3.5)

5. ¬φ ∨ ((φ ∨ γ) ∨ ψ) ((exp) e 3.3.5 em 4.)

6. (φ ∨ γ) ∨ ψ ((corte) em 3. e 5., seguido de (elim))

7. φ ∨ (ψ ∨ γ) (3.3.5 e 3.3.10)

Teorema 3.3.12. (Lei da dupla negação)

(a) φ ⊢_{pc} ¬¬φ.

(b) ¬¬φ ⊢_{pc} φ.

Demonstração: (a) Considere a seguinte prova:

1. φ (hip.)

2. ¬¬φ ∨ ¬φ (axioma)

3. ¬φ ∨ ¬¬φ (3.3.3 em 2.)

4. ¬¬φ (3.3.2 em 1., 3.)

(b) Considere a seguinte prova:

1. ¬¬φ (hip.)

2. ¬¬φ ∨ φ (exp)

3. ¬φ ∨ φ (axioma)

4. φ ∨ φ ((corte) em 3., 2.)

5. φ (elim)

Teorema 3.3.13. φ, ¬φ ⊢_{pc} ψ. (Princípio de Pseudo-Scotus)

Demonstração:

1. φ (hip.)

2. ¬φ (hip.)

3. ¬φ ∨ ψ (exp)

4. ψ (3.3.2 em 1., 3.)

Provaremos a seguir o Teorema da Dedução, na forma sintática, que permite transformar a prova de uma dedução na prova de uma implicação. (Lembramos que a implicação φ ⇒ ψ é uma abreviação da fórmula ¬φ ∨ ψ.) É um resultado bastante útil, pois permite trabalhar com um número maior de premissas para provar fórmulas mais simples (de menor complexidade). Observe que um resultado análogo, na forma semântica, foi demonstrado no Teorema 2.2.31(9).

Teorema 3.3.14. (Teorema da Dedução, forma sintática) Γ, φ ⊢_{pc} ψ se, e só se, Γ ⊢_{pc} φ ⇒ ψ.

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} γ.

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 proposicional 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 Completude. 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 recíprocas das respectivas noções de completude: S é fracamente (fortemente, respectivamente) correto se ⊢_{s} φ (Γ ⊢_{s} φ, respectivamente) 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 recíproca não é necessariamente 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 Compacidade, 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 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 ¬p_{0} ∨ p_{0}, portanto ⊧ φ. Suponha o resultado válido para toda φ que admite uma prova de comprimento 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 exercí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 Teorema 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. Γ ⊬_{pc} φ;

2. Se ψ ∉ Γ 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 γ ∈ Γ; (c) ¬ψ ∈ Γ sse ψ ∉ Γ.

(d) A função característica χ_{Γ} de Γ (isto é, a função χ_{Γ} : Prop → 2 tal que χ_{Γ}(ψ) = 1 sse ψ ∈ Γ) é uma valoração clássica (ver Definição 2.2.1).

Demonstração: (a) Se ψ ∈ Γ então evidentemente Γ ⊢_{pc} ψ, pela noção de prova em sistemas axiomáticos (veja Teorema 3.2.6(c)). Reciprocamente, suponha que ψ ∉ Γ. Como Γ é φ-saturado, temos que Γ, ψ ⊢_{pc} φ. Se Γ ⊢_{pc} ψ então Γ ⊢_{pc} φ, pelo Teorema 3.2.6(f), contradição. Portanto Γ ⊬_{pc} ψ.

(b) Suponhamos que (ψ ∨ γ) ∈ Γ. Se ψ ∉ Γ e γ ∉ Γ então Γ, ψ ⊢_{pc} φ e Γ, γ ⊢_{pc} φ, pois Γ é φ-saturado. Daqui obtemos que Γ, ψ ∨ γ ⊢_{pc} φ, pelo Teorema 3.3.16(a), e então Γ ⊢_{pc} φ, contradição. Portanto: se (ψ ∨ γ) ∈ Γ então ψ ∈ Γ ou γ ∈ Γ. Reciprocamente, suponha que ψ ∈ Γ. De ψ ⊢_{pc} ψ ∨ γ obtemos que Γ ⊢_{pc} ψ∨γ, portanto (ψ∨γ) ∈ Γ, pelo item (a). Analogamente, de γ ∈ Γ inferirmos que (ψ ∨ γ) ∈ Γ.

(c) Suponhamos que ¬ψ ∈ Γ. Se ψ ∈ Γ então, dado que ψ, ¬ψ ⊢_{pc} φ (pelo Teorema 3.3.13), obtemos que Γ ⊢_{pc} φ, uma contradição. Portanto: se ¬ψ ∈ Γ então ψ ∉ Γ. Reciprocamente, suponha que ψ ∉ Γ. Então Γ, ψ ⊢_{pc} φ. Se ¬ψ ∉ Γ então Γ, ¬ψ ⊢_{pc} φ, portanto Γ ⊢_{pc} φ pelo Teorema 3.3.16(b), contradição. Logo: se ψ ∉ Γ então ¬ψ ∈ Γ.

(d) Seja χ_{Γ} : Prop → 2 a função característica de Γ. Então, para toda ψ, γ ∈ Prop temos o seguinte: χ_{Γ}(ψ ∨ γ) = 1 sse (pela definição de χ_{Γ}) (ψ ∨ γ) ∈ Γ sse (pelo item (b)) ψ ∈ Γ ou γ ∈ Γ sse χ_{Γ}(ψ) = 1 ou χ_{Γ}(γ) = 1 sse ∨(χ_{Γ}(ψ), χ_{Γ}(γ)) = 1. Por outro lado, χ_{Γ}(¬ψ) = 1 sse ¬ψ ∈ Γ sse (pelo item (c)) ψ ∉ Γ sse χ_{Γ}(ψ) = 0 sse ¬(χ_{Γ}(ψ)) = 1. Isto mostra que χ_{Γ} é uma valoração clássica sobre Prop (veja a Definição 2.2.1), concluindo a demonstração.

Lema 3.4.5. (Lindembaum-Asser) Seja Γ∪{φ} um conjunto de fórmulas tais que Γ ⊬_{pc} φ. Então existe um conjunto Δ tal que Γ ⊆ Δ e Δ é φsaturado.

Demonstração: Considere uma enumeração {φ_{n} : n ∈ ℕ} do conjunto Prop (note que Prop é enumerável, pois os conjuntos V e |C^{0}| são enumeráveis). Definiremos uma seqüência {Γ_{n}}_{n∈ℕ} de conjuntos de fórmulas da maneira seguinte: Γ_{0} = Γ e, para todo n ≥ 0,

Γ_{n+1} = \{ \begin{matrix}Γ_{n} ∪ \{φ_{n}\} & se Γ_{n}, φ_{n} ⊬_{pc} φ; \\ Γ_{n} ∪ \{¬φ_{n}\} & se Γ_{n}, φ_{n} ⊢_{pc} φ. \end{matrix}

É fácil provar o seguinte Fato:

(a) Γ_{n} ⊆ Γ_{n+1} para todo n ∈ ℕ;

(b) Γ_{n} ⊬_{pc} φ para todo n ∈ ℕ. Com efeito, (a) é imediato da definição dos conjuntos Γ_{n}. Provaremos (b) por indução em n. Se n = 0 então o resultado vale pela hipótese sobre Γ. Suponha que Γ_{n} ⊬_{pc} φ, para um dado n ≥ 0. Se Γ_{n+1} = Γ_{n} ∪ {φ_{n}} então claramente Γ_{n+1} ⊬_{pc} φ, pela definição de Γ_{n+1}. Por outro lado, se Γ_{n+1} = Γ_{n} ∪ {¬φ_{n}} então Γ_{n}, φ_{n} ⊢_{pc} φ, pela definição de Γ_{n+1}. Suponha que Γ_{n+1} ⊢_{pc} φ. Então, pelo Teorema 3.3.16(b), obtemos que Γ_{n} ⊢_{pc} φ, contradição. Logo Γ_{n+1} ⊬_{pc} φ. Isto prova o Fato. Considere agora o conjunto Δ = ⋃_{n∈ℕ} Γ_{n}. Claramente Γ ⊆ Δ. Provaremos a seguir que Δ é φ-saturado. Suponha que Δ ⊢_{pc} φ. Pelo Teorema 3.2.6(g) temos que Δ_{0} ⊢_{pc} φ para algum subconjunto finito Δ_{0} de Δ. Pela definição de Δ e pelo Fato(a) inferimos que Γ_{n} ⊢_{pc} φ para algum n suficientemente grande. Mas isto contradiz o Fato(b). Portanto Δ ⊬_{pc} φ. Seja agora ψ uma fórmula em Prop tal que ψ ∉ Δ. Existe um número m tal que ψ = φ_{m}, pois partimos de uma enumeração de Prop. Dado que φ_{m} ∉ Δ então φ_{m} ∉ Γ_{m+1}, portanto Γ_{m+1} = Γ_{m} ∪{¬φ_{m}} e Γ_{m}, φ_{m} ⊢_{pc} φ, pela construção da seqüência de conjuntos Γ_{n}. Mas então obtemos que Δ, φ_{m} ⊢_{pc} φ, isto é, Δ, ψ ⊢_{pc} φ. Isto prova que Δ é φ-saturado, concluindo a demonstração.

Teorema 3.4.6. (Completude Forte de PC) Seja Γ ∪ {φ} um conjunto de fórmulas em Prop. Então Γ ⊧ φ implica Γ ⊢_{pc} φ.

Demonstração: Suponhamos que Γ ⊬_{pc} φ. Então existe um conjunto φsaturado Δ tal que Γ ⊆ Δ, pelo Lema 3.4.5. Seja χ_{Δ} : Prop → 2 a função característica do conjunto Δ; logo, χ_{Δ} é uma valoração, pelo Lema 3.4.4(d). Mais ainda, χ_{Δ}(ψ) = 1 para toda ψ ∈ Γ (pois Γ ⊆ Δ), e χ_{Δ}(φ) = 0, pois φ ∉ Δ (pelo Teorema 3.2.6(c)). Logo, Γ |̸= φ, pela definição de conseqüência semântica 2.2.28. Ou seja: se Γ ⊧ φ então Γ ⊢_{pc} φ, como queríamos demonstrar.

Corolário 3.4.7. (Adequação Forte de PC) O sistema PC é fortemente adequado, isto é, PC é fortemente correto e fortemente completo com relação à semântica de valorações: para todo conjunto de fórmulas Γ ∪ {φ} em Prop temos que Γ ⊧ φ sse Γ ⊢_{pc} φ.

Como corolário do Teorema da Adequação Forte, obtemos o Teorema da Compacidade, que afirma que a relação de conseqüência semântica é finitária, no sentido em que uma sentença é semanticamente dedutível de no 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 (observe que uma versão sintática deste resultado aparece no Teorema 3.2.6(g)).

Corolário 3.4.8. (Teorema da Compacidade de 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.

É possível dar uma outra formulação equivalente do teorema da compacidade, 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 Γ |̸= φ. Ou seja: se Γ ⊧ φ então Γ ∪ {¬φ} é insatisfatível. Reciprocamente, suponha que Γ |̸= φ. 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:

(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, Γ ⊧ ¬(p_{0} ∨ ¬p_{0}) (isto sai claramente da definição de consequência semântica). Usando (a) temos que Γ_{0} ⊧ ¬(p_{0} ∨ ¬p_{0}) para algum subconjunto finito Γ_{0} de Γ, portanto Γ_{0} ∪ {¬¬(p_{0} ∨ ¬p_{0})} é insatisfatível, pela Proposição 3.4.10. Mas, dado que ¬¬(p_{0} ∨ ¬p_{0}) é 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 subconjunto finito Γ_{0} de Γ temos que Γ_{0} ∪ {¬φ} é satisfatível, e seja Δ = Γ ∪ {¬φ}. Seja Δ_{0} ⊆ Δ finito, e considere Γ_{0} = Δ_{0} − {¬φ} (note que possivelmente ¬φ ∉ Δ_{0}). Então Γ_{0} é um subconjunto finito de Γ, portanto Γ_{0} ∪ {¬φ} é satisfatível, por hipótese. Dado que Δ_{0} ⊆ Γ_{0} ∪ {¬φ} (a igualdade 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 q_{1}, …, q_{n} as variáveis proposicionais que ocorrem em φ. Seja v uma valoração qualquer. Para 1 ≤ i ≤ n definimos

q_{i}^{⋆} = \{ \begin{matrix}q_{i} & se v(q_{i}) = 1 \\ ¬q_{i} & se v(q_{i}) = 0 \end{matrix}

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 φ é q_{1}, portanto Δ_{φ} = {q_{1}} ou Δ_{φ} = {¬q_{1}}, e o problema se reduz a mostrar que q_{1} ⊢_{pc} q_{1} ou ¬q_{1} ⊢_{pc} ¬q_{1}, 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 daí Δ_{φ} ⊢_{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(φ) = {q_{1}, …, q_{n}} o conjunto das variáveis proposicionais que ocorrem em φ. Considere duas valorações v_{1} e v_{2} tais que v_{1} atribui 1 a todas as variáveis proposicionais de φ e v_{2} atribui 1 a todas, exceto a q_{n}, isto é, v_{2}(q_{n}) = 0. Pelo lema anterior, temos:

{q_{1}, q_{2}, …, q_{n}} ⊢_{pc} φ e {q_{1}, q_{2}, …, ¬q_{n}} ⊢_{pc} φ.

Pelo Teorema 3.3.16(b) obtemos

(∗) {q_{1}, q_{2}, …, q_{n−1}} ⊢_{pc} φ.

Repetindo este processo para valorações v_{3} e v_{4} tais que v_{3}(q_{i}) = 1 (1 ≤ i ≤ n − 2), v_{3}(q_{n−1}) = 0, v_{3}(q_{n}) = 1, e v_{4}(q_{i}) = 1 (1 ≤ i ≤ n − 2), v_{4}(q_{n−1}) = 0, v_{4}(q_{n}) = 0, temos, da mesma forma,

(∗∗) {q_{1}, q_{2}, …, ¬q_{n−1}} ⊢_{pc} φ.

Consequentemente, aplicando Teorema 3.3.16(b) em (∗) e (∗∗), obtemos

(∗ ∗ ∗) {q_{1}, q_{2}, …, q_{n−2}} ⊢_{pc} φ.

Observe que, utilizando valorações v_{1} e v_{2} conseguimos eliminar q_{n} em (∗), e em seguida utilizando v_{3} e v_{4} pudemos eliminar também q_{n−1} em (∗∗∗). Fica claro, entao, que repetindo este procedimento com 2^{n} valorações, obteremos ⊢_{pc} φ.

Observe que, neste ponto, para obter uma outra prova do Teorema de Completude Forte (a partir do Teorema de Completude Fraca) deveriamos primeiro dar uma prova independente do Teorema da Compacidade (isto é, que não utilize o Teorema de Completude Forte, como nós fizemos na prova do Corolário 3.4.8). Usando estes resultados (Completude Fraca e Compacidade semântica) junto com o Teorema da Dedução (sintático e semântico) conseguiriamos então uma outra prova do Teorema de Completude Forte. Deixamos os detalhes como exercício para o leitor.

3.5 Outras Axiomáticas

A axiomática PC que utilizamos na seção anterior possui apenas um axioma e diversas regras de inferência. Existem muitas outras axiomáticas, considerando a mesma linguagem (ou otras linguagens apropriadas) de LPC, mas com diferentes axiomas, e em geral utilizando apenas a regra de Modus Ponens.

A seguinte axiomática foi popularizada no conhecido livro de Mendelson [Mendelson], embora pertença a Hilbert e Bernays, e é sem dúvidas uma das axiomáticas de LPC mais divulgadas na literatura:

Definição 3.5.1. O sistema axiomático M para LPC escrito na linguagem Prop_{1} consiste dos seguintes axiomas e regras de inferência:

(Axioma 1)  φ ⇒ (ψ ⇒ φ)

(Axioma 2)  (φ ⇒ (ψ ⇒ γ)) ⇒ ((φ ⇒ ψ) ⇒ (φ ⇒ γ))

(Axioma 3)  (¬ψ ⇒ ¬φ) ⇒ ((¬ψ ⇒ φ) ⇒ ψ)

(Modus Ponens) \frac{φ φ ⇒ ψ}{ψ}

É possível mostrar que o sistema M equivale ao sistema PC, no sentido em que cada regra de M pode ser demonstrada em PC, e vice-versa, com as respectivas traduções entre linguagens: φ ⇒ ψ é representado como ¬φ ∨ ψ em Prop, e φ ∨ ψ é representado como ¬φ ⇒ ψ em Prop_{1}. Portanto, M satisfaz o Teorema da Dedução e o Teorema da Adequação Forte com relação à semântica de valorações da Definição 2.2.6(i).

Podemos considerar uma variante de M:

Definição 3.5.2. O sistema axiomático M_{1} para LPC escrito na linguagem Prop_{1} consiste dos seguintes axiomas e regras de inferência:

(Axioma 1)  φ ⇒ (ψ ⇒ φ)

(Axioma 2)  (φ ⇒ (ψ ⇒ γ)) ⇒ ((φ ⇒ ψ) ⇒ (φ ⇒ γ))

(Axioma 3)  ¬¬φ ⇒ φ

(Modus Ponens) \frac{φ φ ⇒ ψ}{ψ}

Com a mesma tradução entre linguagens considerada acima, pode-se provar que PC e M_{1} são sistemas equivalentes.

Ainda outro sistema que podemos mostrar equivalente a PC (e portanto a todos os demais) é o sistema M_{2}, que é obtido de M_{1}, substituindo-se (Axioma 3) por dois novos axiomas:

Definição 3.5.3. O sistema axiomático M_{2} para LPC é escrito na linguagem L(C^{3}), onde C^{3} é a assinatura obtida de C^{1} acrescentando uma constante ⊥ ∈ C_{0}^{3}, e consiste dos seguintes axiomas e regras de inferência:

(Axioma 1)  φ ⇒ (ψ ⇒ φ)

(Axioma 2)  (φ ⇒ (ψ ⇒ γ)) ⇒ ((φ ⇒ ψ) ⇒ (φ ⇒ γ))

(Axioma 3)  ⊥ ⇒ φ

(Axioma 4)  ((φ ⇒ ψ) ⇒ φ) ⇒ φ

(Modus Ponens) \frac{φ φ ⇒ ψ}{ψ}

O último axioma de M_{2} é conhecido como “Lei de Peirce” (devido ao lógico e filósofo norte-americano Charles S. Peirce). A semântica de L(C^{3}) a ser tomada consiste basicamente das valorações v para Prop_{1} tais que v(⊥) = 0. Pode-se provar então que M_{2} satisfaz o Teorema da Dedução e o Teorema da Adequação Forte com relação à semântica de valorações que acabamos de mencionar.

Um outro tipo de axiomática que pode-se introduzir lida diretamente com conjuntos de fórmulas (cf. [CR]). Podemos interpretar intuitivamente um conjunto Γ de fórmulas como a disjunção de seus elementos. Dessa forma, para Γ finito, “Γ, φ” denota a disjunção dos elementos de Γ ∪ {φ}. Lembremos que φ ∧ ψ é representado por ¬(¬φ ∨ ¬ψ) em Prop.

Definição 3.5.4. O sistema CR definido sobre C^{0} é da seguinte forma:

Axiomas: Γ, φ, ¬φ Regras:

R_{1}  \frac{Γ, φ}{Γ, φ ∨ ψ}  R_{2} \frac{Γ, ψ}{Γ, φ ∨ ψ}

R_{3}  \frac{Γ, φ  Γ, ψ}{Γ, φ ∧ ψ}  R_{4} \frac{Γ, φ}{Γ, ¬¬φ}

Corte \frac{Γ, φ  Γ, ¬φ}{Γ}

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} ⋁_{i=1}^{n} φ_{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 demonstrada por G. Gentzen, num teorema conhecido como “Hauptsatz”, com conseqüências profundas para os fundamentos da matemática.

Finalizamos esta seção mencionando um teorema importante (e surpreendente) da lógica proposicional, o Teorema da Interpolação de Craig:

Teorema 3.5.5. (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 exercí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 capítulo mostrando duas axiomatizações não completas de 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, 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 axiomá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 C^{4} dada por C_{0}^{4} = {⊥}, C_{2}^{4} = {∨, ⇒} e C_{n}^{4} = ∅ nos outros casos. O sistema axiomático P escrito na linguagem L(C^{4}) consiste dos seguintes axiomas e regras de inferência:

(Ax1) (φ ∨ φ) ⇒ φ

(Ax2) φ ⇒ (ψ ∨ φ)

(Ax3) (φ ⇒ ψ) ⇒ ((γ ∨ φ) ⇒ (ψ ∨ γ))

(MP) \frac{φ φ ⇒ ψ}{ψ}

Definição 3.6.2. Uma valoração para P é uma função v : L(C^{4}) → 2 tal que:

1. v(⊥) = 0;

2. v(φ ∨ ψ) = ∨(v(φ), v(ψ));

3. v(φ ⇒ ψ) = ⇒(v(φ), v(ψ)),

onde ∨ : L(C^{4})^{2} → 2 e ⇒: L(C^{4})^{2} → 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, Prop_{1} e Prop_{2}, 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 valoraçõ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(C^{4})) que não é demonstrável em P. Considere a fórmula φ = (⊥ ⇒ p_{0}). Claramente φ é uma tautologia. Provaremos que φ não é demonstrável em P usando a 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(p_{0}) = 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 LPC é a ausência de axiomas e regras governando o sí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 representam 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 incompletude é 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(C^{4}) é a extensão de P obtida pelo acréscimo dos seguintes axiomas a P (onde ¬φ denota φ ⇒ ⊥):

(Ax4) ⊥ ⇒ φ

(Ax5) φ ⇒ (¬φ ⇒ ψ)

(Ax6) ¬¬φ ⇒ φ

(Ax7) φ ⇒ ¬¬φ

(Ax8) ¬φ ∨ φ

Primeiro de tudo, observemos que os acréscimos feitos ao sistema P são classicamente corretos.

Proposição 3.6.6. O sistema P^{+} é correto com relação à semântica clássica de valorações v tais que v(⊥) = 0.

Demonstração: Imediata.

Para provar a incompletude de P^{+} com relação à semântica clássica introduzimos uma semântica alternativa para o sistema, tal que P^{+} é correto com relação a essa semântica; porém, essa semântica não valida uma certa tautologia clássica.

Definição 3.6.7. Seja 3 = \{0, \frac{1}{2}, 1\}. Uma valoração^{∗} para P^{+} é uma função v : L(C^{4}) → 3 tal que:

1. v(⊥) = 0;

2. v(φ ∨ ψ) = ∨(v(φ), v(ψ));

3. v(φ ⇒ ψ) = ⇒(v(φ), v(ψ)),

onde ∨ : L(C^{4})^{2} → 3 e ⇒: L(C^{4})^{2} → 3 são as funções de verdade definidas pelas matrices abaixo.

\begin{matrix}∨ & 1 & ^{1}/_{2} & 0 \\ 1 & 1 & 1 & 1 \\ ^{1}/_{2} & 1 & 0 & 0 \\ 0 & 1 & 0 & 0 \end{matrix}  \begin{matrix}⇒ & 1 & ^{1}/_{2} & 0 \\ 1 & 1 & 0 & 0 \\ ^{1}/_{2} & 1 & ^{1}/_{2} & 1 \\ 0 & 1 & 1 & 1 \end{matrix}

(Aqui, o primeiro argumento das funções ∨ e ⇒ é dado pela primeira coluna de cada matriz, e o segundo argumento vem dado pela primeira linha de cada matriz; por exemplo, ⇒(\frac{1}{2}, 1) = 1.) A noção de conseqüência semântica ⊧_{∗} é definida como segue: Γ ⊧_{∗} φ se, para toda valoração^{∗} v, se v(γ) = 1 para toda γ ∈ Γ, então v(φ) = 1.

Note que a tabela-verdade para a negação ¬p := ⇒(p, 0) é a seguinte:

\begin{matrix}p & ¬p \\ 1 & 0 \\ ^{1}/_{2} & 1 \\ 0 & 1 \end{matrix}

Proposição 3.6.8. O sistema P^{+} é correto com relação à semântica de valorações^{∗} da Definição 3.6.7.

Demonstração: Uma verificação rotineira, que deixamos como exercício para o leitor.

Proposição 3.6.9. O sistema P^{+} não é completo com relação à semântica de valorações clássicas.

Demonstração: A fórmula φ = (p_{0} ⇒ p_{0}) é uma tautologia clássica, porém não é uma tautologia com relação à semântica de valorações^{∗} para P^{+} introduzida na Definição 3.6.7. Com efeito, qualquer valoração^{∗} v tal que v(p_{0}) = \frac{1}{2} produz v(φ) = \frac{1}{2}, portanto |̸=_{∗} φ. Pela Proposição 3.6.8 temos que ⊬_{p^{+}} φ. Logo, P^{+} não é uma axiomática completa para LPC.

Como conseqüência imediata da prova da Proposição 3.6.9 obtemos que P^{+} não satisfaz o Teorema da Dedução: com efeito, temos que p_{0} ⊢_{p^{+}} p_{0}, porém ⊬_{p^{+}} (p_{0} ⇒ p_{0}). O mesmo fenômeno acontece com a relação de conseqüência semântica ⊧_{∗}.

3.7 Exercícios

1. Prove o Teorema 3.2.6.

2. Prove o Lema 3.2.8.

3. Seja S um sistema axiomático definido sobre uma assinatura C que contém (entre outras coisas) um conectivo binário c ∈ C_{2}. Suponha que existe uma relação de conseqüência semântica ⊧ determinada por um conjunto de valorações v : L(C) → 2 tal que as seguintes propriedades são satisfeitas, para todo conjunto Γ ∪ {φ, ψ} ⊆ L(C):

(a) Se Γ ⊧ φ então existe Γ_{0} ⊆ Γ finito tal que Γ_{0} ⊧ φ;

(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 M_{1} são equivalentes.

7. Mostre que os sistemas PC e M_{2} são equivalentes.

8. Mostre que os sistemas PC e CR são equivalentes.

9. Mostre que em cada um dos sistemas PC, M_{1} e M_{2} todos os axiomas e regras são independentes (i.e., retirando-se algum axioma ou regra o sistema não é mais completo). Sugestão: use tabelas trivalentes “esdrúxulas” que modelem todas as regras menos uma delas.

10. 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 introduzido independentemente por Gentzen e Jaśkowski):

(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) ¬¬φ ⊢ φ

11. Um operador de conseqüência de Tarski é uma operação entre conjuntos 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).

Mostre que Cn(Γ) = {φ ∈ L(C) : Γ ⊢_{s} φ} é um operador de conseqüência, para todo sistema axiomático S.

12. 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

\frac{Γ, φ Γ, ¬φ}{Γ},

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 daí, use a hipótese de indução.

13. Prove o Teorema da Interpolação 3.5.5.

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}) ≠ ∅ (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 Γ |̸= φ_{2} então Γ ∪ {¬φ_{2}} é consistente, e daí 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.

14. Prove a Proposição 3.6.8.

3.8 Notas Bibliográficas

[CR]- Carnielli, W. A. e Rathjen, M., Hydrae and Subsystems of Arithmetic, Int. Berch. Institut für math. Logik und Grudlagenforschun, Univ. Münster

[Beth]- Beth, E. W., “The Foundations of Mathematics”, North-Holland (1959)

[Hintikka]- Hintikka, K. J. J., Form and Content in Quantification Theory Acta Philosophica Fennica 8, 7-55 (1955)

[Gentzen]- Gentzen, G., Untersuchungen über das logische Schliessen, Mathematische Zeitschrift 39, 176-210, 405-431 (1935)

[Mendelson]- Mendelson, E., “Introduction to mathematical logic”, The University series in undergraduate mathematics, Van Nostrand, Princeton (1966.)

[Smullyan]- Smullyan, R. M., “First-Order Logic”, Springer-Verlag (1968)