O Mtodo AxiomticoCurso de vero UFSC, 01-05/02/2010 Jairo Jos da Silva Histrico Perodo clssico: a) Aristteles: O Primeiros Analiticos (340 A.E.C.) constitui o primeiro estudo de lgica formal da histria; a silogstica aristotlica um tratado sistemtico, mas longe de exaustivo, de modos vlidos de inferncia formal, isto , regras para se obter concluses verdadeiras a partir de pressupostos verdadeiros, que no dependem, porm, do contedo material particular (o qu est sendo dito), mas apenas da forma lgica das asseres envolvidas (abstradas de seu contedo material; i.e. independentemente da denotao de seus termos). Dedues vlidas preservam a verdade, por oposio a indues, que preservam a falsidade na deduo a verdade flui; na induo, reflui. Uma inferncia logicamente ou formalmente vlida se a veracidade das premissas condio suficiente (mas possivelmente no necessria) para a veracidade da concluso, independentemente de se premissas e concluso so ou no efetivamente verdadeiras. Por exemplo, a seguinte inferncia formalmente vlida: se todos os homens so imortais, dado que Scrates homem, ento Scrates imortal; apesar da premissa maior e a concluso serem juzos falsos. Essa inferncia envolve as regras de especificao e modus ponens. A premissa maior: para todo x, se x tem a propriedade Q, ento x tem a propriedade P, nos d, por especificao: se a tem a propriedade Q, ento a tem a propriedade P. Como, pela premissa menor, a tem a propriedade Q, ento, por modus ponens, tem-se a concluso: a tem a propriedade P (na verdade, essas duas regras no so mencionadas por Aristteles. Uma regra de inferncia tipicamente aristotlica o silogismo Barbara: se todo A B e todo B C, ento todo A C). No Segundos Analiticos (330 A. E. C.) Aristteles apresenta sua viso do conhecimento cientfico como um edifcio construdo sobre princpios necessrios. Nesses dois livros esto os fundamentos do mtodo axiomtico em cincia. b) Euclides (300 A.E.C.): Em Os Elementos h, como em Aristteles, uma clara distino entre princpios (postulados, verdades evidentes da cincia do espao, e noes comuns,

1

verdades da razo) e teoremas (Euclides separa teoremas de problemas, que envolvem construes). No h, porm, uma distino entre termos primitivos, cujo sentido obvio, e termos derivados, cujo sentido dado por definies (Euclides apresenta definies de todos os termos). Ao contrrio de Aristteles, as regras de inferncia no so explicitadas; mas, como em Aristteles, a linguagem no formal. O sistema de Euclides , ademais, uma axiomtica material, i.e. que se refere a um contexto materialmente determinado o espao da percepo (veja as definies abaixo). c) Aristarco de Samos (sc. III A.E.C.): Sobre os tamanhos e distncias do Sol e da Lua o primeiro tratado axiomtico de Astronomia (Aristarco props um sistema heliocntrico). Arquimedes (sc. II A.E.C.) aplica o mtodo axiomtico Fsica (Esttica e Hidrosttica). Idade Mdia: traduo e assimilao no Ocidente da tradio clssica, a partir do sculo XII E.C. a partir de tradues rabes e originais gregos (as tradues fluem da Espanha muulmana el Aldalus , Toledo principalmente. A rapinagem promovida pelos cruzados em Constantinopla, em 1204, provavelmente aumenta o estoque de originais gregos na intelectualmente depauperada Europa latina) . a) Leonardo Fibonacci (Leonardo de Pisa): escreve o tratado axiomtico de geometria A prtica da geometria, 1220. b) Jordano de Nemora (Jordanus Nemorarius): tratado axiomtico de aritmtica Aritmtica, 1250. c) Thomas Bradwardine: aplicao do mtodo axiomtico no apenas matemtica e fsica, mas tambm teologia. Em seu Tratado sobre as propores das velocidades e dos movimentos (1328) o mtodo aplicado pela primeira vez cinemtica (exercendo influncia em Galileu); em Tratado sobre o contnuo (1335) aplica o mtodo ao estudo das grandezas contnuas em matemtica e fsica; em Sobre a causa de Deus (1340) tentou dar forma axiomtica s provas da existncia e atributos de Deus (no que foi seguido por Descartes e Spinoza). Idade Moderna: a) axiomatizao de teorias fsicas: Nicol Tartaglia (1537): Cincia Nova mecnica; Guidobaldo del Monte (1577): Livro das Mecnicas mecnica; Galileu (1638): terceira jornada dos Discursos sobre duas novas cincias (Sobre o movimento local) fundamentos da cinemtica.

