FUNDAMENTOS DE MATEMÁTICA - ELAINE PIMENTEL

Prévia do material em texto

Fundamentos de Matema´tica
Elaine Gouveˆa Pimentel
12 de marc¸o de 2008
Resumo
O presente texto visa descrever alguns aspectos da fundamentac¸a˜o da
matema´tica, mostrando, a partir de uma visa˜o histo´rica, como alguns
conceitos de matema´tica foram formalizados. A eˆnfase sera´ sobre a teoria
de conjuntos e “resoluc¸a˜o” de paradoxos. Tambe´m sera´ dada uma apre-
sentac¸a˜o formal da teoria de provas, onde sistemas lo´gicos servira˜o como
ferramenta para a fundamentac¸a˜o de conceitos tais como a “demonstrac¸a˜o
por absurdo”. Por fim, sera´ apresentada o teorema da incompletude de
Go¨del que diz, basicamente, que dentro de um determinado ramo da ma-
tema´tica que possui um nu´mero finito de axiomas (como, por exemplo,
a aritme´tica de Peano), existem sempre teoremas (ou seja, proposic¸o˜es
verdadeiras) que na˜o podem ser provados.
1
Suma´rio
1 Fundamentos da matema´tica 4
2 Lo´gica matema´tica (cla´ssica) 4
2.1 Semaˆntica . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
2.1.1 Tabela da verdade . . . . . . . . . . . . . . . . . . . . . . 7
2.1.2 A´lgebra de Boole . . . . . . . . . . . . . . . . . . . . . . . 8
3 Lo´gica intuicionista 10
3.1 Semaˆntica . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
4 Lo´gica e Matema´tica 13
5 Matema´tica como uma cieˆncia independente 13
5.1 A aritmetizac¸a˜o da Ana´lise . . . . . . . . . . . . . . . . . . . . . 14
5.2 Crite´rios para a fundamentac¸a˜o . . . . . . . . . . . . . . . . . . . 15
6 Sistema de Frege 16
6.1 Ide´ias ba´sicas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16
6.2 O sistema formal . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
6.3 Paradoxos e a teoria de tipos de Russell . . . . . . . . . . . . . . 20
7 Teoria de conjuntos de Zermelo-Fraenkel 21
7.1 Ide´ias ba´sicas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
7.2 Formalizac¸a˜o de ZF . . . . . . . . . . . . . . . . . . . . . . . . . 22
7.3 Axioma da escolha . . . . . . . . . . . . . . . . . . . . . . . . . . 24
8 O programa de Hilbert e a incompletude de Go¨del 26
8.1 O programa de Hilbert . . . . . . . . . . . . . . . . . . . . . . . . 27
8.2 Teoremas de incompletude de Go¨del . . . . . . . . . . . . . . . . 28
8.3 O me´todo de prova dos teoremas de Go¨del: func¸o˜es recursivas . . 29
8.3.1 Prova do primeiro teorema de incompletude de Go¨del . . 31
8.3.2 Prova do segundo teorema de incompletude de Go¨del . . . 34
9 λ-calculus e computabilidade 34
10 λ-calculus tipado simples 36
10.1 Tipos . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
10.2 Sistemas de Tipos . . . . . . . . . . . . . . . . . . . . . . . . . . 38
10.3 Outras propriedades de sistemas de tipos . . . . . . . . . . . . . 40
10.4 Tipos Simples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
10.5 Tipo produto, tipo soma e tipos recursivos . . . . . . . . . . . . . 43
10.5.1 Produtos cartesianos . . . . . . . . . . . . . . . . . . . . . 43
10.5.2 Somas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
10.6 Polimorfismo . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
10.7 Infereˆncia de tipos . . . . . . . . . . . . . . . . . . . . . . . . . . 45
11 Isomorfismo de Curry-Howard 45
2
12 Tipos e Significados: Semaˆntica 47
12.1 Semaˆntica Denotacional . . . . . . . . . . . . . . . . . . . . . . . 48
12.2 Semaˆntica Operacional . . . . . . . . . . . . . . . . . . . . . . . . 50
13 Semaˆntica denotacional do λ-calculus 53
13.1 Conjunto parcialmente ordenado (POSET) . . . . . . . . . . . . 54
13.2 Ordem parcial completa (CPO) . . . . . . . . . . . . . . . . . . . 55
14 Lo´gica Linear 57
14.1 Semaˆntica . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58
15 Lo´gica e Cieˆncia da Computac¸a˜o 59
16 Logical frameworks 60
16.1 Lo´gica Linear como framework para especificar sistemas de sequ¨en-
tes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61
A De deduc¸a˜o natural para ca´lculo de sequ¨entes 62
A.1 Deduc¸a˜o natural . . . . . . . . . . . . . . . . . . . . . . . . . . . 62
A.2 Ca´lculo de sequ¨entes . . . . . . . . . . . . . . . . . . . . . . . . . 63
A.2.1 Cut elimination . . . . . . . . . . . . . . . . . . . . . . . . 65
3
1 Fundamentos da matema´tica
O termo “fundamentos da matema´tica” (em ingleˆs, foundations of mathematics)
e´ em geral usado para certas a´reas da matema´tica, como por exemplo a lo´gica
matema´tica, teoria de conjuntos axioma´tica, teoria de provas, teoria de modelos,
teoria da recursa˜o. A procura de fundamentos para a matema´tica e´ tambe´m
uma questa˜o central de filosofia da matema´tica: quando podemos dizer que uma
afirmac¸a˜o matema´tica pode ser chamada verdadeira?
No paradigma matema´tico dominante atualmente, a verdade de uma afir-
mativa pode ser derivada dos axiomas da teoria de conjuntos usando regras de
lo´gica formal.
A preocupac¸a˜o em estabelecer uma base lo´gica e filoso´fica para a matema´tica
comec¸ou com os Elementos de Euclides. Essencialmente, Euclides foi o primeiro
a questionar quando os axiomas de um certo ca´lculo (no seu caso, a geometria),
podem assegurar completeza e consisteˆncia. Na era moderna, esse debate deu
origem a treˆs escolas de pensamento: logicismo, formalismo e intuicionismo.
Logicistas propo˜e que objetos matema´ticos abstratos devem ser inteiramente
desenvolvidos a partir de ide´ias ba´sicas de conjuntos e pensamento racional ou
lo´gico.
Formalistas acreditavam que a matema´tica era a manipulac¸a˜o de confi-
gurac¸o˜es de s´ımbolos de acordo com regras prescritas, um jogo, independente
de qualquer interpretac¸a˜o f´ısica dos s´ımbolos.
Intuicionistas rejeitam certos conceitos de lo´gica e a noc¸a˜o que um me´todo
axioma´tico seria suficiente para explicar toda a matema´tica, e veˆem a ma-
tema´tica como uma atividade intelectual que lida com construc¸o˜es mentais
(construtivismo), independente da linguagem e de qualquer realidade externa.
O presente texto diz respeito apenas ao logicismo e, portanto, visa estudar as
ide´ias ba´sicas da teoria de conjuntos (de Zermelo-Fraenkel), bem como a teoria
de provas, tendo como pano de fundo sempre a lo´gica cla´ssica.
2 Lo´gica matema´tica (cla´ssica)
A lo´gica matema´tica lida com a formalizac¸a˜o e a ana´lise de tipos de argu-
mentac¸a˜o utilizados em matema´tica.
Desta forma, os sistemas lo´gicos formais utilizados para esse fim devem ser
ferramentas adequadas para provar proposic¸o˜es. Parte do problema com a for-
malizac¸a˜o da argumentac¸a˜o matema´tica e´ a necessidade de se especificar de
maneira precisa uma linguagem matema´tica formal. Linguagens naturais, as-
sim como o portugueˆs ou ingleˆs, na˜o servem a este propo´sito: elas sa˜o muito
complexas e em constante modificac¸a˜o. Por outro lado, linguagens formais como
(algumas) linguagens de programac¸a˜o, que tambe´m sa˜o rigidamente definidas,
sa˜o muito mais simples e menos flex´ıveis que as linguagens naturais. Utilizamos
enta˜o um sistema lo´gico formal.
Um sistema lo´gico formal e´ composto, ale´m da sintaxe (ou notac¸a˜o), de uma
especificac¸a˜o cuidadosa de regras de argumentac¸a˜o (regras de infereˆncia), bem
como de alguma noc¸a˜o de como interpretar e dar um significado a sentenc¸as (ou
proposic¸o˜es) da linguagem adotada (semaˆntica).
A linguagem usada atualmente para formalizar a argumentac¸a˜o matema´tica
e´ a lo´gica (cla´ssica) de primeira ordem, juntamente com um sistema formal de
4
provas, que sera˜o apresentados a seguir.
Comec¸aremos pela sintaxe (ou notac¸a˜o). A ide´ia e´ que expresso˜es va´lidas
da linguagem lo´gica sa˜o sequ¨eˆncias especiais de s´ımbolos de um dado alfabeto,
geradas por uma definic¸a˜o indutiva (grama´tica). Desta forma, partindo do
alfabeto ba´sico:
ALFABETO
Letras : A,B,C, ...
Conectivos : ¬,∧,∨,⇒,⊥
Agrupamento : (·)
as fo´rmulasda lo´gica cla´ssica proposicional de primeira ordem sa˜o dadas pela
grama´tica:
GRAMA´TICA
F ::= A|(¬F )|(F ∧ F )|(F ∨ F )|(F ⇒ F )|⊥|∀x.F |∃x.F
que significa que uma fo´rmula F pode ser uma proposic¸a˜o atoˆmica (ou seja,
uma fo´rmula A sem conectivos lo´gicos), a negac¸a˜o de uma fo´rmula, a conjunc¸a˜o
de duas fo´rmulas, a disjunc¸a˜o de duas fo´rmulas, implicac¸a˜o, falso ou fo´rmulas
quantificadas (para todo e existe).
Vale ressaltar que a grama´tica acima na˜o e´ minimal. De fato, podemos, por
exemplo, identificar ¬A com A⇒ ⊥. Mas escrever a negac¸a˜o de forma concisa
facilitara´ a visualizac¸a˜o de provas em deduc¸a˜o natural, que veremos a seguir.
Outra observac¸a˜o importante e´ que ⊥ na˜o e´ uma fo´rmula atoˆmica, mas sim o
zero-a´rio do conectivo ∨.
A segunda parte de um sistema lo´gico consiste em estabelecer os axiomas e
as regras de infereˆncia do sistema.
Existem diversas formas de se definir regras e axiomas de um sistema lo´gico
formal. Comec¸aremos por descrever rapidamente os sistemas de Hilbert.
Os sistemas de Hilbert (tambe´m chamados de sistemas axioma´ticos) sa˜o
muito utilizados por filo´sofos para formalizar a argumentac¸a˜o lo´gica. Tais sis-
temas sa˜o, em geral, fa´ceis de serem compreendidos, mas extremamente dif´ıceis
de serem usados para provar teoremas. Sistemas de Hilbert possuem um grande
nu´mero de axiomas ba´sicos, como por exemplo:
⊢ A ⊃ A ∨B ou ⊢ A ⊃ (B ⊃ A)
e no caso da lo´gica proposicional existe apenas uma regra de infereˆncia: modus
ponens (veja definic¸a˜o abaixo). Desta forma, derivac¸o˜es sa˜o sequ¨eˆncias lineares
que comec¸am com instaˆncias dos axiomas que sa˜o decompostos pela regra de
infereˆncia, ate´ que a conclusa˜o e´ atingida.
De maneira oposta, em sistemas de deduc¸a˜o natural existem apenas regras de
infereˆncia, ale´m de afirmativas que comec¸am as derivac¸o˜es, como por exemplo:
(A)
...
B
A⇒ B
Neste caso, os pontos verticais indicam a derivac¸a˜o de B a partir de A, que por
sua vez e´ descartada na linha de infereˆncia (procedimento indicado pelo uso de
5
pareˆntesis em torno de A) para produzir A ⇒ B. Desta forma, uma prova de
B depende de uma prova de A, enquanto que a prova de A⇒ B na˜o.
Utilizaremos aqui uma presentac¸a˜o mais moderna de deduc¸a˜o natural, que
utiliza um sistema a` la ca´lculo de sequ¨entes (veja Sec¸a˜o A.2), onde as afirmativas
a serem “descartadas” na linha de infereˆncia sa˜o anotadas no contexto. Isto
e´, os nodos da a´rvore de uma derivac¸a˜o deixam de ser fo´rmulas para se tornar
sequ¨entes da forma Γ ⊢ C, onde Γ e´ um conjunto de fo´rmulas chamado contexto
ou antecedente enquanto que C uma fo´rmula chamada sucedente. Desta forma,
a regra acima pode ser re-escrita como:
A ⊢ B
⊢ A⇒ B
Nesta presentac¸a˜o, a lo´gica cla´ssica tem um e apenas um axioma:
Γ, A ⊢ A Inicial
que diz que uma fo´rmula e´ prova´vel a partir de si mesma.
Como exemplo de regra de infereˆncia, apresentamos aqui o famoso modus
ponens1:
Γ ⊢ A Γ ⊢ A⇒ B
Γ ⊢ B (⇒ E)
Informalmente, essa regra diz que se temos uma func¸a˜o do tipo A ⇒ B e um
argumento do tipo A, enta˜o podemos aplicar a func¸a˜o ao argumento e obter um
resultado do tipo B.
Veja a Figura 1 para lista completa das regras de deduc¸a˜o natural para a
lo´gica ca´ssica.
Vale a pena observar que, em lo´gica ca´ssica, vale o ta˜o comentado princ´ıpio
do meio exclu´ıdo. Ou seja, a proposic¸a˜o
p ∨ ¬p
e´ sempre va´lida. Isso significa que uma fo´rmula e´ sempre ou verdadeira, ou
falsa.
Essa afirmac¸a˜o e´ extremamente na˜o construtiva, uma vez que nada se pode
dizer de qual das das opc¸o˜es e´ valida. Existe uma se´rie de consequ¨eˆncias que
derivam dessa fo´rmula, e esse sera´ objeto de um estudo cuidadoso durante o
decorrer destas notas.
A prova formal do princ´ıpio do meio exclu´ıdo utilizando as regras de deduc¸a˜o
natural (Figura 1) e´:
¬(p ∨ ¬p), p ⊢ p (Inicial)
¬(p ∨ ¬p), p ⊢ p ∨ ¬p (∨I1) ¬(p ∨ ¬p) ⊢ ¬(p ∨ ¬p) (Inicial)
¬(p ∨ ¬p), p ⊢ ⊥ (¬E)
¬(p ∨ ¬p) ⊢ ¬p (¬I)
¬(p ∨ ¬p) ⊢ p ∨ ¬p (∨I2) ¬(p ∨ ¬p) ⊢ ¬(p ∨ ¬p) (Inicial)
¬(p ∨ ¬p) ⊢ ⊥ (¬E)
⊢ ¬¬(p ∨ ¬p) (¬I)
⊢ p ∨ ¬p (DN)
1Esta e´ uma regra de eliminac¸a˜o, pro´pria de sistemas descritos em deduc¸a˜o natural. Veja
o Apeˆndice A.2 para a diferenc¸a entre ca´lculo de sequ¨entes e deduc¸a˜o natural.
6
Γ, A ⊢ A Inicial
Γ ⊢ A Γ ⊢ B
Γ ⊢ A ∧B (∧I)
Γ ⊢ A ∧B
Γ ⊢ A (∧E1)
Γ ⊢ A ∧B
Γ ⊢ B (∧E2)
Γ ⊢ A
Γ ⊢ A ∨B (∨I1)
Γ ⊢ B
Γ ⊢ A ∨B (∨I2)
Γ ⊢ A ∨B Γ, A ⊢ C Γ, B ⊢ C
Γ ⊢ C (∨E)
Γ, A ⊢ B
Γ ⊢ A⇒ B (⇒ I)
Γ ⊢ A Γ ⊢ A⇒ B
Γ ⊢ B (⇒ E)
Γ ⊢ ⊥
Γ ⊢ A (⊥E)
Γ, A ⊢ ⊥
Γ ⊢ ¬A (¬I)
Γ ⊢ A Γ ⊢ ¬A
Γ ⊢ ⊥ (¬E)
Γ ⊢ ¬(¬A)
Γ ⊢ A (DN)
Figura 1: Deduc¸a˜o natural para a lo´gica ca´ssica
A B ¬A A ∧B A ∨B A⇒ B ⊥
V V F V V V F
V F F F V F F
F V V F V V F
F F V F F V F
Tabela 1: Tabela da verdade
2.1 Semaˆntica
Com relac¸a˜o a` semaˆntica (significado dos s´ımbolos lo´gicos), no caso proposici-
onal (isto e´, sem os quantificadores) o significado de fo´rmulas em lo´gica pode
ser dado de maneira trivial, baseado na tabela da verdade, ou um pouco mais
elaborada utilizando, por exemplo, a´lgebras de Boole.
2.1.1 Tabela da verdade
A` cada s´ımbolo ba´sico da lo´gica e´ dado um valor (semaˆntico): verdadeiro V ou
falso F . Dependendo desse valor, chegamos ao valor das fo´rmulas formadas a
partir da grama´tica analisando a Tabela 1.
A semaˆntica dos quantificadores e´ mais complicada e na˜o sera´ objeto de
estudo neste curso.
Atrave´s dessa ana´lise semaˆntica, podemos ver, por exemplo, por que as
7
fo´rmulas A⇒ B, ¬B ⇒ ¬A e ¬(A ∧ ¬B) possuem o mesmo comportamento:
A B A⇒ B ¬B ⇒ ¬A ¬(A ∧ ¬B)
V V V V V
V F F F F
F V V V V
F F V V V
Ou seja, provas matema´ticas do fato:
B segue de A
utilizando qualquer dos seguintes me´todos:
direto, contra-rec´ıproco, por absurdo
sa˜o equivalentes.
2.1.2 A´lgebra de Boole
Nesta sec¸a˜o mostraremos como utilizar a´lgebras de Boole para estabelecer a
semaˆntica da lo´gica cla´ssica proposicional. Ale´m de ser interessante por si so´, po-
deremos utilizar alguns conceitos aqui estabelecidos para a semaˆntica da lo´gica
intuicionista (ver Sec¸a˜o 3.1).
Comec¸aremos por relembrar o conceito de ane´is
Definic¸a˜o 1 Um conjunto na˜o vazio R fechado com relac¸a˜o a`s operac¸o˜es + e
· e´ dito um anel associativo se ∀ a, b e c em R:
1. a+ b = b+ a
2. (a+ b) + c = a+ (b+ c)
3. ∃0 ∈ R tal que a+ 0 = a ∀a ∈ R
4. ∀a.∃(−a) tal que a+ (−a) = 0
5. (a.b).c = a.(b.c)
6. a.(b+ c) = a.b+ a.c e (b + c).a = b.a+ c.a
Os ı´tens (1)−(4) dizem queR e´ um grupo abeliano com relac¸a˜o a +, enquanto
que (5) diz que R e´ um semigrupo com operador ·.
Dizemos ainda que R e´ um anel com unidade se ∃1 ∈ R tal que ∀a ∈ R
a.1 = 1.a = a. Ale´m disso, R e´ um anel comutativo se ∀a, b ∈ R, a.b = b.a.
Exemplo 1 a) (Z,+, ·) e´ um anel comutativo com unidade.
• R = conjunto dos inteiros pares e´ anel comutativo sem unidade.
b) (Q,+, ·) e´ anel comutativo com unidade. Ale´m disso, os elementos de Q
diferentes de zero formam um grupo abeliano com relac¸a˜o a` multiplicac¸a˜o.
Um anel com esta propriedade e´ chamado corpo.
c) (Z6,+, ·) e´ um anel comutativo com unidade, mas na˜o um corpo.
8
Definic¸a˜o 2 (A´lgebra Booleana) Uma a´lgebra Booleana e´ um anel (R,+, ·,0,1)
no qual cada elemento e´ idempotente com relac¸a˜o a` multiplicac¸a˜o (ou seja, igual
ao seu quadrado).
Exemplo 2 a) (P(A),∆,∩, ∅, A) e´ uma a´lgebra booleana, onde ∆ e´ a operac¸a˜o
de diferenc¸a sime´trica:
X∆Y = (X ∪ Y )− (X ∩ Y ) = (X ∩ (A− Y )) ∪ ((A −X) ∩ Y ).
b) Z2 e´ a u´nica a´lgebra de Boole que tambe´m e´ um corpo. De fato, seja B uma
a´lgebra de Boole que e´ um corpo. Para todo x ∈ B, x2 = x ≡ x(x−1) = 0.
Enta˜o, se B e´ um domı´nio de integridade, temos x = 0 ou x = 1. Ou
seja, B e´ isomorfo a Z2.
Propriedade 1 1. Em qualquer a´lgebra de Boole, todo elemento e´ seu pro´prio
inversoaditivo.
2. Toda a´lgebra de Boole e´ comutativa.
Prova Como (a+ b)2 = (a+ b) e (a+ b)2 = a2 + a.b+ b.a+ b2 enta˜o:
a.b+ b.a = 0 (1)
Fazendo b = 1, obtemos a = −a. Para a segunda parte, sabemos que a.b e´ o
inverso de a.b. Mas por (1), a.b tambe´m e´ o inverso de b.a e portanto a.b = b.a.
A semaˆntica da lo´gica cla´ssica proposicional sera´ dada a seguir.
Seja F o conjunto de todas as fo´rmulas proposicionais da lo´gica cla´ssica e ∼
a seguinte relac¸a˜o de equivaleˆncia:
ϕ ∼ ψ se e somente se ⊢ ϕ⇒ ψ e ⊢ ψ ⇒ ϕ
Seja F∼ = F/ ∼= {[ϕ]∼ : ϕ ∈ F}. As seguintes operac¸o˜es sobre F∼ sa˜o bem
definidas:
[α]∼ ∪ [β]∼ = [α ∨ β]∼ [α]∼ ∩ [β]∼ = [α ∧ β]∼
−[α]∼ = [¬α]∼ [α]∼ → [β]∼ = [α⇒ β]∼
[α]∼ ↔ [β]∼ = [α⇔ β]∼ [α]∼ = [β]∼ = [α< β]∼
Chame 0 = [⊥]∼ e 1 = [⊤]∼, onde ⊤ = ⊥ ⇒ ⊥. Enta˜o (F∼,=,∩,0,1) e´
uma a´lgebra de Boole.
Observe que
[⊤]∼ = {ϕ : ∅ ⊢ ϕ}
ou seja, 1 e´ a classe das tautologias. Observe tambe´m que
−a ∩ a = [⊥]∼ e − a ∪ a = [⊤]∼.
a u´ltima igualdade sendo equivalente ao princ´ıpio do meio exclu´ıdo.
Seja PVc o conjunto de varia´veis proposicionais da lo´gica cla´ssica. Dizemos
que uma valuac¸a˜o v em F∼ e´ uma aplicac¸a˜o v : PVc −→ {0,1}.
Dada uma valuac¸a˜o v em F∼, definimos a aplicac¸a˜o [[•]]vc : F −→ {0,1} de
maneira trivial:
9
[[p]]vc = v(p) para p ∈ PV
[[⊥]]vc = 0
[[ϕ ∨ ψ]]vc = [[ϕ]]vc ∪ [[ψ]]vc
[[ϕ ∧ ψ]]vc = [[ϕ]]vc ∩ [[ψ]]vc
[[ϕ⇒ ψ]]vc = [[ϕ]]vc → [[ψ]]vc
Escreveremos Γ |= ϕ sempre que [[Γ]]vc = 1 implica [[ϕ]]vc = 1 para todos B e
v relacionados com a a´lgebra de Boole F∼.
O seguinte teorema diz que o modelo semaˆntico baseado em a´lgebra de Boole
e´ completo e “sound”:
Teorema 1 As seguintes condic¸o˜es sa˜o equivalentes:
1. Γ ⊢ ϕ;
2. Γ |= ϕ.
3 Lo´gica intuicionista
Como descrito na Sec¸a˜o 2, o entendimento cla´ssico de lo´gica e´ baseado na noc¸a˜o
de verdade. Ou seja, a veracidade de uma afirmativa e´ “absoluta” e indepen-
dente de qualquer argumentac¸a˜o, crenc¸a ou ac¸a˜o.
Desta forma, afirmativas sa˜o ou falsas ou verdadeiras (princ´ıpio do meio
excu´ıdo), onde falso e´ a mesma coisa que na˜o verdadeiro (veja Tabela 1).
Claro que essa abordagem de pensamento e´ muito intuitiva e baseada em
experieˆncia e observac¸a˜o. Para um matema´tico preocupado em provar um teo-
rema, e´ importante a ide´ia de que toda afirmativa pode ser provada verdadeira
se uma prova e´ apresentada ou falsa se existe um contra-exemplo. Ale´m disso,
va´rias te´cnicas de demostrac¸a˜o utilizam implicitamente o princ´ıpio do meio ex-
clu´ıdo.
Considere o seguinte exemplo:
Teorema 2 Existem dois nu´meros irracionais x e y tais que xy e´ racional.
Prova A prova desse fato e´ bastante simples: se 2
√
2 e´ racional, enta˜o toma-
mos x = y =
√
2.
Caso contra´rio, tomamos x = 2
√
2 e y =
√
2.
Observe que na˜o temos como saber qual dos casos realmente acontece, porque
na˜o se sabe se 2
√
2 e´ racional ou irracional. Mas o princ´ıpio do meio exclu´ıdo
nos garante que uma das opc¸o˜es ocorre e isso e´ bastante natural de se aceitar.
Enta˜o, para o exemplo acima descrito, o problema se limita ao fato de que a
prova apresentada na˜o e´ construtiva.
Um caso mais se´rio surge com o seguinte teorema:
Teorema 3 Existem sete 7’s consecutivos na representac¸a˜o decimal do nu´mero
π.
Ora, ou algue´m algum dia chega a` representac¸a˜o de com um nu´mero de
casas decimais grande o suficiente de modo a encontrar sete 7’s consecutivos ou
enta˜o... na˜o se sabe!
Considere p a afirmativa:
10
existe uma prova de que existem sete 7’s consecutivos na representac¸a˜o
decimal do nu´mero π.
e chamemos de t o predicado dado pelo enunciado do Teorema 3. Parece claro
que p ⇔ t. Mas isso vale somente se p e´ verdadeiro. Se p e´ falso na˜o se pode
dizer que t e´ falso.
Esse e´ um exemplo de uma afirmativa para a qual na˜o existe sentido a sua
negac¸a˜o. Ou seja, o princ´ıpio do meio exclu´ıdo na˜o se encaixa em um sistema que
possui esse tipo de “teorema”. Observe que aqui “infinitude” esta´ envolvida.
Ou seja, muito provavelmente, provar o Teorema 3 significa testar todas as
(infinitas) possibilidades.
A lo´gica intuicionista abandona a ide´ia de verdade absoluta, e afirmativas
sa˜o consideradas va´lidas se e somente se existe uma prova construtiva da mesma.
Ou seja, o princ´ıpio do meio exclu´ıdo na˜o e´ mais va´lido.
Com relac¸a˜o ao sistema de provas da lo´gica intuicionista, em deduc¸a˜o natural
as regras sa˜o as mesmas das apresentadas na Figura 1, com excessa˜o da regra de
dupla negac¸a˜o, (DN). Ja´ em ca´lculo de seqe¨ntes, a presentac¸a˜o mais conhecida
e´ o sistema de Gentzen LJ , onde os sequ¨entes va´lidos possuem exatamente
uma fo´rmula como sucedente e as regras de weakening and contraction na˜o sa˜o
va´lidas a` direita. Isto e´, sa˜o consideradas todas as regras da Figura A.2 menos
as regras weakR e contR. Daremos maiores detalhes na Sec¸a˜o 8.
Exemplo 3 Todos os sequ¨entes abaixo sa˜o prova´veis em lo´gica cla´ssica:
1. ¬(p ∨ q) ⊢ (¬p ∧ ¬q)
2. (p ∨ q) ⊢ ¬(¬p ∧ ¬q)
3. (p ∨ q) ⊢ (¬p⇒ q)
4. ¬(p ∧ q) ⊢ (¬p ∨ ¬q)
5. ((p⇒ q)⇒ p) ⊢ p
6. ⊢ (p⇒ q) ∨ (q ⇒ p)
Mas apenas (1), (2) e (3) apresentam provas construtivas, isto e´, sa˜o prova´veis
intuicionisticamente.
3.1 Semaˆntica
Um dos modelos semaˆnticos mais populares para a lo´gica intuicionista e´ baseado
em a´lgebras de Heyting. Descreveremos aqui (de maneira resumida) a semaˆntica
para o caso proposicional [31].
Seja Φ o conjunto de todas as fo´rmulas proposicionais da lo´gica intuicionista,
considere Γ ⊆ Φ e seja ∼ a seguinte relac¸a˜o de equivaleˆncia:
ϕ ∼ ψ se e somente se Γ ⊢ ϕ⇒ ψ e Γ ⊢ ψ ⇒ ϕ
Seja LΓ = Φ/ ∼= {[ϕ]∼ : ϕ ∈ Φ} e defina uma ordem parcial ≤ sobre LΓ da
seguinte forma:
[ϕ]∼ ≤ [ψ]∼ se e somente se Γ ⊢ ϕ⇒ ψ.
11
Podemos tambe´m definir as seguintes (bem definidas) operac¸o˜es sobre LΓ:
[α]∼ ∪ [β]∼ = [α ∨ β]∼;
[α]∼ ∩ [β]∼ = [α ∧ β]∼;
−[α]∼ = [¬α]∼;
ou ainda ir mais adiante e mostrar que as operac¸o˜es ∩ e ∪ sa˜o operac¸o˜es “´ınfimo”
e “supremo” com relac¸a˜o a ≤, e que as leis de distributividade
(a ∪ b) ∩ c = (a ∩ c) ∪ (b ∩ c) e (a ∩ b) ∪ c = (a ∪ c) ∩ (b ∪ c)
sa˜o satisfeitas 2. A classe [⊥]∼ e´ o menor elemento (0) de LΓ e [⊤]∼, onde
⊤ = ⊥ ⇒ ⊥, e´ o maior elemento (1). Temos tambe´m que [⊤]∼ = {ϕ : Γ ⊢
ϕ}. Entretanto, existem algumas dificuldades (ja´ esperadas) com a operac¸a˜o
complementar:
−a ∩ a = [⊥]∼ mas na˜o necessariamente − a ∪ a = [⊤]∼.
Oma´ximo que podemos afirmar e´ que−a e´ omaior elemento tal que −a∩a =
0. Chamamos −a de pseudo-complemento de a. Uma vez que a negac¸a˜o e´ um
caso especial de implicac¸a˜o (pois ¬a ≡ a ⇒ ⊥), o que foi dito acima merece
uma generalizac¸a˜o. Um elemento c e´ chamado um pseudo-complemento relativo
de a com relac¸a˜o a b se e somente se c e´ o maior elemento tal que a ∩ c ≤ b. O
pseudo-complemento relativo, caso existir, e´ denotado por a ⇀ b.
Na˜o e´ dif´ıcil de ver que na a´lgebra LΓ (comumente chamada de a´lgebra de
Lindenbaum), temos
[ϕ]∼ ⇀ [ψ]∼ = [ϕ⇒ ψ]∼.
Formalmente, uma a´lgebra de Heyting (ou a´lgebra pseudo-Booleana), e´ um
sistema alge´brico H que e´ um reticulado distributivo contendo o zero e que
possui um pseudo-complemento relativo definido para cada par de elementos.
Em particular, cada a´lgebra de Boolean e´ uma a´lgebra de Heyting com a ⇀ b
definido como −a ∪ b 3.
A semaˆntica da lo´gica intuicionista proposicional e´ dada pela aplicac¸a˜o [[•]]i,
definida a seguir.
Definic¸a˜o 3 Seja H = 〈H,∪,∩,⇀,−, 0, 1〉 uma a´lgebra de Heyting. Denota-
mos por PV ao conjunto de varia´veis proposicionais da lo´gica intuicionista.
i. Uma valuac¸a˜o v em H e´ uma aplicac¸a˜o v : PV −→ H.
ii. Dada uma valuac¸a˜o v em H, definimos a aplicac¸a˜o [[•]]vi : Φ −→ H por:
[[p]]vi = v(p) para p ∈ PV
[[⊥]]vi = 0
[[ϕ ∨ ψ]]vi = [[ϕ]]vi ∪ [[ψ]]vi
[[ϕ ∧ ψ]]vi = [[ϕ]]vi ∩ [[ψ]]vi
[[ϕ⇒ ψ]]vi = [[ϕ]]vi ⇀ [[ψ]]vi
2Ou seja, LΓ e´ um reticulado distributivo.3O exemplo mais conhecido de a´lgebra de Heyting que na˜o e´ uma a´lgebra de Boole e´ a
a´lgebra de conjuntos abertos de um espac¸o topolo´gico.
12
Escreveremos Γ |= ϕ sempre que [[Γ]]vi = 1 implica [[ϕ]]vi = 1 para todos H e
v relacionados com a a´lgebra de Heyting H.
O seguinte teorema diz que o modelo semaˆntico baseado em a´lgebra de Hey-
ting e´ completo e “sound”:
Teorema 4 As seguintes condic¸o˜es sa˜o equivalentes:
1. Γ ⊢ ϕ;
2. Γ |= ϕ.
4 Lo´gica e Matema´tica
Para muitos, lo´gica na˜o faz parte da matema´tica. De fato, parece paradoxal di-
zer que a lo´gica e´ um ramo da matema´tica, uma vez que a lo´gica e´ o instrumento
utilizado para a formalizac¸a˜o da matema´tica.
Na realidade, o estudo da lo´gica como um modelo para a matema´tica, sendo
ao mesmo tempo uma parte da matema´tica na˜o forma um c´ırculo vicioso, mas
pode ser entendido como uma escada em espiral. Se a matema´tica esta´ no n-
e´simo degrau (chamado degrau intuitivo), o degrau n + 1 conte´m um modelo
reduzido, um proto´tipo (degrau formal). A passagem do degrau n para o degrau
n+ 1 e´ chamado formalizac¸a˜o.
Com relac¸a˜o a` lo´gica, a passagem do degrau n para o degrau n+ 1 implica
em aumentar a ordem. Enta˜o, a lo´gica cla´ssica de primeira ordem (que e´ um
ramo da matema´tica) da´ origem a` lo´gica de segunda ordem (que conte´m toda a
matema´tica), onde predicados podem ser quantificados, e na˜o apenas varia´veis.
E´ interessante tambe´m ressaltar que, nas a´reas cla´ssicas da matema´tica, o
propo´sito inicial e´ propor um modelo matema´tico para alguma situac¸a˜o mais
ou menos concreta. Com a lo´gica, acontece algo similar. A sua particularidade
reside no fato de que a “realidade” que a lo´gica visa descrever na˜o e´ fora do
mundo matema´tico, mas sim a pro´pria matema´tica. Desta forma, do mesmo
modo que um matema´tico na˜o confunde o ambiente f´ısico em que vive com um
espac¸o vetorial euclideano tri-dimensional, um pesquisador na a´rea de lo´gica
na˜o a confunde com a matema´tica sendo descrita.
Por fim, observe que tanto na matema´tica quanto na lo´gica, o estudo de mo-
delos da´ origem ao aparecimento de novos ramos de estudo, que aparentemente
nada ou pouco teˆm a ver com o objetivo inicial de descrever um “objeto”, seja ele
concreto ou na˜o. Desta forma, a lo´gica como disciplina passa a ter vida pro´pria,
e o seu estudo na˜o se limita ao caso cla´ssico. Isto justifica o aparecimento e
estudo de lo´gicas como a intuicionista, linear, fuzzy, modal, etc.
5 Matema´tica como uma cieˆncia independente
Existem diversas opinio˜es a respeito de como surgiu a matema´tica. Alguns ma-
tema´ticos tendem a considerar a f´ısica como a principal fonte de problemas e
ide´ias matema´ticas. Outros consideram a intuic¸a˜o matema´tica ligada principal-
mente com a estrutura abstrata de objetos matema´ticos (o que quer que venha
a ser isso) e portanto independente de outras cieˆncias. Essa dicotomia de pen-
samento vem desde os primo´rdios do estudo da matema´tica. Por exemplo, os
matema´ticos gregos desenvolveram a geometria axioma´tica e deram os primeiros
13
passos em lo´gica formal, mas na˜o possuiam nem mesmo um sistema nume´rico:
trabalhavam com comprimentos de segmentos de reta e suas razo˜es. Eles clara-
mente reconheciam pontos e retas como entidades abstratas e na˜o-f´ısicas, apesar
de saber que a geometria por eles desenvolvida podia ser aplicada a problemas
pra´ticos de medic¸a˜o de espac¸o, por exemplo.
O ca´lculo diferencial foi inventado ao mesmo tempo por Newton e Leibniz, o
primeiro claramente motivado por um forte sentido de realidade f´ısica, enquanto
que o segundo estava muito mais interessado em lo´gica e matema´tica formal.
De qualquer forma, existem va´rios pontos fundamentais nos quais a maioria
dos matema´ticos concorda, independentemente de convicc¸o˜es filoso´ficas, relaci-
onados a` natureza da matema´tica. A primeira e´ que a matema´tica e´ abs-
trata, e isso consiste essencialmente em argumentar com abstrac¸o˜es. A segunda
e´ que a verdade ou falsidade de uma proposic¸a˜o em matema´tica e´ determinada
por um processo de deduc¸a˜o, ou seja, mostrando que uma proposic¸a˜o pode
ser provada tendo como base alguns princ´ıpios ou verdades assumidas. Esse
processo difere de outras cieˆncias ao menos em um aspecto: todas as outras
cieˆncias (mesmo uma ta˜o abstrata quanto a f´ısica teo´rica) dependem de uma
certa quantidade de manipulac¸a˜o do mundo f´ısico. Ou seja, as hipo´teses e leis
sa˜o consideradas va´lidas apenas depois de serem testadas atrave´s de algum ex-
perimento. Em matema´tica, teoremas sa˜o provados (portanto estabelecendo a
sua veracidade) sem a necessidade de convalidar o resultado no mundo f´ısico.
Desta forma, o primeiro ingrediente dos estudos modernos dos fundamentos
da matema´tica e´ a visa˜o da matema´tica como uma cieˆncia independente da
realidade f´ısica, uma cieˆncia cujos objetos de estudo sa˜o sistemas abstratos e
auto-consistentes, e que usa a prova como te´cnica principal para determinar a
verdade.
Enta˜o, o que e´ uma prova? Praticamente falando, uma prova e´ qualquer
argumento razoa´vel aceito como tal pelos matema´ticos. Esta definic¸a˜o e´ muito
imprecisa, e na˜o da´ pistas de que tipo de proposic¸o˜es podem ser provadas ou
na˜o. Essa e´ uma das razo˜es para o estudo de lo´gica matema´tica.
5.1 A aritmetizac¸a˜o da Ana´lise
Um segundo ingrediente dos estudos modernos dos fundamentos da matema´tica
e´ o desenvolvimento da Ana´lise e da Teoria da Conjuntos nos se´culos XIX e XX.
Este desenvolvimento teve o efeito de separar aspectos puramente aritme´ticos
ou alge´bricos do nu´mero, dos aspectos geome´tricos.
A´lgebra foi desenvolvida pelas civilizac¸o˜es Indu-A´rabe e Descartes “inven-
tou” a Ana´lise atrave´s da fusa˜o de A´lgebra e Geometria em uma u´nica disci-
plina, a geometria anal´ıtica. Isto permitiu que os matema´ticos “vissem” func¸o˜es
atrave´s de seus gra´ficos. Um nu´mero real passou a ser considerado como um
continuum que era ao mesmo tempo geome´trico e alge´brico, e provas de fatos
relacionados a func¸o˜es eram feitas atrave´s da ana´lise de seus gra´ficos. Desta
forma, uma func¸a˜o nunca era separada da curva que era a sua contrapartida
geome´trica.
A aritmetizac¸a˜o da Ana´lise (Dedekind, Weierstrass, Cauchy, Cantor, etc) foi
responsa´vel pelo desenvolvimento de uma noc¸a˜o alge´brica de nu´mero real que
na˜o apelava para a intuic¸a˜o geome´trica. A definic¸a˜o de nu´meros reais partia dos
nu´meros racionais. Os racionais eram, por sua vez, definidos a partir de razo˜es
de inteiros e os inteiros eram facilmente constru´ıdos a partir dos naturais.
14
Apo´s a aritmetizac¸a˜o da Ana´lise, veio a generalizac¸a˜o da Geometria, criando
a Topologia, que hoje e´ uma disciplina independente. As duas possuem uma
intersec¸a˜o quando se fala de espac¸os me´tricos.
Neste ponto, ficou claro que a fundamentac¸a˜o matema´tica necessa´ria para
suportar esse boom de novas teorias e a´reas da matema´tica deveria ir muito
ale´m de reduzir tudo aos nu´meros naturais. De fato, eram necessa´rios: os
naturais e mais uma se´rie de argumentac¸o˜es baseadas em teoria de conjuntos.
O problema e´ que a teoria de conjuntos usada na e´poca era extremamente
ingeˆnua, e o aparecimento de contradic¸o˜es lo´gicas (ou paradoxos) estremeceu a
base da argumentac¸a˜o matema´tica.
Alguma coisa tinha que ser feita, e foi da´ı que surgiram os primeiros esforc¸os
de axiomatizar a teoria de conjuntos. Esse assunto foi definitivamente encerrado
na primeira de´cada do se´culo XX, quando Zermelo publicou o seu trabalho, logo
complementado por Fraenkel. Surge enta˜o a teoria de conjuntos de Zermelo-
Fraenkel, que sera´ o objeto de estudo da Sec¸a˜o 7.
5.2 Crite´rios para a fundamentac¸a˜o
Nesta sec¸a˜o estabeleceremos alguns crite´rios que devem ser seguidos na hora de
decidir o que e´ uma fundac¸a˜o (ou fundamentac¸a˜o) paraa matema´tica.
1. Uma fundac¸a˜o para a matema´tica deve ser adequada para argumentar
sobre uma porc¸a˜o grande da matema´tica.
De acordo com o Teorema de incompletude de Go¨del (veja Sec¸a˜o 8.2), na˜o
existe uma fundac¸a˜o que seja consistente e completa, ou seja, que seja
adequada para toda a matema´tica. Sempre va˜o existir alguns teoremas
va´lidos que na˜o podera˜o ser obtidos puramente atrave´s de um processo
formal de argumentac¸a˜o. Basta enta˜o decidir quais verdades sa˜o mais
importantes, de maneira a se minimizar as perdas.
2. Uma fundac¸a˜o deve derivar de alguns princ´ıpios intuitivos e naturais.
Um sistema axioma´tico e´ o meio mais comum de catalogar um conjunto
de “verdades” e, em geral, esse sistema e´ baseado em intuic¸a˜o.
3. Os princ´ıpios ba´sicos e noc¸o˜es primitivas (na˜o definidas) devem ser ta˜o
econoˆmicas quanto poss´ıvel.
4. A fundac¸a˜o deve ser consistente.
A na˜o consisteˆncia tem uma consequ¨eˆncia desastrosa: as regras da lo´gica
de primeira ordem podem ser usadas para provar que qualquer afirmativa
e´ um teorema (ou seja, e´ sempre verdadeira). Desta forma, o sistema
resultante e´ trivial e portanto inu´til.
5. A fundac¸a˜o deve poder ser expressa como um sistema formal.
E´ claro que uma fundac¸a˜o para a matema´tica poderia ser proposta de
modo a na˜o poder ser expressa atrave´s de um sistema formal. De fato,
os resultados de Go¨del a respeito da incompletude de sistemas formais
colaboraria para que essa fosse a soluc¸a˜o mais adequada. Entretanto,
na˜o haver um sistema formal implica sempre em se desenvolver discursos
quase-filoso´ficos e obscuros, onde a impera a auseˆncia de uniformidade e
clareza.
15
6. A construc¸a˜o da matema´tica do dia-a-dia no sistema adotado deve ser
natural e ordenada.
6 Sistema de Frege
No comec¸o de sua carreira, Georg Cantor investigou conjuntos de pontos de des-
continuidade em func¸o˜es que admitiam representac¸o˜es de Fourier. Ele tambe´m
apresentou uma construc¸a˜o dos nu´meros reais a partir dos racionais, e mostrou
que existe muito mais reais que racionais. Cantor seguia uma noc¸a˜o de conjun-
tos abstratos, trabalhando com hierarquias tais como o “conjunto de todos os
subconjuntos”.
Mas o que vem a ser um conjunto abstrato? Em alguns textos matema´ticos
muito, mas muito antigos, um conjunto e´ definido como sendo uma aglomerac¸a˜o
de elementos, que se juntam de maneira arbitra´ria e veˆm de fontes independen-
tes. Mas essa definic¸a˜o, ale´m de ser muito doida, entra em conflito direto com
a pra´tica matema´tica, que busca sempre a descric¸a˜o formal e precisa dos entes
a serem definidos, e possui pouca aplicac¸a˜o pra´tica tambe´m em filosofia.
6.1 Ide´ias ba´sicas
Comec¸ando em 1879, Gottlob Frege [8] definiu conjuntos atrave´s da compre-
ensa˜o de predicados, onde qualquer predicado (ou propriedade) pudesse ser
usado para definir um conjunto.
Se pensarmos em um conjunto como uma colec¸a˜o de objetos, enta˜o existem
basicamente duas maneiras diferentes de descrever conjuntos:
(1) exibindo cada um de seus objetos;
(2) apresentando uma propriedade que seja uma condic¸a˜o necessa´ria e sufici-
ente para pertineˆncia ao conjunto.
Para conjuntos finitos, podemos utilizar tanto (1) quanto (2). De fato, o
conjunto A = {a1, . . . , an} e´ determinado pela propriedade
x1 = a1 ∨ . . . ∨ xn = an
Para conjuntos infinitos, (1) e´ claramente imposs´ıvel. A pergunta que surge
enta˜o e´: quando dois conjuntos sa˜o iguais?
A condic¸a˜o mais aceita e intuitivamente correta e´ que dois conjuntos sa˜o
iguais se e somente se eles possuem os mesmos elementos. Mas, apesar de
intuitiva, essa afirmativa e´ altamente na˜o trivial pois as propriedades usadas
na descric¸a˜o de dois conjuntos com elementos iguais podem ser diferentes. Por
exemplo, o conjunto de todos os inteiros irracionais e o conjunto das pessoas
imortais e´ igual. Dois conjuntos com os mesmos elementos sa˜o ditos serem
co-estensivos.
Se aceitarmos a condic¸a˜o descrita anteriormente para igualdade de conjuntos,
enta˜o essa relac¸a˜o entre conjuntos deve satisfazer todas as propriedades de uma
relac¸a˜o de igualdade. A reflexividade vale obviamente, pois todo conjunto possui
os mesmos elementos que si mesmo. A outra condic¸a˜o ba´sica da igualdade e´
que dois conjuntos iguais devem possuir as mesmas propriedades:
A = B ⇒ P (A) ≡ P (B)
16
Esta condic¸a˜o na˜o pode ser deduzida a partir da noc¸a˜o de co-extenc¸a˜o. Ou seja,
se desejamos que co-extensa˜o caracterize a identidade entre conjuntos, enta˜o essa
condic¸a˜o (ou princ´ıpio) deve ser posta como axioma. Esse princ´ıpio e´ conhecido
como o princ´ıpio ou axioma da extensionalidade.
Observamos que o princ´ıpio da extensionalidade pode parecer o´bvio, mas e´
poss´ıvel formular uma teoria de conjuntos coerente em que tal princ´ıpio na˜o
vale.
Uma vez que acreditamos no princ´ıpio da extensionalidade, surge uma outra
questa˜o: toda propriedade define um conjunto? Ou seja, dada uma propriedade
P , existe um conjunto definido exatamente por aqueles objetos que satisfazem a
condic¸a˜o P? A tese de que toda propriedade ou condic¸a˜o define um conjunto e´
conhecida como princ´ıpio da abstrac¸a˜o (o conjunto e´ abstra´ıdo da propriedade
que o define). Formalmente:
∀P.∃A.∀x.(x ∈ A ≡ P (x))
Frege e Dedekind provaram, utilizando uma se´rie de construc¸o˜es engenhosas,
que toda a matema´tica ba´sica podia ser descrita usando apenas lo´gica de pri-
meira ordem mais os dois princ´ıpios: extensionalidade e abstrac¸a˜o. Ou seja, se
considerarmos a l.p.o. (com “∈” como o u´nico predicado primitivo) mais os axi-
omas citados acima enta˜o e´ poss´ıvel, por meio de construc¸o˜es e definic¸o˜es dentro
do sistema, definir os nu´meros naturais, os reais, e reproduzir formalmente as
provas usuais dos teoremas conhecidos sobre tais conjuntos e seus elementos.
6.2 O sistema formal
A linguagem F definida por Frege conte´m apenas um predicado, que escrevere-
mos como ∈. As fo´mulas de F sa˜o definidas abaixo.
1. Toda varia´vel e´ um termo.
2. Se x, y sa˜o termos, enta˜o x ∈ y e´ uma fo´rmula.
3. Se A e´ uma fo´rmula e x e´ uma varia´vel, enta˜o ∀x.A e ∃x.A sa˜o fo´rmulas.
4. Se A e´ uma fo´rmula contendo x como varia´vel livre, enta˜o {x | A} e´ um
termo.
5. Se A,B sa˜o fo´rmulas, enta˜o ¬A,A ∨B sa˜o fo´rmulas.
6. As fo´rmulas e termos de F sa˜o exatamente as definidas pelas regras acima.
A primeira definic¸a˜o de F e´ a de igualdade:
Definic¸a˜o 4 Escrevemos (x = y) para
∀z.z ∈ x ≡ z ∈ y
onde a varia´vel z na˜o ocorre livre em x ou y.
Os axiomas de extensionalidade e abstrac¸a˜o sa˜o os u´nicos axiomas de F :
F1. ∀x.∀y.(x = y) ⇒ A(x, x) ≡ A(x, y) onde A(x, y) e´ obtido de A(x, x)
substituindo x por y zero, uma ou mais ocorreˆncias de x em A(x, x) e y e´
livre em x em todas as ocorreˆncias de x por ele substitu´ıdas.
17
F2. ∀x.x ∈ {y | A(y)} ≡ A(x) onde A(y) conte´m y livre, x e´ livre em y em
A(y) e A(x) e´ obtido de A(y) substituindo y por x em todas as ocorreˆncias
livres de y em A(y).
Segue imediatamente que se ⊢ A(x) ≡ B(x) enta˜o ⊢ {x | A(x)} = {x |
B(x)}.
A seguir, apresentaremos algumas definic¸o˜es e teoremas em F .
Teorema 5 ⊢ ∀x.x = x
Prova Considere a seguinte derivac¸a˜o:
⊢ x2 ∈ x1 ≡ x2 ∈ x1 (inicial)
⊢ ∀x2.x2 ∈ x1 ≡ x2 ∈ x1 (∀I)
Pela Definic¸a˜o 4, obtemos ⊢ x1 = x1. Logo,
⊢ x1 = x1 (inicial)
⊢ ∀x1.x1 = x1 (∀I)
como quer´ıamos.
Definic¸a˜o 5 V denota {x | x = x}
Teorema 6 ⊢ ∀x.x ∈ V
Ou seja, V e´, na verdade, o conjunto universal contendo tudo. Em particular,
V conte´m ele mesmo.
Definic¸a˜o 6 ∅ denota {x | x 6= x}
Teorema 7 ⊢ ∀x.x /∈ ∅
∅ e´ o conjunto vazio, um conjunto que na˜o conte´m elementos. Poder´ıamos
seguir adiante e definir unia˜o, intersec¸a˜o e complementar de conjuntos. Veja a
refereˆncia 5 para a lista completa de definic¸o˜es.
O mais impressionante dessa teoria, e´ que podemos definiro conjunto dos
naturais com apenas o que foi descrito ate´ agora. A seguir, as definic¸o˜es de zero,
sucessor e do conjunto dos naturais.
Definic¸a˜o 7 0 denota {∅}
Definic¸a˜o 8 S(x) denota {y | ∃z.z ∈ y ∧ (y ∩ z) ∈ x}
Definic¸a˜o 9 N denota {x1 | ∀x2.(0 ∈ x2) ∧ ((∀x3.x3 ∈ x2 ⇒ S(x3) ∈ x2) ⇒
x1 ∈ x2)}
Um conjunto e´ dito indutivo se conte´m o sucessor de todos os seus elementos.
N e´ o menor conjunto indutivo contendo o 0.
Com as definic¸o˜es acima, podemos provar alguns teoremas sobre o conjunto
N .
Teorema 8 ⊢ 0 ∈ N
18
Ou seja, 0 e´ um nu´mero natural. Tambe´m, 0 na˜o e´ o sucessor de nenhum
nu´mero natural:
Teorema 9 ⊢ ∀x.0 6= S(x)
O sucessor de um natural tambe´m e´ natural:
Teorema 10 ⊢ ∀x.x ∈ N ⇒ S(x) ∈ N
Teorema 11 ⊢ ∀x1.(0 ∈ x1 ∧ ∀x2.x2 ∈ x1 ⇒ S(x2) ∈ x1)⇒ (N ⊂ x1)
O teorema acima diz que N esta´ contido em qualquer conjunto contendo o
zero e o sucessor de cada um de seus elementos, e permite enunciar a induc¸a˜o
matema´tica:
Teorema 12 ⊢ (P (0) ∧ ∀x.P (x)⇒ P (S(x)))⇒ ∀x.(x ∈ N ⇒ P (x))
Algumas observac¸o˜es importantes sobre o que foi discutido acima:
• Os cinco postulados de Peano (formalizac¸a˜o da aritme´tica) podem ser
provados a partir do sistema de Frege.
• As operac¸o˜es de adic¸a˜o, multiplicac¸a˜o, etc, podem ser definidas utilizando
a recursa˜o:
x+ 0 = x
x+ S(y) = S(x+ y)
Claro que o segundo ı´tem depende do Teorema da recursa˜o primitiva: dadas
as func¸o˜es g(x1, . . . , xn) e h(x1, . . . , xn, y, z), existe uma func¸a˜o f(x1, . . . , xn, xn+1)
tal que f(x1, . . . , xn, 0) = g(x1, . . . , xn) e f(x1, . . . , xn, S(y)) = h(x1, . . . , xn, y, f(x1, . . . , xn, y)).
Tal teorema pode ser provado por induc¸a˜o, tambe´m dentro do sistema de Frege.
Mas na˜o pode ser provado apenas a partir dos axiomas de Peano.
O sistema de Frege e´ certamente via´vel e satisfaz claramente 5 dos crite´rios
estabelecidos anteriormente para uma boa fundamentac¸a˜o da matema´tica. As
construc¸o˜es sa˜o naturais e intuitivas e os axiomas na˜o fazem nada a mais que
expressar formalmente algumas caracter´ısticas que parecem ba´sicas e essenciais
em teoria de conjuntos.
Mas falta o mais importante: a consisteˆncia!
Teorema 13 ⊢ {x | x /∈ x} /∈ {x | x /∈ x}
Teorema 14 ⊢ {x | x /∈ x} ∈ {x | x /∈ x}
Se toda condic¸a˜o determina um conjunto, enta˜o considere o conjunto y de-
terminado pela condic¸a˜o x /∈ x. Ou seja, y e´ o conjunto de todos os conjuntos
que na˜o sa˜o elementos de si mesmos.
A princ´ıpio, y e´ um conjunto grande, uma vez que a maioria dos conjuntos
na˜o e´ membro de si mesmo. Por exemplo, o conjunto dos reais na˜o e´ um nu´mero
real. O paradoxo consiste no fato de que y e´ um elemento de si mesmo se e
somente se na˜o o e´. Mais sobre o Paradoxo de Russell na Sec¸a˜o 6.3.
Sendo o Sistema de Frege inconsistente, qualquer coisa pode ser provada
dentro dele e, portanto, ele na˜o poder ser usado como uma fundac¸a˜o para a
matema´tica.
19
Mas, apesar de ser inconsistente, nem tudo o que foi desenvolvido por Frege
era errado. Por exemplo, a construc¸a˜o dos conjuntos nume´ricos e´ consistente.
O erro consistiu em considerar o princ´ıpio da abstrac¸a˜o de uma maneira geral.
Enta˜o a pergunta que surge e´: e´ poss´ıvel propor um sistema baseado nas
ide´ias de Frege que na˜o seja contradito´rio? Veja a resposta na Sec¸a˜o 7.
6.3 Paradoxos e a teoria de tipos de Russell
Em 1903, Bertrand Russell publicou Principles of Mathematics, onde ele afirma
que matema´tica e lo´gica sa˜o ideˆnticas. Em suas palavras:
“Pure mathematics is the class of all propositions of the form p implies q
where p and q are propositions ... and neither p nor q contains any constants
except logical constants.”
No seu trabalho posterior Principia Mathematica, escrito entre 1910 e 1913
em colaborac¸a˜o com Alfred North Whitehead (1861-1947), Russell propo˜e um
sistema que pensa ser completo para matema´tica pura, baseado exclusivamente
em princ´ıpios lo´gicos puros, e formulado utilizando uma linguagem simbo´lica
precisa.
A preocupac¸a˜o principal do Principia Mathematica era evitar os ta˜o famosos
paradoxos circulares viciosos, tais como o paradoxo de Russell. O paradoxo de
Russell comec¸a com o questionamento se um conjunto qualquer e´ um membro
de si mesmo ou na˜o.
Por exemplo, o conjunto de todos os gatos na˜o e´ membro de si mesmo, por
na˜o ser um gato. Mais interessante, considere R a colec¸a˜o contendo apenas os
conjuntos que na˜o sa˜o membros de si mesmos. A pergunta que surge e´: R e´
um conjunto ou na˜o? Suponha que sim. Enta˜o existem duas possibilidades: ou
R ∈ R, ou R /∈ R. No primeiro caso, R deve satisfazer a condic¸a˜o de pertineˆncia
a R, ou seja, R na˜o deve ser um membro de si mesmo, o que e´ um absurdo.
Conversamente, suponha que R na˜o seja um elemento de si mesmo. Enta˜o R
na˜o satisfaz a condic¸a˜o de pertineˆncia a R. Ou seja, R deve ser um elemento de
si mesmo. De qualquer modo, chegamos a uma posic¸a˜o contradito´ria, onde R e´
um membro de si mesmo precisamente quando na˜o o e´. Observe que o fato de
R ser finito ou infinito e´ irrelevante.
O mesmo paradoxo aparece em diversas outras situac¸o˜es, como por exemplo
o cla´ssico: a bibliografia de todas as bibliografias. A esse tipo de “conjunto de
todos os conjuntos” chamamos usualmente de colec¸a˜o.
Examinando de perto o paradoxo de Russell, vemos que R e´ definido atrave´s
de uma refereˆncia impl´ıcita a si mesmo, e portando gerando um c´ırculo vicioso.
A soluc¸a˜o apresentada por Russell para esse tipo de problema com auto-
refereˆncia foi a de excluir todas as colec¸o˜es cuja definic¸a˜o fazia refereˆncia a`
pro´pria colec¸a˜o. Ou seja, ele sugeriu uma teoria de tipos ou n´ıveis, onde a` toda
classe (conjunto, colec¸a˜o) corresponde um tipo e uma classe pode conter apenas
elementos de menor tipo. Com essa restric¸a˜o, classes devem possuir tipo maior
que o tipo de cada um de seus membros, evitando paradoxos como o de Russell.
A teoria desenvolvida por Russell foi chamada de teoria ramificada de tipos,
e consiste na espinha dorsal do Principia Mathematica. Enquanto a teoria
ramificada de tipos exclui a possibilidade de paradoxos, e´ um sistema muito
fraco para sevir como ferramenta lo´gica para a matema´tica. De fato, na˜o se
pode nem ao menos provar que existe uma infinidade de nu´meros naturais, ou
20
mesmo que cada nu´mero natural possui um sucessor diverso. Desta forma, a
tentativa de Russell de reduzir a matema´tica a` lo´gica foi um fracasso.
7 Teoria de conjuntos de Zermelo-Fraenkel
A partir dos trabalhos de Frege e Russell, se tornava evidente que um maior
esforc¸o deveria ser feito no sentido de formalizar (ou axiomatizar) a teoria de
conjuntos.
Isso foi feito com sucesso por Ernst Zermelo. Suas razo˜es para fazeˆ-lo foram
duas. Primeiro, a descoberta do paradoxo de Russell. Como ja´ observado anteri-
ormente, a soluc¸a˜o proposta pro Russell em sua teoria de tipos na˜o e´ satisfato´ria.
Mas Zermelo observou que o paradoxo de Russell pode ser evitado atrave´s de
uma escolha cuidadosa dos princ´ıpios de construc¸a˜o de conjuntos, obtendo ainda
o poder de expressa˜o necessa´rio para a argumentac¸a˜o matema´tica.
O prec¸o que se deve pagar para evitar inconsisteˆncia e´ apenas que alguns
“conjuntos” na˜o existem, como por exemplo o conjunto “universal” (conjunto
de todos os conjuntos), ou o conjunto de todos os nu´meros cardinais.
A segunda raza˜o e´ um pouco mais delicada. No desenvolvimento da teoria
de nu´meros cardinais e ordinais de Cantor, surgiu a questa˜o de qual tipo de
conjunto pode ser ordenado. De fato, Zermelo provou que todo conjunto satisfaz
o princ´ıpio da boa ordenac¸a˜o, mas pode fazer isso apenas depois de introduzir
um novo axioma que parecia ser independente dos outros (como realmente o e´).
O seu axioma da escolha se tornou a ferramenta padra˜o da matema´tica
moderna, e a discussa˜o que surgiu em torno desseaxioma se compara a` de
outro axioma famoso, o quinto postulado de Euclides. Mais sobre o axioma da
escolha na Sec¸a˜o 7.3. A teoria axioma´tica de conjuntos que utilizamos hoje em
dia (ZF) e´ baseada na proposic¸a˜o original de Zermelo, depois melhorada por
Fraenkel em 1922.
7.1 Ide´ias ba´sicas
Respondendo a` pergunta feita no final da Sec¸a˜o 6, Zermelo evitou os paradoxos e
inconsisteˆncias no sistema de Frege baseando-se na ide´ia de que conjuntos podem
ser constru´ıdos a partir de alguns conjuntos simples e algumas operac¸o˜es.
Com relac¸a˜o ao princ´ıpio da abstrac¸a˜o: quando conjuntos sa˜o definidos
por propriedades, eles sa˜o usualmente subconjuntos de um dado conjunto ma-
tema´tico. Por exemplo, um matema´tico trabalha com o conjunto de todas as
func¸o˜es reais cont´ınuas quando define a noc¸a˜o “f e´ cont´ınua” em termos lo´gicos
puros. Mas este e´ um subconjunto do conjunto de todas as func¸o˜es reais, que
os matema´ticos consideram um objeto matema´tico va´lido. Mas certamente na˜o
ocorreria a um matema´tico considerar o conjunto de todas as func¸o˜es (ou equi-
valentemente o conjunto de todos os conjuntos). A raza˜o e´ simples: na˜o tem
sentido em se falar do conjunto de todas as func¸o˜es, uma vez que cada func¸a˜o
e´ determinada por um domı´nio, uma regra matema´tica, um co-domı´nio e assim
por diante.
Portanto, no sistema de Zermelo, o princ´ıpio da abstrac¸a˜o se torna o princ´ıpio
da separac¸a˜o. Basicamente, esse princ´ıpio determina um processo de obter sub-
conjuntos a partir de um conjunto dado atrave´s de propriedades, ao inve´s de
defini-los a priori pelas propriedades.
21
O princ´ıpio da separac¸a˜o pode ser definido de maneira intuitiva:
Para cada condic¸a˜o P (que possa ser expressa por uma fo´rmula lo´gica
na nossa teoria formal) e para cada conjunto y dado, o conjunto de
todos os elementos de y que satisfazem a propriedade P existe.
Utilizando a notac¸a˜o lo´gica:
⊢ ∀y.∃x.∀z.(z ∈ x) ≡ (z ∈ y) ∧ P (z)
Ou seja, ao inve´s de propor a existeˆncia de conjuntos, o princ´ıpio da se-
parac¸a˜o fala sobre a existeˆncia de subconjuntos de um dado conjunto.
O u´nico conjunto cuja existeˆncia pode ser provada a partir do princ´ıpio da
separac¸a˜o e´ o conjunto vazio. Basta tomar qualquer propriedade auto contra-
dito´ria para P . Por exemplo:
⊢ ∃x1.∀x2.(x2 ∈ x1) ≡ (x2 ∈ x3) ∧ ((x2 ∈ x2) ∧ (x2 /∈ x2))
o que implica
⊢ ∃x1.∀x2.(x2 /∈ x1)
Observe que nenhuma fo´rmula lo´gica P da´ origem ao conjunto universal.
Com o princ´ıpio da separac¸a˜o podemos apenas construir o conjunto vazio.
Todos os outros conjuntos devem ser subconjuntos de conjuntos dados. Enta˜o
devemos determinar quais sa˜o esses conjuntos. Basicamente, conjuntos va´lidos
sa˜o constru´ıdos atrave´s do conjunto vazio e operac¸o˜es ba´sicas como power set e
unia˜o. Temos necessidade de outros postulados (ou axiomas) para garantir essas
operac¸o˜es. Esses axiomas adicionais, juntamente com o princ´ıpio da separac¸a˜o,
constituem o sistema de Zermelo-Fraenkel (ZF).
7.2 Formalizac¸a˜o de ZF
A grama´tica de termos e fo´rmulas de ZF e´ basicamente a mesma descrita
anteriormente para o sistema de Frege, exceto pela introduc¸a˜o de termos que
sa˜o operadores primitivos, que sera˜o apresentados ao longo do texto.
A primeira definic¸a˜o de ZF e´ a de igualdade, igual a` definic¸a˜o de Frege:
Definic¸a˜o 10 Escrevemos (x = y) para
∀z.z ∈ x ≡ z ∈ y
onde x e y sa˜o quaisquer termos nos quais a varia´vel z na˜o ocorre livre.
O axioma de extensionalidade de ZF :
ZF1. ∀x.∀y.(x = y) ⇒ A(x, x) ≡ A(x, y) onde A(x, y) e´ obtido de A(x, x)
substituindo x por y zero, uma ou mais ocorreˆncias de x em A(x, x) e y e´
livre em x em todas as ocorreˆncias de x por ele substitu´ıdas.
Teorema 15 ⊢ ∀x1.∀x2.((x1 = x2)⇒ ∀x3.(x1 ∈ x3) ≡ (x2 ∈ x3))
22
Prova Considere a deduc¸a˜o abaixo:
x1 = x2 ⊢ (x1 ∈ x3) ≡ (x2 ∈ x3)
x1 = x2 ⊢ ∀x3.(x1 ∈ x3) ≡ (x2 ∈ x3) (∀I)
⊢ (x1 = x2)⇒ ∀x3.(x1 ∈ x3) ≡ (x2 ∈ x3) (⇒ I)
⊢ ∀x1.∀x2.((x1 = x2)⇒ ∀x3.(x1 ∈ x3) ≡ (x2 ∈ x3)) (∀I)
Pelo axioma ZF1 com x = x1, y = x2 e A(x, x) = ∀x3.x ∈ x3 ≡ x ∈ x3:
⊢ (x1 = x2)⇒ ∀x3.(((x1 ∈ x3) ≡ (x1 ∈ x3)) ≡ ((x1 ∈ x3) ≡ (x2 ∈ x3)))
Logo,
(x1 = x2) ⊢ (((x1 ∈ x3) ≡ (x1 ∈ x3)) ≡ ((x1 ∈ x3) ≡ (x2 ∈ x3))) (x1 = x2) ⊢ (x1 ∈ x3) ≡ (x1 ∈ x3)
x1 = x2 ⊢ (x1 ∈ x3) ≡ (x2 ∈ x3)
O axioma da separac¸a˜o e´ formalmente enunciado como:
ZF2. ∀x.∀y.(x ∈ {y | (y ∈ z) ∧A(y)}) ≡ (x ∈ z) ∧A(x).
A diferenc¸a entre o princ´ıpio da separac¸a˜o e o princ´ıpio da abstrac¸a˜o de
Frege e´ a condic¸a˜o extra y ∈ z.
O axioma a seguir que diz que 0 e´ o conjunto vazio:
ZF3. 0 = {x1 | x1 ∈ 0 ∧ x1 6= x1}, onde 0 e´ uma constante primitiva.
Como ja´ observamos antes, a existeˆncia do conjunto vazio pode ser deduzida
a partir de ZF2. ZF3 apenas nos diz que 0 e´ o conjunto de nenhum elemento,
como o 0 = ∅ do sistema de Frege.
Teorema 16 ⊢ ∀x.(x = x)
A demonstrac¸a˜o do teorema acima e´ trivial e este resultado pode ser usado para
provar:
Teorema 17 ⊢ ∀x.(x /∈ 0)
Prova Por ZF2, x ∈ 0 = x ∈ 0 ∧ x 6= x. Logo x ∈ 0 ⇒ x 6= x pode ser
provado:
x ∈ 0 ⊢ x ∈ 0 ∧ x 6= x (inicial)
x ∈ 0 ⊢ x 6= x (∧E)
⊢ x ∈ 0⇒ x 6= x (⇒ I)
Utilizando as equivaleˆncias De Morgan, a conclusa˜o da derivac¸a˜o acima e´ equi-
valente a ⊢ x = x⇒ x /∈ 0. Logo,
⊢ x = x⇒ x /∈ 0
⊢ ∀x.x = x
⊢ x = x (∀E)
⊢ x /∈ 0 (⇒ E)
⊢ ∀x.x /∈ 0 (∀I)
Dado que P e´ a representac¸a˜o da func¸a˜o primitiva que indica o “power set”
(P(y) e´ o conjunto de todos os subconjuntos de y), o quarto axioma do sistema
ZF pode ser enunciado assim:
23
ZF4. ∀x.∀y.x ∈ P(y) ≡ (x ⊂ y).
Seja {y, z} a representac¸a˜o da func¸a˜o primitiva que indica o par na˜o ordenado
de y e z, ou o conjunto cujos u´nicos elementos sa˜o y e z.
ZF5. ∀y.∀z.∀x.x ∈ {y, z} ≡ (x = y ∨ x = z).
Seja
⋃
a representac¸a˜o da func¸a˜o primitiva tal que
⋃
(y) indica a unia˜o de
todos os conjuntos na colec¸a˜o y. O pro´ximo axioma e´ conhecido como axioma
da soma de conjuntos.
ZF6. ∀y.∀x.x ∈ ⋃(y) ≡ ∃z.(z ∈ y) ∧ (x ∈ z).
Definic¸a˜o 11 Denotaremos x ∪ y = ⋃({x, y}).
Definic¸a˜o 12 Denotaremos x′ = x ∪ {x}. Em particular, escreveremos 1 =
0′, 2 = 1′. etc.
O operador x′ e´ a func¸a˜o sucessor no sistema de Zermelo. A versa˜o de
nu´meros naturais que obtemos e´ a mesma desevolvida por von Neumann. In-
tuitivamente, os nu´meros naturais formam o menor conjunto contendo o 0 e
fechado com relac¸a˜o a` operac¸a˜o sucessor.
Ao total, sa˜o 10 os axiomas de ZF . Na˜o discutiremos todos os outros aqui,
mas de especial interesse sa˜o aqueles que tratam da existeˆncia do conjunto
infinito e o axioma da escolha, que e´ o assunto da pro´xima sec¸a˜o.
7.3 Axioma da escolha
No livro Introduc¸a˜o a` Filosofia da Matema´tica, Russell relata a para´bola de um
miliona´rio cujo guarda roupa possui um nu´mero enumera´vel (infinito) de pares
de sapatos, assim como de meias. Parece o´bvio que existe uma bijec¸a˜o entre
os sapatos e os nu´meros naturais, e uma bijec¸a˜o entre as meias e os nu´meros
naturais.
Com relac¸a˜o aos sapatos, essa bijec¸a˜o e´ fa´cil de estabelecer: o sapato es-
querdo do n-e´simo par corresponde ao nu´mero 2n, enquanto que o sapato direito
corresponde ao nu´mero 2n+1. E com relac¸a˜o a`s meias? O problema e´ que, em
geral, na˜o se pode distinguir meias de um certo par, como feito com sapatos.
Ou seja, para que o mesmo procedimento funcione nesse caso e´ necessa´rio que
as meias de todos os pares (a menos de um nu´mero finito) sejam diversas. Mas
na˜o somente isso, as meias devem ser diversas mas seguindo um certo crite´rio,
como por exemplo uma e´ azul e a outra preta.
O fato de que na˜o existe um modo sistema´tico de escolher uma meia de um
par significa que precisamos da uma func¸a˜o de escolha, mesmo que na˜o possamos
apresenta´-la explicitamente.
Uma func¸a˜o de escolha em uma famı´lia S de conjuntos e´ uma func¸a˜o f com
domı´nio S tal que, para todo conjunto na˜o vazioX em S, f(X) e´ um elemento
de X . Em outras palavras, f “escolhe” um elemento para cada membro de S.
Se S e´ finito, a existeˆncia da func¸a˜o de escolha em S e´ uma consequeˆncia
trivial dos princ´ıpios ba´sicos de formac¸a˜o de conjuntos e das regras de lo´gica
cla´ssica.
Quando S e´ infinito, entretanto, esses princ´ıpios na˜o sa˜o suficientes e por-
tanto a existeˆncia de uma func¸a˜o de escolha deve ser postulada. A afirmativa
24
que em qualquer famı´lia de conjuntos na˜o vazios (mesmo que sejam infinitos)
existe ao menos uma func¸a˜o de escolha e´ chamado o axioma da escolha. Esse
princ´ıpio foi proposto por Zermelo em 1904.
Formalmente, o axioma da escolha diz o seguinte:
ZF10. ∀x.x 6= 0 ⇒ σ(x) ∈ x onde σ e´ a representac¸a˜o da func¸a˜o primitiva que
indica a func¸a˜o escolha.
σ(x) escolhe exatamente um elemento do conjunto na˜o vazio x. Claramente,
σ escolhe o mesmo elemento para dois conjuntos iguais:
Teorema 18 ⊢ ∀x1.∀x2.(x1 = x2)⇒ σ(x1) = σ(x2)
O cara´ter altamente na˜o construtivo do axioma da escolha provocou uma
grande cr´ıtica inicialmente: ao mesmo tempo que garante a possibilidade de se
fazer um nu´mero arbitrariamente grande de escolhas arbitra´rias, o axioma na˜o
da´ nenhuma indicac¸a˜o de como essas escolhas devem ser feitas.
Em 1938, Go¨del estabeleceu a relativa consisteˆncia do axioma da escolha
com relac¸a˜o a sistemas usuais de teoria de conjuntos e isso, juntamente com a
importaˆncia do axioma da escolha em provas de muitos teoremas matema´ticos
importantes, fez com que o axioma fosse aceito pela maioria da comunidade
acadeˆmica.
A prova de independeˆncia do axioma da escolha (com relac¸a˜o aos demais
axiomas da teoria de conjuntos de Zermelo Fraenkel) foi apresentada em 1964
por P. J. Cohen.
A julgar pelo nu´mero de consequ¨eˆncias matema´ticas, o axioma da escolha e´
sem du´vida o mais fe´rtil princ´ıpio da teoria de conjuntos.
Muitas dessas consequ¨eˆncias sa˜o, na verdade, equivalentes ao teorema da
escolha. As mais famosas sa˜o:
1. Teorema da boa ordenac¸a˜o de Zermelo: todo conjunto pode ser bem or-
denado.
2. Princ´ıpio de tricotomia: em todo par de nu´meros cardinais, um e´ menor
que o outro, ou eles sa˜o iguais.
3. Lema de Kuratowski-Zorn: qualquer conjunto na˜o vazio no qual todo
subconjunto ordenado possui um limite superior, possui um elemento ma-
ximal.
4. Teorema de Tychonov: o produto de qualquer famı´lia de espac¸os to-
polo´gicos compactos e´ compacto.
5. Teorema de Hamel-Banach: todo espac¸o vetorial possui uma base.
Como observado anteriormente, o cara´ter na˜o construtivo do axioma da
escolha foi notado desde quando foi proposto. Entretanto, a questa˜o de qual e´
o seu “status” lo´gico continuou sem soluc¸a˜o por um bom tempo. Finalmente,
em 1975, Diaconescu mostrou que o axioma da escolha implica o princ´ıpio do
meio exclu´ıdo (veja Teorema 19 abaixo). Esse resultado e´ extraordina´rio per
se, apesar de na˜o ser de todo surpreendente. De fato, isso basta para entender
porque os me´todos de prova em matema´tica sa˜o baseados em lo´gica cla´ssica,
como a demonstrac¸a˜o por absurdo por exemplo.
A seguir, uma prova fa´cil de que o axioma da escolha implica o princ´ıpio do
meio exclu´ıdo.
25
Teorema 19 Considere a seguinte formulac¸a˜o do axioma da escolha:
ZF10′ : Se S e´ um subconjunto do produto cartesiano A × B e, para cada
x ∈ A existe y ∈ B tal que (x, y) ∈ S, enta˜o existe uma func¸a˜o f : A → B tal
que (x, f(x)) ∈ S para cada x ∈ A.
Enta˜o vale o princ´ıpio do meio exclu´ıdo: ⊢ p ∨ ¬p.
Prova Seja A = {s, t}, onde s = t se e somente ⊢ p, onde p e´ um predicado
qualquer. Seja B = {0, 1} e seja S = {(s, 0), (t, 1)} ⊂ A×B. Se f : A→ B e´ a
func¸a˜o de escolha para S, enta˜o
(I) f(s) = 1 ou f(t) = 0, enta˜o devemos ter s = t e, portanto p vale; ou
(II) f(s) = 0 e f(t) = 1, e portanto s na˜o pode ser igual a t e p na˜o vale.
Finalmente, um comenta´rio rapidinho sobre as consequ¨eˆncias “paradoxais”
do axioma da escolha. Em 1914, Hausdorff provou, utilizando o axioma da
escolha, que 2/3 da superf´ıcie da esfera e´ congruente a 1/3 dela. Esse resul-
tado foi mais tarde estendido para o caso tri-dimensional por Banach e Tarski
em 1924, onde eles utilizaram o axioma da escolha para provar que qualquer
esfera so´lida pode ser decomposta em um nu´mero finito de subconjuntos, que
podem ser re-arranjados de tal modo a formar duas esferas so´lidas, cada uma
do mesmo tamanho da original. Esse resultado e´ conhecido como o paradoxo
de Banach-Tarski. Por mais estranhos que esses resultados possam parecer,
eles na˜o constituem, verdadeiramente, contradic¸o˜es. Decomposic¸o˜es “parado-
xas” como essas so´ se tornam poss´ıveis em teoria de conjuntos porque objetos
geome´tricos cont´ınuos foram considerados como um conjunto discreto de pon-
tos, que o axioma da escolha enta˜o permite ser rearranjado em uma maneira
arbitra´ria.
8 O programa de Hilbert e a incompletude de
Go¨del
Nesta sec¸a˜o comec¸aremos a discutir algumas questo˜es ba´sicas que dizem respeito
a` relac¸a˜o entre provas dentro de uma certa linguagem formal e a argumentac¸a˜o
meta-matema´tica sobre as provas dentro da linguagem.
O problema ba´sico a ser abordado e´ o seguinte: dado um sistema lo´gico
formal, como podemos provar que tal sistema e´ consistente?
Para provar a inconsisteˆncia, basta exibir uma deduc¸a˜o de uma contradic¸a˜o,
como foi feito no caso do sistema de Frege.
Para provar a consisteˆncia, devemos provar que e´ imposs´ıvel que qualquer
contradic¸a˜o possa ser um teorema do sistema. Existem basicamente dois me´todos
para fazer isso. O primeiro e´ mostrar que o sistema formal e´, na verdade, uma
estrutura matema´tica. Atrave´s de uma exaustiva ana´lise do processo de prova
dentro do sistema (visto como uma operac¸a˜o matema´tica) pode-se mostrar que
contradic¸o˜es na˜o esta˜o presentes no sistema. Este me´todo e´ conhecido como
proof theory.
O segundo me´todo utiliza o fato de que qualquer sistema que possui um
modelo (matema´tico) e´ consistente. Essa abordagem e´ conhecida como model
theory.
26
Em qualquer um dos dois me´todos, para provar consisteˆncia devemos utilizar
a matema´tica. Como a matema´tica na˜o foi provada consistente, existe a´ı uma
circularidade.
Uma maneira de evitar este dilema e´ restringir as ferramentas matema´ticas
utilizadas para prova de consisteˆncia. Por exemplo, utilizar apenas o que pode
ser desenvolvido atrave´s de me´todos matema´ticos construtivos. Um exemplo e´
a prova de consisteˆncia da lo´gica de primeira ordem.
Para a discussa˜o que se segue, precisaremos da linguagem S da aritme´tica
de primeira ordem.
S e´ uma teoria de primeira ordem com um predicado bina´rio primitivo “=”,
duas func¸o˜es bina´rias primitivas “+” e “•”, uma func¸a˜o una´ria “′” e uma cons-
tante primitiva “0”. Intuitivamente, tais entes primitivos representam a relac¸a˜o
de igualdade, as operac¸o˜es de adic¸a˜o, multiplicac¸a˜o e sucessor nos naturais, e
zero, respectivamente. Os axiomas de S consistem daqueles para igualdade (ver
Hatcher pa´gina 70), os axiomas de Peano para o 0 e ′, e as definic¸o˜es recursivas
para a adic¸a˜o e multiplicac¸a˜o:
x+ 0 = x ∧ x+ y′ = (x+ y)′
x • 0 = 0 ∧ x • y′ = x • y + x
Observe que esta linguagem e´ bem mais fraca que uma baseada em teoria de
conjuntos, uma vez que todos os axiomas de S sa˜o teoremas dentro da teoria de
conjuntos ZF .
Os teoremas de aritme´tica que podem ser provados dentro de S sa˜o ditos
elementares.
Observe que para provar a consisteˆncia de S devemos utilizar a aritme´tica.
Ou seja, devemos assumir que S e´ consistente e pronto! Tambe´m porque a
teoria de nu´meros e´ uma parte ba´sica da matema´tica, enta˜o S ser inconsistente
desmorona toda a matema´tica que conhecemos.
8.1 O programa de Hilbert
Em 1899 David Hilbert publicou o seu trabalho Grundlagen der Geometrie
(Fundamentos da Geometria), quemarcou e´poca. Sem introduzir nenhum sim-
bolismo especial, nesse trabalho Hilbert formula um tratamento axioma´tico ri-
goroso da geometria euclideana.
Ele tambe´m estabelece a consisteˆncia do seu sistema axioma´tico mostrando
que ele pode ser interpretado em um sistema de nu´meros reais. Com esse sis-
tema, Hilbert procurava mostrar que a geometria era inteiramente auto sufici-
ente como um sistema dedutivo.
O grande sucesso que Hilbert obteve com esse trabalho o levou a tentar apli-
car o mesmo me´todo a` matema´tica pura como um todo, deste modo assegurando
o que ele esperava ser o rigor perfeito de toda matema´tica.
Hilbert foi o primeiro a formular o conceito de meta-matema´tica, por meio
da qual ele pretendia estudar sistemas formais atrave´s de me´todos concretos
(construtivos) de teoria de nu´meros. O objetivo era apresentar uma prova de
consisteˆncia de um sistema no qual toda a matema´tica poderia ser deduzida.
O programa de Hilbert (1920) tinha como objetivo prover uma nova fundac¸a˜o
para a matema´tica, na˜o reduzindo-a a` lo´gica, mas representando a sua forma
essencial dentro de s´ımbolos concretos. Desta forma, proposic¸o˜es matema´ticas
27
que se referiam apenas a objetos concretos foram chamados reais, ou concre-
tos, enquanto que outras proposic¸o˜es matema´ticas eram consideradas ideais ou
abstratas.
Enta˜o, por exemplo, 2+2=4 seria considerado como uma proposic¸a˜o real,
enquanto que “existe um nu´mero ı´mpar perfeito” seria visto como ideal. Na
verdade, proposic¸o˜es ideais eram pensadas como pontos no infinito da geometria
projetiva.
As ambic¸o˜es propostas no programa de Hilbert foram derrubadas mais tarde
por Go¨del, que provou, atrave´s do seus famosos teoremas de incompletude, que
existem sempre proposic¸o˜es reais prova´veis atrave´s de me´todos ideais que na˜o
podem ser provadas por me´todos concretos. Ou seja, o programa de Hilbert
para estabelecer a consisteˆncia da matema´tica se mostrou irrealiza´vel.
8.2 Teoremas de incompletude de Go¨del
No princ´ıpio do se´culo XX, Go¨del acabou com qualquer esperanc¸a de encontrar
uma base axioma´tica para a matema´tica que fosse ao mesmo tempo completa e
livre de contradic¸o˜es.
De uma maneira concisa, o teorema da incompletude de Go¨del diz que:
em qualquer formalizac¸a˜o consistente da matema´tica que seja su-
ficientemente forte para definir o conceito de nu´meros naturais, se
pode sempre construir uma afirmativa que na˜o pode ser provada
verdadeira ou falsa dentro do sistema.
Mais especificamente, seja F um sistema de primeira ordem no qual igual-
dade pode ser definida. Dizemos que F e´ suficientemente rico se ao menos a
aritme´tica de primeira ordem pode ser desenvolvida dentro de F . Ou seja, os
axiomas de S devem ser teoremas de F . Go¨del provou que:
1. Se o conjunto de axiomas de um sistema for decid´ıvel (no sentido de que
podemos decidir por me´todos construtivos quando uma fo´rmula e´ ou na˜o
um axioma), enta˜o na˜o e´ poss´ıvel construir um sistema formal de primeira
ordem suficientemente rico no qual todos os teoremas dentro do sistema
sa˜o prova´veis verdadeiros.
2. A consisteˆncia de um sistema formal de primeira ordem suficientemente
rico F na˜o pode ser provado por me´todos que podem ser expressos em F .
Em particular, se S e´ consistente, enta˜o na˜o podemos provar a consisteˆncia
de S dentro de S4. Ou seja, na˜o existe uma prova absoluta de consisteˆncia
para nenhum sistema consistente e suficientemente rico.
Observe que o ı´tem (2) e´ equivalente a dizer que e´ imposs´ıvel provar a con-
sisteˆncia da matema´tica dentro de um sistema de primeira ordem. Enta˜o, como
resultado imediato do fato de que a lo´gica de primeira ordem ser consistente,
temos que a matema´tica na˜o pode ser formalizada utilizando apenas lo´gica de
primeira ordem.
A prova apresentada por Go¨del e´ feita atrave´s de uma modificac¸a˜o engenhosa
do paradoxo do mentiroso:
4E´ importante observar que S foi provado consistente por Gentzen, mas seu me´todo usa
induc¸a˜o transfinita e portanto envolve os me´todos de teoria geral de conjuntos.
28
“esta sentenc¸a e´ falsa”.
Basicamente, Go¨del provou que se nessa frase se substitui a palavra falsa pela
frase na˜o concretamente prova´vel, enta˜o a proposic¸a˜o resultante e´ verdadeira,
mas na˜o concretamente prova´vel. Estendendo esse argumento, Go¨del foi capaz
de provar que a consisteˆncia da aritme´tica na˜o pode ser provada por meios
concretos.
8.3 O me´todo de prova dos teoremas de Go¨del: func¸o˜es
recursivas
Ilustraremos aqui, de maneira intuitiva, o me´todo utilizado por Go¨del para o
sistema S.
O primeiro passo para demonstrar o resultado (1) e´ estabelecer uma corres-
pondeˆncia 1 − 1 (g) entre os s´ımbolos primitivos, expresso˜es bem formadas e
sequ¨eˆncias de expresso˜es bem formadas de S e os nu´meros naturais. A imagem
de um certo s´ımbolo ou expressa˜o e´ chamada de nu´mero de Go¨del.
Deste modo, os nu´meros de Go¨del para S (por convenc¸a˜o) sa˜o:
g(0) = 3,g(′) = 5,g(() = 7,g()) = 9,g(+) = 11,g(•) = 13,g(=) = 15,g(xn) = 15+2n
onde xn e´ qualquer varia´vel.
Depois, lembramos que uma expressa˜o e´ qualquer sequ¨eˆncia finita de s´ımbolos
primitivos, e que toda expressa˜o bem formada e´ uma expressa˜o. Atribu´ımos
nu´meros de Go¨del a expresso˜es da seguinte forma:
• Se a0a1 . . . an e´ uma sequ¨eˆncia finita de s´ımbolos primitivos, enta˜o
g(a0a1 . . . an) = 2
g(a0) · 3g(a1) · . . . · pg(an)n
onde pn e´ o n-e´simo primo.
• Se x = e0e1 . . . en e´ uma sequ¨eˆncia finita de expresso˜es, enta˜o
g(x) =
n∏
i=0
p
g(ei)
i
Observe que a correspondeˆncia g e´ 1-1 entre conjunto formado pela unia˜o dis-
junta de s´ımbolos primitivos, expresso˜es bem formadas ou sequ¨eˆncias de ex-
presso˜es e a sua imagem nos naturais. De fato, o me´todo apresentado para
calcular o nu´mero de Go¨del e´ construtivo. Reciprocamente, podemos decidir se
um dado natural e´ um nu´mero de Go¨del e, mais ainda, encontrar a expressa˜o
nesse caso.
Outra observac¸a˜o e´ que o nu´mero de Go¨del para s´ımbolos primitivos e´ ı´mpar,
enquanto que o de expresso˜es e´ par com todos os expoentes ı´mpares na fatorac¸a˜o
prima. O nu´mero de Go¨del para sequ¨eˆncias de expresso˜es e´ par com todos os
expoentes pares.
Exemplo 4 Calculemos o nu´mero de Go¨del para a expressa˜o (x1 = x1).
g((x1 = x1)) = 2
g(() · 3g(x1) · 5g(=) · 7g(x1) · 11g())
27 · 317 · 515 · 717 · 119
29
Uma vez que estabelecemos uma correspondeˆncia entre a aritme´tica e uma
linguagem formal, podemos observar que toda propriedade da linguagem for-
mal da´ origem a uma propriedade da aritme´tica e vice versa. Por exemplo, a
propriedade
ser uma expressa˜o bem formada de S
determina um u´nico conjunto de expresso˜es e, por consequ¨eˆncia, um u´nico con-
junto de nu´meros que representam a contrapartida aritme´tica da propriedade
em questa˜o, a saber:
ser um nu´mero de Go¨del para uma expressa˜o bem formada.
Ale´m disso, note que podemos representar todos os nu´meros naturais em S.
De fato, o nu´mero zero e´ representado pela constante “0” e, de uma maneira
geral, o nu´mero n e´ representado pelo termo 0
′′...′ com n ocorreˆncias do s´ımbolo
primitivo ′. Chamaremos de numerais esses termos de S e escreveremos n¯ para
o numeral associado ao nu´mero n.
Passaremos agora a definir o conceito de func¸a˜o recursiva. As seguintes
func¸o˜es aritme´ticas sa˜o iniciais:
• a func¸a˜o zero: Z(x) = 0 para todo x ∈ N ;
• a func¸a˜o sucessor: v(x) = x+ 1 para todo x ∈ N ;
• as func¸o˜es projec¸a˜o: Uni (z1, . . . , zi, . . . , zn) = zi onde (z1, . . . , zi, . . . , zn) ∈
Nn
As seguintes operac¸o˜es elementares definem uma func¸a˜o aritme´tica a partir
de outras func¸o˜es aritme´ticas dadas:
• Substituic¸a˜o: dadas n func¸o˜es h1, . . . , hn dem varia´veis cada e uma func¸a˜o
g de n varia´veis, a func¸a˜o f e´ definida por:
f(z1, . . ., zm) = g(h1(z1, . . . , zm), h2(z1, . . . , zm), . . . , hn(z1, . . . , zm))
• Recursa˜o primitiva: dadas uma func¸a˜o h de n+ 2 varia´veis e uma func¸a˜o
g de n varia´veis, a func¸a˜o f de n+ 1 varia´veis e´ definida por:
f(z1, . . . , zn, 0) = g(z1, . . . , zn)
f(z1, . . . , zn, y + 1) = h(z1, . . . , zn, y, f(z1, . . . , zn, y))
• Minimalizac¸a˜o: associa a` func¸a˜o f de n varia´veis a func¸a˜o h de n + 1
varia´veis tal que
f(z1, . . . , zn) = min y(h(z1, . . . , zn, y) = 0)
onde min y significa “o menor y tal que”. Claro que pode ocorrer que tal
mı´nimo na˜o esteja definido para um determinado h e para certos valores
z1, . . . , zn. Desta forma, o uso de minimalizac¸a˜o sera´ restrito a`queles casos
onde existe um mı´nimo para cada conjunto de valores dos paraˆmetros zi.
Definic¸a˜o 13 1. Uma func¸a˜o recursiva e´ qualquer func¸a˜o que e´ ou inicial
ou pode ser obtida a partir de uma func¸a˜o inicial por um nu´mero finito de
aplicac¸o˜es de operac¸o˜es elementares.
30
2. Um conjunto recursivo de nu´meros naturais e´ definido como um conjunto
de nu´meros naturais cuja func¸a˜o caracter´ıstica (ou seja, a func¸a˜o que vale
0 para todos os elementos do conjunto e 1 fora dele) e´ recursiva.
3. Uma relac¸a˜o e´ recursiva se sua func¸a˜o caracter´ıstica e´ recursiva.
4. Uma func¸a˜o primitiva recursiva e´ uma func¸a˜o recursiva que pode ser obtida
a partir das func¸o˜es iniciais sem o uso de minimalizac¸a˜o.
Intuitivamente, uma func¸a˜o recursiva e´ aquela cujos valores podem ser cal-
culados por um computador. Ou seja, func¸o˜es recursivas sa˜o computa´veis. A
rec´ıproca na˜o pode ser demonstrada porque na˜o existe uma definic¸a˜o precisa do
que vem a ser computa´vel (Tese de Church).
De maneira semelhante, um conjunto recursivo de nu´meros naturais e´ intui-
tivamente um conjunto “decid´ıvel” no sentido que podemos decidir quando um
objeto esta´ ou na˜o no conjunto.
Definimos o conjunto recursivo de expresso˜es bem formadas como sendo todo
conjunto para o qual o conjunto correspondente de nu´meros de Go¨del e´ recur-
sivo. Similarmente, uma relac¸a˜o entre expresso˜es bem formadas e´ dita recursiva
se a relac¸a˜o correspondente nos nu´meros naturais tambe´m e´ recursiva. Em
particular, dizer que o conjunto de axiomas de um sistema formal e´ decid´ıvel
significa que o seu conjunto de nu´meros de Go¨del e´ recursivo. Um sistema cujo
conjunto de axiomas e´ recursivo e´ dito axioma´tico.
Dada uma relac¸a˜o R de grau n entre nu´meros naturais, dizemos que R pode
ser expressa em S se existe uma expressa˜o bem formada A(x1, . . . , xn) tal que:
i. Se a n-tupla 〈y1, . . . , yn〉 de nu´meros naturais esta´ em R, enta˜o
⊢ A(y¯1, . . . , y¯n)
onde y¯i representa o numeral associado a yi.
ii. Se a n-tupla 〈y1, . . . , yn〉 de nu´meros naturais na˜o esta´ em R, enta˜o
⊢ ¬A(y¯1, . . . , y¯n)
Se R pode ser expressa em S, dizemos que A(x1, . . . , xn) expressa R.
A importaˆncia crucial do conceito de recursividade se baseia no fato de que
toda relac¸a˜o recursiva pode ser expressa em S. E e´ essa possibilidade de expressar
afirmativas sobre S dentro de S que e´ importante para provar os resultados (1)
e (2) formulados por Go¨del.
A ide´ia da prova de (1) e´ baseada na construc¸a˜o de uma expressa˜o bem
formada G de S tal que nem G nem ¬G podem ser provadas como teorema de
S se S e´ consitente. O me´todo para obter tal G utiliza os nu´meros de Go¨del.
Passemos enta˜o a` prova detalhada do primeiro teorema de Go¨del.
8.3.1 Prova do primeiro teorema de incompletude de Go¨del
Em primeiro lugar, definimos os predicados P e Q.
P Sejam n o nu´mero de Go¨del de alguma sequ¨eˆncia de expresso˜es e1, . . . , en
e m o nu´mero de Go¨del de uma expressa˜o bem formada e. Definimos o
predicado Pnm como sendo verdadeiro se e1, . . . , en ⊢ e. Dizemos que P
prova o par 〈n,m〉.
31
Q Seja Qx uma expressa˜o bem formada que possui uma u´nica varia´vel livre
x e seja n o seu nu´mero de Go¨del. Representamos por Qn a expressa˜o
bem formada (fechada) formada a partir de Qx instanciando todas as
ocorreˆncias de x por n. Uma vez que Qn possui um nu´mero de Go¨del,
definimos o predicado Qxy que diz que y e´ o nu´mero de Go¨del de Qx.
Por um lado, Qn significa que algum nu´mero n possui a propriedade n. Mas
Qn tambe´m diz que a expressa˜o bem formada com nu´mero de Go¨del n (a saber,
Qx), possui a propriedade Q, uma vez que n e´ apenas a refereˆncia a Qx. Ou
seja, n cria um tipo de auto-refereˆncia indireta5. Observe que predicados que
fazem refereˆnca a si pro´prios correspondem a func¸o˜es recursivas.
Com o predicado Pxy, podemos tambe´m dizer que uma expressa˜o bem for-
mada A na˜o e´ um teorema, ou na˜o pode ser provada em S.De fato, seja a o
nu´mero de Go¨del de A. Enta˜o a expressa˜o
¬(∃x.Pxa)
diz que na˜o existe sequ¨eˆncia que prova A, ou simplesmente:
¬(⊢ A)
O segundo passo para provar o teorema de Go¨del consiste em construir a
sentenc¸a bem formulada F de S:
F : ¬(∃x.∃y.Pxy ∧Qzy)
Em palavras, F diz que na˜o existe uma prova do par 〈x, y〉 onde y e´ o nu´mero
de Go¨del de Qz. Ou seja, Qz na˜o pode ser provado em S.
Para fazer F falar de si pro´prio, instanciamos a u´nica varia´vel livre de F , z,
ao nu´mero f de Go¨del de F :
G : ¬(∃x.∃y.Pxy ∧Qfy)
Alguns comenta´rios sobre G:
i. G = Qf , ou seja, G e´ a auto refereˆncia de F .
ii. G diz que na˜o existe prova do par 〈x, y〉, onde y e´ o nu´mero de Go¨del de
Qf . Mas Qf e´ G.
iii. Ou seja, G diz que na˜o existe prova em S de G:
G ≡ ¬(⊢ G)
iv. Mas a negac¸a˜o de G tambe´m na˜o pode ser provada em S. De fato, suponha
que ¬G seja prova´vel em S. Ou seja,
⊢ ¬G
Como G e´ o mesmo que a proposic¸a˜o ¬(⊢ G), obtemos
⊢ ¬G ≡ ⊢ ¬(¬(⊢ G))
≡ ⊢ G
o que contraria a nossa hipo´tese.
5Se voceˆ tem a impressa˜o que o ce´rebro vai dar um no´, enta˜o e´ porque voceˆ esta´ entendendo.
32
v. Desta forma, dizemos que G e´ indecid´ıvel em S, ou seja, nem G nem a sua
negac¸a˜o podem ser provados em S.
O comenta´rio v acima ja´ e´ suficiente para provar a incompletude de S e, por-
tanto, provar o primeiro teorema de incompletude de Go¨del para S.
Mas o fato mais extraordina´rio sobre G e´ que ele e´ verdadeiro! De fato, G
diz que na˜o existe prova de G em S e isso no´s acabamos de ver que e´ verdadeiro.
Observe que no´s “provamos” que G e´ verdadeiro atrave´s de uma meta-ana´lise,
na˜o dentro de S.
Ou seja, na˜o obstante existem expresso˜es bem formadas que na˜o podem ser
provadas em S, existem teoremas que na˜o podem ser provados.
Vale notar que existem outras provas do resultado (1). Algumas bastante
simples, como a descrita abaixo:
1. Algue´m mostra a Go¨del a MV U , uma ma´quina que supo˜e-se ser uma
Ma´quina da Verdade Universal, capaz de responder corretamente qualquer
pergunta.
2. Go¨del pede para ver o programa e o circuito da MVU . O programa pode
ser complicado, mas possui comprimento finito. Chamemos este programa
de P (MV U).
3. Sorrindo de maneira sarca´stica, Go¨del escreve a seguinte sentenc¸a:
“A ma´quina constru´ıda com base no programa P (MV U) nunca vai dizer
que esta sentenc¸a e´ verdadeira.”
Chame a sentenc¸a acima de G, de Go¨del. Note que G e´ equivalente a:
“MVU nunca vai dizer que G e´ verdadeiro.”
4. Agora Go¨del ri e pergunta a MVU se G e´ verdadeiro ou na˜o.
5. Acontece que se MV U diz que G e´ verdadeiro, enta˜o “MVU nunca vai
dizer que G e´ verdadeiro” e´ falso. Da mesma forma, se MVU diz que G
e´ falso, enta˜o “MVU nunca vai dizer que G e´ verdadeiro” e´ verdadeiro.
PortantoMV U na˜o pode dar nenhuma resposta, uma vez que faz apenas
afirmativas verdadeiras.
6. Em particular, MVU nunca vai dizer que G e´ verdadeiro. Ou seja, G e´
verdadeiro!
7. “Eu sei uma verdade que MVU nunca podera´ provar,” diz Go¨del. “Eu
sei que G e´ verdadeiro. MVU na˜o e´ universal!”
Observe que a prova acima mostra que Go¨del provou uma coisa que