b) axiomatizao da metafsica: Descartes (1641): Respostas s segundas objees s Meditaes Metafsicas apresentao axiomtica da demonstrao da existnca de Deus; Benedictus (Baruch) Spinoza (1663): Princpios da Filosofia de Descartes demonstrados de modo geomtrico apresentao axiomtica da filosofia de Descartes; tica, demonstrada de modo geomtrico (1677) sistema axiomatizado de metafsica. c) Blaise Pascal (1656): Sobre o esprito geomtrico elogio do mtodo axiomtico, introduo da idia de termos primitivos e regras para definies (termos devem ser definidos a partir de termos mais simples), axiomas (devem ser evidentes) e demonstraes (proposies devem ser demonstradas a partir de proposies evidentes e outras j demonstradas). Arnold & Nicole: Logique de Port Royal (1662) repete as regras de Pascal. Leibniz (circa 1670) apresenta suas idias seminais de caracteristica universalis, uma linguagem simblica, como a da aritmtica, para a expresso dos juzos, de calculus ratiocinatur, um sistema de regras de clculo, maneira das regras do clculo aritmtico, para se raciocinar sem pensar, isto , operando com smbolos segundo regras (daprs Raimond Lulio e Thomas Hobbes) e de mathesis universalis, uma cincia universal expressa na caracterstica e desenvolvida segundo o clculo regrado (lembre-se que o clculo infinitesimal de Leibniz era justamente um clculo regrado, e que ele foi um dos grandes criadores de notao matemtica). Isaac Newton (1687): Principia Mathematica axiomatizao da cincia do movimento (ele apresenta seus trs axiomas como leis: a primeira, o princpio de inrcia de Galileu, , na verdade, a definio de sistema inercial; a segunda tambm uma definio, a definio mecnica de fora; a terceira apenas um axioma propriamente dito): os princpios que Newton elenca, no entanto, no so apresentados como proposies evidentes. Optica (1704) tratamento axiomtico da ptica; as demonstraes, porm, no tem carter lgico, envolvendo observaes e experimentos. Idade Contempornea: A axiomtica, em sua vertente formal, alcana plena realizao na segunda metade do sculo XIX; contribuiram para isso os desenvolvimentos que culminaram na criao da geometria no-Euclidiana (Lobachevski, 1829; Bolyai, 1832), lgica simblica (Boole, Peirce, Schrder, Frege) e teoria de conjuntos (Cantor: teoria ingnua; Zermelo: teoria axiomtica). a) geometria no-Euclidiana: Saccheri (1733): Euclides livre de toda mcula tentativa de demonstrar o postulado das paralelas por reduo ao absurdo. Gauss: trabalhos nopublicados de geometria no-euclidiana (hiperblica). Geometria hiperblica: Lobachevski,

3

1829; Bolyai, 1832. Beltrami: modelo euclidiano para partes da geometria hiperblica; Klein (1871) e Poincar (1881): modelos euclidianos para a geometria hiperblica. b) Grasmann (1844): Teoria da extenso linear idia de espao vetorial n-dimensional. Riemann (1854): Sobre as hipteses que subjazem aos fundamentos da geometria geometria riemanniana de espaos abstratos n-dimensionais de curvatura varivel. Helmholtz (1870): Sobre a origem e o significado dos axiomas da geometria idia de geometria como cincia puramente formal (no uma teoria do espao da intuio), estabelecida sobre bases axiomticas hipotticas e passvel de diferentes interpretaes. c) Pash (1882): Lies de geometria moderna axiomatizao da geometria projetiva. Hilbert (1899): Fundamentos da geometria apresentao da geometria euclidiana (mas tambm no-euclidianas) como sistemas axiomticos desprovidos de interpretao privilegiadas (demonstravelmente consistentes com relao aritmtica, dado que admitem interpretaes aritmticas). Outras axiomatizaes da geometria euclidiana: O. Veblen (1904), V. Huntington (1913). d) Axiomatizao da teoria dos grupos: Huntington e, independentemente, E. H. Moore (1902); geometria elptica: G. Halsted (1904) e G. Hessenberg (1905); topologia de conjuntos de pontos: Haussdorf (1914); teoria das magnitudes contnuas: Huntington (1902). Por essa poca a concepo formal do mtodo axiomtico estava plenamente estabelecida: sistemas de axiomas so, nas palavras de Hilbert, definies implcitas dos termos que neles ocorrem (ou, como prefiro, definies de estruturas ou famlias de estruturas formais). Segundo essa concepo, sistemas axiomticos no expressam verdades materialmente determinadas, mas apenas relaes formais, s vezes arbitrariamente estabelecidas, entre objetos no especificados. d) Axiomatizao da lgica: G. Boole (1847): A anlise matemtica da lgica desenvolvendo a idia leibniziana de uma caracteristica (um sistema simblico) e um calculus ratiocinatur (um sistema de regras para manipulaes de smbolos), Boole cria uma aritmtica para o pensamento que permite realizar operaes elementares de raciocnio como se fossem clculos aritmticos. Boole entendia que esse clculo, que hoje conhecemos como lgebras de Boole, poderia receber diferentes interpretaes, sendo assim simplesmente a teoria de uma estrutura formal que subjaz a vrios domnios materialmente distintos (ou, equivalentemente, a teoria desses domnios considerados exclusivamente em seus aspectos formais). G. Frege (1879): A conceitografia: uma linguagem formal para o pensamento copiada da aritmtica axiomatizao da lgica; Frege apresenta um sistema axiomatizado de lgica de segunda ordem, contendo como subsistemas o clculo proposicional clssico e a

lgica clssica de primeira ordem (ou clculo elementar de predicados). O sistema de Frege formalizado, mas tem interpretao determinada fixa (ou seja, interpretado). Infelizmente, ele se revelou inconsistente, como demonstrou Russell (1902), com o famoso paradoxo que leva o seu nome. e) Axiomatizao da aritmtica: G. Peano (1889 e, de modo aperfeioado, 1895) axiomatizao da aritmtica elementar a partir dos trabalhos de R. Dedekind. Peano introduziu uma linguagem simblica que se tornou bem mais popular que a de Frege. f) Teoria de conjuntos: Cantor (1874-1897): teoria ingnua paradoxos: Burali-Forti (maior ordinal), Cantor (maior cardinal ou conjunto universo), Russell (1902, inconsistncia da noo lgica irrestrita de conjunto). Teorema da boa-ordem (todo conjunto pode ser bemordenado): na busca de uma demonstrao desse resultado, Zermelo (Investigaes sobre os fundamentos da teoria de conjuntos, 1908) encontra uma axiomatizao (incompleta) da teoria de conjuntos. Essa axiomatizao completada por A. Fraenkel em 1922 (com o acrscimo do axioma da substituio): teoria ZF. g) Axiomatizao de teorias fsicas: o sexto problema de Hilbert (1900). Axiomatizao da mecnica: G. Hamel (1909): Sobre os fundamentos da mecnica. C. Carathodory (1909): Sobre os fundamentos da termodinmica. h) Axiomatizao da teoria das probabilidades: A. Kolmogorov (1933): Conceitos fundamentais da teoria das probabilidades. Em 1931 K. Gdel demonstra seus clebres teoremas de incompletude: o primeiro mostra as limitaes da formalizao em matemtica (a noo formal de demonstrao no sempre forte o suficiente para representar a noo matemtica de verdade); o segundo mostra que a aritmtica elementar (i.e. de primeira ordem) de Peano, teorias a ela equivalentes ou suas extenses no so capazes de demonstrar a sua prpria consistncia; ou melhor, no se pode representar nessas teorias uma demonstrao de sua consistncia (isso exige necessariamente teorias mais potentes). Definies Def. 1: Uma linguagem um conjunto de smbolos (o alfabeto da linguagem) com os quais so escritas as expresses bem-formadas da linguagem, isto , seqncias admissveis de smbolos do alfabeto. So expresses bem-formadas: 1) os termos, que denotam objetos do domnio (ou domnios) a que a linguagem se refere termos podem ser constantes, quando denotam um objeto determinado do domnio de discurso, tais como D. Pedro II, o

5

meu irmo, seno, ou 1+1; ou variveis, como, por exemplo, 2+x ou y+1, quando envolvem variveis individuais sobre o universo de objetos do domnio de discurso; termos variveis denotam objetos determinados do domnio apenas quando as variveis individuais que neles ocorrem recebem um valor determinado (uma valorao) e 2) as frmulas, expresses da linguagem que denotam asseres ou enunciados; frmulas podem tambm funcionar como variveis (funes proposicionais), quando envolvem variveis individuais ou termos variveis, como ele um crpula, x maior que y ou x+2 = 4 (onde ele, x e y so variveis individuais), e representam enunciados completos apenas quando as variveis individuais que porventura nelas ocorram so valoradas; ou como constantes, em cujo caso chamam-se sentenas, sentenas so frmulas em que no ocorrem variveis de nenhuma espcie, e que, assim, admitem um valor de verdade (verdadeiro ou falso) determinado, por exemplo, Pedro um crpula, 2 maior que 3, ou todo homem mortal. Ex.: as linguagens naturais (portugus, ingls, etc.) e as linguagens artificiais (linguagens matemticas, linguagens de programao). Linguagens podem ser interpretadas ou no. As linguagens naturais so sempre interpretadas, isto , sequncias de smbolos do alfabeto da linguagem compem unidades de significado. As menores dessas unidades so os morfemas; por exemplo, em Portugus: rvore, -al, in-, eu, -ose (in-, por exemplo, um prefixo que denota negao). Unidades maiores de significado so composies de morfemas. As linguagens matemticas so tambm, em geral, interpretadas; qunado fazemos geometria, por exemplo, os termos reta, ponto, plano, crculo, etc., tm significados precisos e determinados (eles denotam certos conceitos abstratos, instanciveis por abstrao e idealizao). Porm, ns podemos abstrair qualquer linguagem matemtica do seu contedo material, isto , do significado determinado associado a seus smbolos e expresses, tornando-a numa linguagem no-interpretada a qual outros significados podem ser atribudos. O mesmo pode ser feito com qualquer teoria matemtica, esse processo chamado de abstrao formal. Por seu intermdio teorias matemticas so depuradas de qualquer contedo material, tornando-se teorias no-interpretadas que, ao invs de descrever um domnio particular, descreve qualquer domnio que possa interpret-la, mas apenas em seus aspectos formais, i.e. aqueles que todos os domnios que satisfazem, por interpretao, uma teoria condividem.

Def. 2: Um conjunto decidvel se existe um algortmo (uma regra, um procedimento mecnico, um programa de computador) para decidir se um objeto qualquer ou no um elemento do conjunto. Ex.: o conjunto de nmeros primos. Def. 3: Uma linguagem formal (ou formalizada) se o alfabeto e os conjuntos dos termos e das frmulas, e, portanto, o conjunto das expresses bem-formadas da linguagem, so decidveis (as linguagens naturais no so linguagens formais; no existe um procedimento de deciso que nos diga, por exemplo, se cacumbu ou no uma expresso bem-formada do portugus). Uma linguagem formal, portanto, tem regras explcitas para a formao de suas expresses bem-formadas. Def. 4: Uma regra de deduo (ou derivao) pode ser entendida como uma funo entre asseres cujo valor para um conjunto de asseres (ditas as premissas da deduo) uma outra assero (dita a concluso da deduo). Uma regra de deduo logicamente vlida se a concluso tiver que necessariamente ser admitida como verdadeira sempre que as premissas forem assim admitidas (sejam as premissas ou a concluso de fato verdadeiras ou no como se v, a lgica tem carter coercitivo no campo da razo, ns podemos ser ilgicos, s no podemos ser ao mesmo tempo racionais). Exs. modus (ponendo) ponens: premissas A e A B, concluso B; modus (tollendo) tollens: premissas B e A B, concluso A (onde A e B denotam asseres quaisquer); generalizao: premissa x tal e tal, concluso para todo x que satisfaa a condio C, x tal e tal, desde que a justificao da premissa imponha varivel x a condio C. Uma deduo (derivao ou demonstrao) uma sequncia (suposta, em geral, finita) de asseres em que ocorrem apenas pressupostos e asseres obtidas de asseres anteriores na sequncia por regras de deduo. Uma deduo logicamente vlida se utilizar apenas regras de derivao logicamente vlidas (inferncias indutivas no so logicamente vlidas; indues na verdade preservam falsidade, no veracidade). Note que a validade das regras de deduo lgica independe do significado das asseres envolvidas (ns no precisamos saber o significado das asseres A e B para assentir para a validade da regra de modus ponens; basta saber o significado do conectivo lgico que exprime a implicao material). Isto precisamente marca o carter formal da lgica: a validade lgica depende apenas da forma lgica, no do contedo das asseres envolvidas (podemos definir a forma lgica de uma assero como essa assero abstrada de seu contedo material, i.e. o significado dos seus termos).

7

Def. 5: Uma teoria simplesmente um conjunto de asseres de uma linguagem, nem necessariamente formal, nem necessariamente desprovida de interpretao, juntamente com um aparato dedutivo (nem sempre explicitado). Por exemplo, o conjunto de todas as sentenas de uma linguagem L, conveniente para descrever a estrutura do conjunto dos nmeros reais, que so verdadeiras nesse conjunto (essa teoria usualmente denotada por ThLR ou simplesmente ThR, se a linguagem est subtendida). Denotamos por CnA, A T, o conjunto das asseres derivveis no sistema a partir de A, isto , tomando as asseres de A como pressupostos. Se existe um conjunto decidivel Ax T, dito os axiomas de T, tal que CnAx = T, T diz-se axiomatizvel (se o conjunto Ax for finito dizemos que T finitamente axiomatizavel). Uma teoria que j vem provida de um conjunto decidivel de axiomas dita axiomatizada (finitamemte axiomatizada se esse conjunto for finito). O aparato dedutivo subjacente uma teoria constitudo por um conjunto de axiomas lgicos e por regras de deduo (h vrias lgicas possveis, cada uma com seu conjunto de axiomas e suas regras de derivao). Regras e axiomas no so, em geral, completamente explicitados, mas so, em princpio, explicitveis. Os axiomas lgicos so asseres formalmente (ou logicamente) verdadeiras; isto , verdadeiras em todas as interpretaes ou reinterpretaes possveis da linguagem em que so expressos. Asseres desse tipo so s vezes chamadas de analticas, verdadeiras em todos os contextos possveis ou mundos possveis, numa expresso atribuda a Lebniz, que ele, porm, nunca formulou , ou ainda, verdadeiras em virtude da forma, no do contedo. Por exemplo, se A e B denotam asseres quaisquer, ento A (B A) denota um axioma; note que essa assero verdadeira independentemente do significado de A ou B, ou seja, formalmente verdadeira. Uma nota de cuidado, porm: a verdade incondicional desse axioma depende da interpretao que atribumos ao conectivo denotado por , que expressa o condicional se...ento; se atribuirmos a esse conectivo um outro significado, possvel que essa assero perca o seu carter analtico. Isso ocorre em particular com a negao. A assero A A, ou seja, negar duas vezes implica afirmar, s analtica na interpretao clssica da negao; na interpretao intuicionista essa assero nem sempre verdadeira. Em suma, a veracidade, e, portanto, a analiticidade de asseres depende da interpretao dos smbolos lgicos da linguagem. As dedues num sistema axiomtico podem admitir como pressupostos tanto axiomas lgicos quanto axiomas do sistema. Um teorema do sistema a ltima assero de uma derivao (que a demonstrao desse teorema). Podemos tambm, em dedues, usar

teoremas j demonstrados; eles no tm, entretanto, carter de pressupostos, uma vez que podem ser justificados nas demonstraes em que ocorrem (basta, nas demonstraes em que uma assero j demonstrada aparece, colocar antes dela a sua demonstrao, e ela ficar assim justificada). Def. 6: Um sistema axiomtico (ou teoria axiomtica) formal (ou formalizado) se suas asseres forem expressas numa linguagem formal e sua lgica subjacente for uma lgica formal, isto , suas regras de inferncia forem explicitamenet dadas e formalmente vlidas e, ademais, o seu conjunto de axiomas lgicos for recursivo. Isso implica que o conjunto das dedues no sistema decidvel; ou seja, h um algoritmo que decide se uma sequncia qualquer dada de frmulas da linguagem uma deduo vlida no sistema. Note que os teoremas de um sistema axiomtico formal no constituem necessariamente um conjunto decidvel (se isso fosse verdade, os matemticos poderiam, em princpio, ser substitudos por computadores). O conjunto de teoremas de uma teoria axiomtica formal, entretanto, sempre semi-decidvel, ou recursivamente enumervel, i.e. ns temos um algortimo para enumerar os teoremas da teoria. Em outras palavras, existe um orculoque responde sim pergunta A um teorema do sistema? se a sentena A, expressa na linguagem da teoria, for, de fato, um teorema do sistema, mas que no d nenhuma resposta se A no for um teorema do sistema. Note que se um conjunto e seu complemento so semi-decidveis, ento o conjunto decidivel. Eis como podemos efetivamente enumerar teoremas: escreva todas as sequncias de smbolos do alfabeto que tenham comprimento igual a 1 (h apenas um conjunto finito delas, se o alfabeto for finito), percorra esse conjunto e selecione as expresses bem-formadas; repita o procedimento para sequncias de comprimento igual a 2; e assim por diante. Isso nos d uma enumerao efetiva das expresses bem-formadas da linguagem, seja {Fn} essa sequncia. Agora, uma deduo um subconjunto finito de elementos dessa sequncia, e h um procedimento algortmico que enumera subsequncias finitas de uma sequncia enumervel; resta apenas percorrer essa enumerao, selecionar as subsequncias que so dedues e tomar a expresso bem-formada que comparece em ltimo lugar em cada uma delas. Note que esse procedimento requer que os conjuntos das expresses bem-formadas e das dedues sejam decidiveis. Def. 7: Um sistema axiomtico no-interpretado se suas asseres so expressas em linguagem no-interpretada. Um sistema pode ser no-interpretado sem ser formal (e.g. a geometria axiomatizada por Hilbert), e vice-versa, se ele visto como teoria de um domnio particular (e.g. a aritmtica axiomatizada por Frege). Nas aplicaes contemporneas do9

mtodo axiomtico prefere-se, no entanto, axiomatizaes simultaneamente formais e nointerpretadas. Exemplo de linguagens formais no-interpretadas: as linguagens de primeira ordem Uma linguagem no-interpretada essencialmente um conjunto de smbolos, com os quais podemos denotar e descrever, mediante interpretaes, no importa o que nos interessa denotar e descrever: objetos e suas propriedades, funes e relaes entre objetos e fatos envolvendo isso tudo. Linguagens no-interpretadas admitem diferentes interpretaes; isto , podemos nos referir a diferentes domnios usando a mesma linguagem (nesse caso esses domnios dizem-se de mesma assinatura). Um exemplo de linguagens no-interpretadas formais so as chamadas linguagens de primeira ordem. Essas linguagens admitem os seguintes smbolos: smbolos lgicos, que so sempre interpretados do mesmo modo; entre eles destacam-se os conectivos (que conectam frmulas originando novas frmulas), tais como a disjuno ou (denotada por , do latim vel), a conjuno e (, o invertido), a implicao material se ..., ento ... (geralmente denotada por ), a negao no o caso que () e a equivalncia material se, e somente se (). So tambm lgicos os smbolos chamados de quantificadores, que denotam generalidade, como o quantificador universal para todo (, o A inicial do alemo alles invertido) e o quantificador existencial existe (, o E inicial de es gibt invertido). Esses smbolos ocorrem tipicamente em asseres do tipo todo elemento x tem a propriedade R (em smbolos: x (Rx)) ou existe um elemento x que tem a propriedade R (x (Rx)). O x que aparece nessas asseres (ou frmulas) denota um elemento arbitrrio do domnio de discurso e chamado de smbolo de varivel (nesses exemplos o smbolo de varivel x ocorre ligado, isto , sob o escopo de quantificador; em caso contrrio, como na frmula Rx o elemento x tem a propriedade R o smbolo de varivel ocorre livre. Note que se um smbolo de varivel ocorre livre em uma frmula, ela no tem um valor de verdade verdadeira ou falsa determinado em qualquer interpretao para a linguagem, independentemente de uma atribuio de referente para o smbolo de varivel que ocorre livre). Os smbolos de variveis esto entre os smbolos no-lgicos, que admitem diferentes interpretaes. Alm dos smbolos de variveis a linguagem pode conter, mas no necessariamente, outros smbolos no-lgicos, os smbolos de constantes, que denotam elementos determinados do domnio de discurso (que podem, no entanto, variar com o domnio), os smbolos de funes (que denotam funes determinadas do domnio) e os

smbolos de relaes (que denotam relaes definidas no domnio). Um smbolo lgico que ocorre com frequncia o smbolo de identidade = (usado apenas para denotar que duas expresses que se referem a objetos do domnio, os termos da linguagem smbolos de variveis ou de constantes, ou expresses mais complexas involvendo esses smbolos e smbolos de funes, como 2 + x e indica que esses termos denotam o mesmo objeto, por exemplo: 2 + x = x + 2). Podem ocorrer tambm smbolos sem interpretao, como os parnteses, usados apenas para facilitar a leitura da frmula, mas eles no so essenciais (a chamada notao polonesa prescinde desses smbolos de pontuao). As linguagens de primeira ordem so as mais comuns como meios de expresso da matemtica formal. A caracterstica dessas linguagens que seus smbolos de variveis s denotam objetos do domnio (mesmo que possa haver smbolos de relaes e de funes, eles no funcionam como variveis). Linguagens em que h smbolos de variveis para funes, relaes ou conjuntos de objetos do domnio so chamadas de linguagens de segunda ordem (h, em princpio, linguagens de qualquer ordem superior). H tambm linguagens infinitrias, que admitem frmulas de comprimento infinito, e linguagens com outros tipos de quantificadores (tais como, existem infinitos x, para a maioria dos x, etc.), alm de linguagens modais, enriquecidas com operadores sentenciais, tais como os operadores necessario que ou possvel que. Muitas teorias matemticas, porm, podem ser formalizadas em primeira ordem (teoria de conjuntos, teorias algbricas de grupos, corpos, etc. teorias geomtricas) ou segunda ordem (aritmtica). Mas mesmo as teorias que exigem linguagens superiores, como a aritmtica, admitem verses elementares, isto , de primeira ordem. Interpretaes de linguagens de primeira ordem Uma interpretao de uma linguagem de primeira ordem uma atribuio de significado para os seus smbolos no-lgicos da linguagem. Em primeiro lugar, uma interpretao fixa um universo de discurso ou domnio de variao para os smbolos de variveis. Nesse domnio, os smbolos no-lgicos que a linguagem porventura tiver so interpretados: elementos fixos do domnio interpretam os smbolos de constantes, funes e relaes definidas no domnio interpretam, respectivamente, eventuais smbolos de funes e relaes da linguagem, e assim por diante. Expresses da linguagem em que smbolos de variveis s ocorrem ligados (i.e. sob o escopo de algum quantificador), as chamadas sentenas, tm um valor de verdade determinado numa dada interpretao. Por exemplo, a sentena x (x < 0)

11

verdadeira se o universo for, por exemplo, o conjunto dos nmeros inteiros, o smbolo de constante 0 denotar o nmero 0 e o smbolo de relao < denotar a relao estritamente menor que, j que existe um nmero inteiro estritamente menor que 0. Por outro lado, se mudarmos o domnio pelo conjunto dos inteiros no-negativos, e mantivermos inalterada a interpretao dos smbolos no-lgicos, a sentena se torna falsa. Frmulas que contm variveis livres, como x < 0 no tem um valor de verdade determinado em uma dada interpretao, a menos que fixemos um valor para os smbolos de variveis que ocorrem livres na frmula. As funes do conjunto de smbolos de variveis da linguagem no universo so chamadas de valoraes. Por exemplo, se A(x) denota a frmula (x < 0), I a primeira interpretao acima e v a valorao em que x recebe o valor -1 (irrespectivamente dos valores que os outros smbolos de variveis recebem) ento A verdadeira em I com a valorao v, em smbolos: I |= A(x)(v) ou I(A(x))(v) = T, onde T denota o verdadeiro. Sentenas expressam propriedades formais ou estruturais que os domnios estruturados que interpretam as linguagens em que so expressas podem ou no possuir. Se eles as possuem, as sentenas so verdadeiras nessas interpretaes; se no, so falsas. Uma interpretao para L, a linguagem de uma teoria T, que torna todas as sentenas de T verdadeiras um modelo de T. Axiomatizar uma teoria, como vimos, encontrar um conjunto decidivel de axiomas suficientes para a derivao de todas as asseres da teoria. Formalizar uma teoria axiomatiz-la num contexto formal definido, como uma teoria axiomtica formal. Isso tem vrias vantagens: 1) torn-la mais clara e precisa; 2) tornar explcitos os seus fundamentos ou pressupostos; 3) tornar possvel a verificao mecnica i.e. algortmica de pretensas demonstraes na teoria; 4) explicitar o seu arcabouo formal e a estrutura comum a todos os modelos da teoria isso pode possibilitar a investigao de propriedades de um modelo por intermdio da investigao de outros. Por exemplo, como a teoria axiomtica formal dos corpos algebricamente fechados de caracterstica 0 tem a propriedade que de ser completa, i.e. se uma sentena da linguagem da teoria verdadeira em um modelo verdadeira em todos (sendo, portanto, logicamente derivvel dos axiomas da teoria, uma vez que a lgica de primeira ordem completa i.e. a noo de validade e teorema so extensionalmente equivalentes), podemos demonstrar fatos sobre qualquer corpo algebricamente fechado de caracterstica 0 demonstrando-os para o corpo dos nmeros complexos. Podemos, para tanto, usar qualquer extenso da teoria que seja verdadeira nesse corpo, mesmo que esse recurso no esteja disponvel em outros corpos algebricamente fechados de caracterstica 0. 5)

possibilitar investigaes de natureza metamatemtica: a teoria consistente, completa, categrica? Como so seus modelos, h algum especial? A forma lgica dos axiomas de uma teoria pode, em particular, nos dizer algo sobre seus modelos; por exemplo, que subestruturas ou extenses de modelos tambm so modelos, que unies de cadeias de modelos tambm so modelos, etc.; 6) possibilitar o estudo de relaes lgicas entre teorias (por exemplo, a teoria T extenso conservativa da teoria T i.e. apesar da linguagem ou axiomas de T estenderem a linguagem ou os axiomas de T, aquela no contm mais asseres da linguagem de T que esta , T equiconsistente com T, etc.); 7) possibilitar a demonstrao metaterica de resultados de independncia (podemos, por exemplo, mostrar que a hiptese do contnuo ou o axioma da escolha so independentes da teoria axiomtica formalizada dos conjuntos ZF. Isso nos mostra, entre outras coisas, que nossa concepo de conjunto, que a teoria axiomtica ZF explicita, incompleta; o que coloca um problema de natureza filosfica: quais critrios devem nortear uma extenso da teoria, suficiente ao menos para decidir sobre asseres sabidamente independentes?) Propriedades de teorias axiomticas formalizadas 1) consistncia: T uma teoria consistente se no pudermos derivar a partir de T, na lgica subjacente a T, nenhum par de frmulas contraditrias (A e A) da linguagem de T. Ou, equivalentemente, se existe pelo menos uma frmula da linguagem de T que no pode ser derivada de T. De fato: se A e A so derivveis de T, como (A (A B)), B frmula qualquer, uma tautologia, i.e. uma frmula verdadeira em toda interpretao da linguagem, para toda valorao, sendo por isso um axioma lgico, por duas aplicaes de modus ponens derivamos B. A recproca evidente. Se uma teoria tem pelo menos um modelo, ela obviamente consistente (pois, contrariamente, duas frmulas contraditrias teriam que ser verdadeiras nesse modelo); a recproca, porm, nem sempre vale: h teorias consistentes que no tm modelo (por exemplo, como P2 uma teoria sintaticamente incompleta, existe uma sentena A tal que as teorias P2 + A e P2 + A so ambas consistentes, mas como todos os modelos de P2 satisfazem exatamente as mesmas sentenas, pois P2 uma teoria categrica, uma delas no pode ter modelo, vide abaixo). No entanto, se T uma teoria consistente de primeira ordem, ento T tem necessariamente um modelo (isso uma consequncia da completude da lgica de primeira ordem, segundo o qual toda frmula vlida de uma linguagem de primeira ordem frmula verdadeira em toda interpretao da linguagem, para

13

toda valorao de variveis pode ser demonstrada em lgica de primeira ordem. A lgica de segunda ordem, por outro lado, no completa). 2) categoricidade: T uma teoria categrica se todos os modelos de T so isomorfos. Por exemplo, a teoria cujo nico axioma xy(x=y) categrica; seus modelos so os conjuntos unitrios, todos isomorfos entre si (nesta linguagem desprovida de smbolos nolgicos isomorfia significa simplesmente equinumerosidade, i.e. o mesmo nmero de elementos). Categoricidade uma condio que a maior parte das teorias no satisfaz (o teorema de Loweinheim-Skolem, por exemplo, diz que teorias de primeira ordem que s admitem modelos infinitos tem modelos com qualquer cardinalidade infinita). Por isso, uma condio mais razovel a de categoricidade em determinada potncia: se um nmero cardinal qualquer, T -categrica se todos os modelos de cardinalidade so isomorfos. Por exemplo, a teoria de primeira ordem cujos modelos so as ordens lineares densas sem pontos extremos (essa teoria finitamente axiomatizada) 0-categrica (i.e. categrica em cardinalidade enumervel): todo os seus modelos enumerveis so isomorfos ao conjunto ordenado dos nmeros racionais; mas a teoria admite tambm modelos no enumerveis, por exemplo, o conjunto ordenado dos nmeros reais. A teoria cujos modelos so os corpos algebricamente fechados de caracterstica 0 (demonstravelmente no-finitamente axiomatizvel) 1-categrica (i.e. categrica na cardinalidade do contnuo na verdade a cardinalidade do contnuo 20, mas admitamos a hiptese do contnuo, segundo a qual 20 = 1, sendo 1 o menor cardinal maior que 0 essa hiptese independente da teoria axiomtica dos conjuntos ZFC; i.e. nem ela, nem a sua negao podem ser demonstradas nessa teoria). A teoria dos corpos algebricamente fechados de caracterstica 0, no entanto, admite modelos enumerveis (por exemplo, o fecho algbrico do corpo dos nmeros racionais). H um teorema (Morley) que afirma que se uma teoria de primeira ordem categrica em um cardinal no-enumervel, ela categrica em todos os cardinais noenumerveis. 3) completude: h vrias noes de completude: a) T semanticamente completa se no existe uma sentena da linguagem de T verdadeira em um modelo de T e falsa em outro; b) T sintaticamente completa se para qualquer sentena da linguagem de T, ou demonstrvel a partir de T; c) T completa com relao a um modelo A de T se toda sentena verdadeira nesse modelo (mas no necessariamente em todos os modelos) derivvel a partir de T. Relaes entre essas noes depende de propriedades da lgica subjacente a T. Por exemplo, se essa lgica, como a lgica subjacente s teorias de primeira ordem, completa,

isto , se as asseres verdadeiras em todos os modelos de T so derivveis a partir de T, ento, se T semanticamente completa, ela tambm sintaticamente completa (a recproca incondicionalmente verdadeira). H, no entanto, teorias semntica, mas no sintaticamente completas (por exemplo, a aritmtica de Peano de segunda ordem, vide abaixo). Se a teoria T for sintaticamente completa, ela ser completa com relao a qualquer modelo A de T. De fato, dada uma sentena da linguagem de T verdadeira em A, como T sintaticamente completa, T | ou T | ; se T | ento deve ser verdadeira em todo modelo de T, A em particular; uma contradio, pois, nesse caso, seria falsa em A. Reciprocamente, se T for completa com relao a A, T ser tambm sintaticamente completa. Realmente, seja uma sentena qualquer, uma das duas, ou , verdadeira em A; como T completa com relao a A, T | ou T | ; isto , T sintaticamente completa. Em suma, as noes de completude sinttica e completude com relao a um modelo so equivalentes, mas ambas so mais fortes que a noo de completude semntica. Note que se uma sentena da linguagem de uma teoria de primeira ordem T for verdadeira em todos os modelos de T, ento, pela completude da lgica de primeira ordem, ela ser um teorema de T; mas podem existir sentenas verdadeiras em alguns modelos de T no em todos que no so teoremas, caso T no seja (sintaticamente, ou, pelo menos, semanticamente) completa. Por exemplo, a sentena xy(xy = yx), onde um smbolo de funo binria, verdadeira em alguns modelos da teoria dos grupos (os grupos abelianos) e falsa em outros; ou seja, a teoria dos grupos (axiomas: 1) xyz((xy)z = x(yz)); 2) x(x0 = x 0x = x) e 3) x(xx-1 = 0 x-1x = 0), onde 0 um smbolo de constante e completa. 4) decidibilidade: T uma teoria decidivel se o conjunto das consequncias, ou teoremas de T CnT um conjunto decidivel. Isto , existe um algoritmo que decide se uma qualquer sentena da linguagem de T um teorema da teoria. Infeliz ou felizmente as teorias matemticas mais importantes, como a aritmtica de Peano, no so decidiveis. Em princpio teorias decidiveis, como a geometria euclidiana, podem ser desenvolvidas por computadores.-1

um smbolo de funo unria) no

Alguns fatos importantes: F1) Teste de Los-Vaught: Seja T uma teoria de primeira ordem expressa numa linguagem enumervel. Suponha que T no tem modelos finitos. Se T -categrica para algum cardinal

15

infinito ( 0), ento T completa (lembre-se que em primeira ordem completude sinttica e semntica so conceitos equivalentes). F2) Se T axiomatizvel e sintaticamente completa, ento T decidivel. Exemplos de teorias axiomticas formalizadas I) Aritmtica elementar: Considere a estrutura algbrica N = (N; 0, S,