Provas como Objetos de Estudo: História, Usos e Abusos Edward Hermann Haeusler Prof. do Departamento de Informática PUC/RJ Panorama da Matemática no Século XIX - Problemas da Física Matemática (Sec. XVIII-XIX): - Equação da Onda - Equação do Calor - Equação de Poisson - Técnicas de Fourier - Séries Infinitas são usadas na solução de Eq. Dif. Parciais - Problemas de Fundamentação: - Séries divergentes x Séries Convergentes - Conceito de infinito não era preciso - Conceito de função não era preciso - O próprio conceito de número real não era preciso. - Definição de convergência não existia Necessidade de teoria mais abrangente e abstrata Prof. Edward Hermann Haeusler TECMF-DI-PUC-Rio Provas como Objetos de Estudo: História, 2 Panorama da Matemática no Século XIX (cont.) Dedekind (1831-1916) Cauchy (1789-1857) Bolzano(1781-1848) Definição de número real. Princípio de definição de funções por indução (recursão primitiva) 1888 Aritmetização da Análise, definição dos conceitos de limite, funções e funções contínuas, convergência de sequências e séries infinitas Riemman(1826-1866) Definição do conceito de integral e Teorema Fundamental do Cálculo. Geometrias Não-Euclidianas Peano (em 1889) Define os axiomas da aritmética Weierstrass (1815-1897) Estabelece critérios para a diferenciação e integração, termo a termo, de séries infinitas Hilbert (em 1898-1899) Estabelece a fundamentação da geometria Prof. Edward Hermann Haeusler TECMF-DI-PUC-Rio Provas como Objetos de Estudo: História, 3 Teoria Ingênua dos Conjuntos Bolzano concebe a noção (abstrata) de conjuntos (finitos e infinitos) Cantor (de 1867 a 1871) define a teoria de conjuntos e prova a existência de conjuntos infinitos com cardinalidades diferentes. Conceitos de números cardinais e ordinais transfinitos. Resistência aos principais resultados. Existência Atual posta em cheque. Os paradoxos: - Burali-Forti (1897) “Não há o ordinal de todos os ordinais” - Russell (1902) “Não há o conjunto de todos os conjuntos” R = { x / x x} Prof. Edward Hermann Haeusler TECMF-DI-PUC-Rio ==> R R se e somente se R R Provas como Objetos de Estudo: História, 4 Evolução da Lógica como assunto matemático DeMorgan (1830) Observa que a álgebra não necessita lidar tão somente com conceitos numéricos. Boole (1854) Descreve uma álgebra a partir de operações entre conjuntos e relações lógicas, confirmando DeMorgan. Frege (1879) estabele a lógica como um sistema formal que tem sua linguagem particular e distinta da natural. O conceito de prova matemática passa a ser formal. Frege (1884) busca a fundamentação da aritmética em bases puramente lógicas , com a adição do conceito de pertinência () como primitivo. ===> paradoxos aparecem novamente !! ===> Paradoxos associados ao axioma da escolha Prof. Edward Hermann Haeusler TECMF-DI-PUC-Rio Provas como Objetos de Estudo: História, 5 As 3 Abordagens para a Fundamentação da Matemática Logicismo (Frege) - Toda a Matemática é consequência de princípios puramente lógicos. Formalismo (Hilbert) - A Matemática é fundamentada por sistemas formais cujo único requisito é a consistência Intuicionismo (Brouwer) - A Matemática é uma atividade humana fundamentada em processos construtivos, sendo assim todo objeto matemático tem sua existência expressa por construção. Prof. Edward Hermann Haeusler TECMF-DI-PUC-Rio Provas como Objetos de Estudo: História, 6 O Programa de Hilbert => Obtenção de uma prova da consistência da matemática, observando-se que: - As teorias mais complexas são extensões das mais simples. Th(N) Th(Z) Th(Q) Th(R) Th(C) - Tais extensões são, na sua maior parte, obtidas por operações básicas (classes de equivalência, completamento por simetria, por compactação, completamento algébrico, etc) => Prova da consistência da Aritmética ( Th(N)) com o uso de técnicas finitárias. => Provar que não existe prova de 0 = 1 usando ............ Prof. Edward Hermann Haeusler TECMF-DI-PUC-Rio Provas como Objetos de Estudo: História, 7 Principais Resultados em Lógica/Metamatemática no início do século XX - Teoria dos Tipos como solução ao paradoxo em Russell - Russell e Whitehead publicam o Principia Mathematica. - Presburger (1929) prova que a aritmética sem a multiplicação é decidível. - Skolem (1931) prova que a aritmética sem a adição e o sucessor é decidível - Herbrand (1931) prova a consistência de um fragmento fraco da aritmética (só o sucessor). -Tarski (1930) Prova que a aritmética com adição (+) e menor (<) é decidível. (1936) Formaliza a semântica adequada para a lógica de primeira ordem (1949) Prova da decidibilidade da Teoria dos Reais - Gödel (1930) prova a completude do cálculo de primeira ordem - Gödel (1931) introduz a idéia de aritmetizar (codificar na forma numérica) a linguagem de um sistema formal de forma que (meta) teoremas do sistema possam ser vistos como teoremas aritméticos e prova seu famoso teorema da incompletude. Obs: # é o código de . - Gödel (1931) prova a não-provabilidade da consistência. Prof. Edward Hermann Haeusler TECMF-DI-PUC-Rio Provas como Objetos de Estudo: História, 8 Paradoxo do mentiroso: “Eu estou mentindo” Os Teoremas de Gödel Lema da diagonal (Gödel/Tarski): T |- diagx1(#,#(#)) se ( Th(N) T) se e somente x1 é a única variável livre em e (t) indica sua substituição por t Seja (x1) uma fórmula com somente x1 livre, então existe tal que T |- (#) Teorema de Tarksi: Não existe uma fórmula Verd(x1) em T capaz de definir a verdade aritmética, isto é, T |- Verd(#) se e somente se é verdadeira na aritmética. Teorema de Gödel: Qualquer axiomatização de Th(N) onde seja possível aritmetizar o conceito de prova é incompleta. Prova: Seja Th(N) e uma fórmula Pr(x,y) tal que |- Pr(#, # ) se e somente se é uma prova com axiomas de . Aplique o lema da diagonal a p Pr(p,x1) Segundo Teorema de Gödel: Seja uma axiomatização como acima, então a fórmula p Pr(p,#(0=1)) é demonstrável a partir de se e somente se Cn() é inconsistente Prof. Edward Hermann Haeusler TECMF-DI-PUC-Rio Provas como Objetos de Estudo: História, 9 Gentzen Prova a Consistência da Aritmética (1936) -Criação de um sistema dedutivo “natural” (com estrutura) com o qual pode-se analisar o papel das constantes lógicas na construção de provas. Comparação entre provas ( 1 2 ). -Definição de um processo efetivo de simplificação de provas (normalização) => Para toda prova de a partir de , obtem-se efetivamente ’ que é (uma) prova mais simples de a partir de ’ . -Em uma prova simples todas as fórmulas são sub-fórmulas ou da conclusão da prova ou de alguma das hipóteses (premissas, ’) da prova . -Mostra-se que não existe prova mais simples de 0=1 Não existe prova de 0=1 Prof. Edward Hermann Haeusler TECMF-DI-PUC-Rio Provas como Objetos de Estudo: História, 10 Lembretes: -A prova original de Gentzen usa Cálculo de Sequentes e prova que a regra do corte é desnecessária na construção de provas em aritmética. Usa indução até 0 para provar terminação do processo de construção da prova quando este for o caso. (Folclore do Haupsatz ou eliminação do corte) - Dedução Natural é apresentada por Gentzen mas, somente após Prawitz (1965) os principais problemas com as regras de absurdo (clássico) são resolvidos e a relação entre Normalização e Eliminação do corte é bem estabelecida. - Curry já havia relacionado combinadores (S, K e I) com sistema axiomático de Heyting (lógica intuicionista), originando o termo Lógica Combinatória. Prof. Edward Hermann Haeusler TECMF-DI-PUC-Rio Provas como Objetos de Estudo: História, 11 Evolução da Teoria da Prova - Análise Ordinal (Schütte - Girard) - Provas como Computações (Curry-Howard) - Teoria de Tipos e Modelos Categóricos para Linguagens - Novas lógicas com semânticas operacionais. - Complexidade Lógica. - Compactação de Provas Prof. Edward Hermann Haeusler TECMF-DI-PUC-Rio Provas como Objetos de Estudo: História, 12 Dedução Natural [ (A (B C)) ] (A (B C)) (A B) (A C) (A B) (A C) (A C) (A (B C)) (A C) [B C] [(A (B C)) ] C [A] (A C) (A C) (A C) (A (B C)) (A C) Prof. Edward Hermann Haeusler TECMF-DI-PUC-Rio Provas como Objetos de Estudo: História, 13 Dedução Natural - Simplificando Provas [(B C)] B [A] (A C) (A B) [A] (A B) [(A (B C))] (A B) (A C) [(B C)] C (A C) (A B) (A C) (A B) (A C) [ (A (B C)) ] (A (B C)) (A B) (A C) (A B) (A C) (A C) (A (B C)) (A C) [B C] [(A (B C)) ] [A] (A C) C (A C) (A C) (A (B C)) (A C) Prof. Edward Hermann Haeusler TECMF-DI-PUC-Rio Provas como Objetos de Estudo: História, 14 Algumas Reduções 1 2 B C (B C) 2 C C 1 A 1 A [A] 2 B [A] 2 B AB B 1 A(a) 1 [A] 2 B 1(a/t) A(t) xAx A(t) Prof. Edward Hermann Haeusler TECMF-DI-PUC-Rio Provas como Objetos de Estudo: História, 15 Princípio da Subfórmula para Provas Normais Eliminações Fórmula mínima introduções Toda fórmula na prova ou é subfórmula de ou é subfórmula de Alguma fórmula de Prof. Edward Hermann Haeusler TECMF-DI-PUC-Rio Provas como Objetos de Estudo: História, 16 Consistência da lógica de primeira ordem Suponha Não existe prova de Prof. Edward Hermann Haeusler TECMF-DI-PUC-Rio , pois Então existe Provas como Objetos de Estudo: História, ’ normal 17 Terminologia e Comentários -Ao processo de “siimplificação” de uma prova dá-se o nome de NORMALIZAÇÃO - NORMALIZAÇÃO = (Estratégia de Apl. de Reduções) + Terminação -Para a lógica de primeira ordem a prova de terminação é feita com indução finita. Normalizando Provas na Aritmética Prof. Edward Hermann Haeusler TECMF-DI-PUC-Rio Provas como Objetos de Estudo: História, 18 A Regra de Indução Finita 0 (0) [(a)] s (suc(a)) x (x) Pode haver normalização para a Aritmética ???? Prof. Edward Hermann Haeusler TECMF-DI-PUC-Rio Provas como Objetos de Estudo: História, 19 O Sistema infinitário PA Regra 0 (0) suc(0) sucn(0) (suc(0)) ………. (sucn(0)) ………. x (x) Prof. Edward Hermann Haeusler TECMF-DI-PUC-Rio Provas como Objetos de Estudo: História, 20 Imergindo provas de PA em PA 0 (0) [(a)] s (suc(a)) x (x) 0 (0) 0 (0) . . . 0 s [(0)] [(sucn-1(0))] s s (suc(0)) ……. (sucn(0)) …. x (x) Reduzindo provas em PA Pode-se estimar o tamanho das provas de PA ??? Prof. Edward Hermann Haeusler TECMF-DI-PUC-Rio Provas como Objetos de Estudo: História, 21 Medindo o tamanho das provas em PA que são imagens de provas em PA finita sem IND k IND não aninhadas ≤ k. < 2 uma IND aninhada < 2 IND aninhadas em quantidade arbitrária < Prof. Edward Hermann Haeusler TECMF-DI-PUC-Rio Provas como Objetos de Estudo: História, 22 Medindo o tamanho das provas em PA em função da regra 0 (0) suc(0) sucn(0) (suc(0)) ………. (sucn(0)) ………. = x (x) - Se k finitos então - Se k = k. então = 2 - Se k = k então - Se k = k então A cota superior é então : Prof. Edward Hermann Haeusler TECMF-DI-PUC-Rio 0 = - vezes Provas como Objetos de Estudo: História, 23 0 (0) suc(0) (suc(0)) …. sucn(0) (sucn(0)) …. x (x) (t) t (t) •Tamanho da prova reduzida não é maior e pode-se considerar uma medida no processo de normalização onde a redução tem complexidade menor Prof. Edward Hermann Haeusler TECMF-DI-PUC-Rio Provas como Objetos de Estudo: História, 24 - Prova-se por indução transfinita até 0 que todas as provas em PA que tem um número finito de fórmulas máximas, são normalizáveis - Não existe prova de 0=1 em PA. - PA é consistente Prof. Edward Hermann Haeusler TECMF-DI-PUC-Rio Provas como Objetos de Estudo: História, 25 Estimando o tamanho de provas Normais Em Dedução Natural Proposicional : . 2. . 2tam() F-Max() - Cota-Superior para provas normais : 2 - Exemplos de teoremas que tem cota-inferior hiperexponencial em provas normais e tem tamanho linear em provas não-normais Ex: Fórmulas de Orekov Em Cálculo de Sequentes Proposicional : - Cota-Superior para provas sem corte : 2F-max().tam() - Exemplos de teoremas que tem cota-inferior exponencial em provas sem corte e tem tamanho linear em provas com corte Ex: Princípio da Casa do Pombo (Haken 1984) Prof. Edward Hermann Haeusler TECMF-DI-PUC-Rio Provas como Objetos de Estudo: História, 26 Sistemas de Frege e Simulação polinomial -Um sistema de Frege é defiinido por conjunto finito de regras e axiomas e é completo e correto (com respeito a LK). Teorema: Dados F1 e F2, sistemas de Frege, toda prova em F1 tem uma prova ’ da mesma fórmula e tam(2) Poli(tam(1)) -Um sistema de Frege com extensão permite o uso da regra de extensão : E Fato : O princípio da casa do Pombo (PHP) possui provas de tamanho polinomial em sistemas de Frege com extensão (Reckow 1987) Fato: PHP possui provas de tamanho polinomial em sistemas de Frege (Buss & Reckow 1988) Prof. Edward Hermann Haeusler TECMF-DI-PUC-Rio Provas como Objetos de Estudo: História, 27 Compactando Provas - Ignorar a estrutura da prova e compactar como um string. - Usar a estrutura da prova e introduzir fórmulas máximas (cortes) => Obtem-se redução do gap exponencial para alguns exemplos => Processo já utilizado por Revezs em 1986 no contexto de L.F. PHP polinomial equivalente ao obtido por Buss. Prova obtida a partir de uma prova normal com introdução de fórmulas máximas e axiomas de extensão gerados pela unificação de fórmulas na prova normal (Gonçalves & Haeusler 2005) - Provas como termos de primeira ordem e compactação via algoritmo de unificação PHP polinomial de mesmo grau obtido por Buss. Prova obtida por unificação de subtermos (subprovas) Dificuldade inerente na compactação de provas !!!!! Prof. Edward Hermann Haeusler TECMF-DI-PUC-Rio Provas como Objetos de Estudo: História, 28 A Ciência da Computação Hoje : NP = P ? (Cook 1971) P : Encontra solução em tempo polinomial NP : Verifica solução em tempo polinomial CoNP : Verifica que não é solução, em tempo polinomial Taut CoNP Sat NP Verificação de Modelos Prova de Teoremas Obs: Se CoNP NP então NP P Prof. Edward Hermann Haeusler TECMF-DI-PUC-Rio Provas como Objetos de Estudo: História, 29 Como SAT é NP-Completo então Taut é CoNP-Completo ===> Se existe um sistema dedutivo onde todas as provas tem tamanho polinomial em função do tamanho da conclusão, então CoNP = NP. Senão existe tal sistema então CoNP NP e portanto NP P. =? => Taut Intuicionista é PSPACE-completo (CoNP PSPACE) => A lógica intuicionista só com a implicação é PSPACE-completa Circuitos booleanos monotônicos e provas em Dedução Natural Razborov 1984 e 1989 indica que o uso de negação é essencial na obtenção do Gap exponencial em circuitos booleanos. Uso de desnormalização como mais uma “heurística” de compactação de provas. Prof. Edward Hermann Haeusler TECMF-DI-PUC-Rio Provas como Objetos de Estudo: História, 30 Teorema do Razborov (1985) Fato: Se L P então existe uma família de circuitos booleanos (Cn)nN e um polinômio p(x) tal que Ln é aceita por Cn e | Cn | p(n). Corolário: Se existe L tal que toda família de circuitos para Ln não é limitada por polinômio então NP P. Teorema (Razborov): Circuitos monotônicos para CLIQUEn,k quando k = 4n tem cota inferior : c8 n O 2 Indício de que NP P ?? Obs: A prova do teorema de Razborov usa a técnica de ultraprodutos introduzida em 1938 por Lós para provar a compacidade da lógica de primeira ordem Prof. Edward Hermann Haeusler TECMF-DI-PUC-Rio Provas como Objetos de Estudo: História, 31 Consistência Def. Uma Teoria é consistente se não sustenta fatos falsos. Def. Uma Teoria é consistente se não prova fatos falsos. Def. Uma Teoria é consistente se não prova todos os fatos. Def. Uma Teoria é consistente se não prova algum absurdo. Prof. Edward Hermann Haeusler TECMF-DI-PUC-Rio Provas como Objetos de Estudo: História, 32 O que são técnicas finitárias ??? (visão a posteriori) - Operações efetivas sobre objetos concretos Objetos concretos: |, ||, |||, ||||, ||||||, .... , , , , ........ Operações efetivas: ???????? juntar símbolos apagar símbolos escrever símbolos reconhecer um símbolo Prof. Edward Hermann Haeusler TECMF-DI-PUC-Rio Provas como Objetos de Estudo: História, 33 Equação da onda u ut(x,0) = g(x) e u(x,0) = f(x) D’Alembert 1747 + Euler 1748 u(x,t) = F(x+ct)+G(x-ct) xt Daniel Bernouli 1753 u(x,t) = 2 0 (sinnysinnxcosnct)f(y)dy + 2 0 (1/n) (sinnysinnxsinnct)g(y)dy Lagrange 1759 Prof. Edward Hermann Haeusler TECMF-DI-PUC-Rio Provas como Objetos de Estudo: História, 34 Equação do calor u(0,t) = u(L,t) = 0 u(x,0) = f(x) L u(x,t) = cne-n2 2Kt/L2 sin(nx/L) n=1 f(x) = cnsin(nx/L) n=1 L cn= (2/L) f(x) sin(nx/L)dx 0 Prof. Edward Hermann Haeusler TECMF-DI-PUC-Rio Fourier 1811 ==> Toda “função” tem expansão em série de senos ????? Dirichlet (1829,1837) + Fund. Análise (Bolzano, Cauchy, Weierstrass) + Riemann (def. integral, 1900’s) Provas como Objetos de Estudo: História, 35 Manipulação com séries infinitas (I) : Resolvendo equações C x+ 3 x=6 =9 1 + aC = C C(1-a) = 1 C = 1/(1-a) Prof. Edward Hermann Haeusler TECMF-DI-PUC-Rio Provas como Objetos de Estudo: História, 36 Diferenciação de uma série (termo a termo) dx Integração de uma série (termo a termo) xd x k 0 k Prof. Edward Hermann Haeusler TECMF-DI-PUC-Rio k x k 1 k Provas como Objetos de Estudo: História, 37 Geometrias Não-Euclidianas Hiperbólica Bolyai-Lobachevsky 1820 Plana Euclides 400’s Elíptica Riemman 1800’s Axiomas de Euclides 1. Para cada par de pontos P1 e P2 com P1 P2 existe uma única reta que incide em ambos. 2. Para todos segmentos AB e CD existe um ponto E t.q. E está entre A e B e CDBE 3. Para todo par de pontos O e A com O A existe um única circ. com centro O e raio OA 4. Todos os ângulos retos são congruentes 5. Dados uma reta R e um ponto A fora desta, existe uma única R’ paralela e R e incidente em A. Prof. Edward Hermann Haeusler TECMF-DI-PUC-Rio Provas como Objetos de Estudo: História, 38 T |- (#) Seja t = #(x2(diagx1(x1,x2) (x2))) então será x2(diagx1(t,x2) (x2))) x2(substx1(t,x2) (x2))) (diagx1(t, #) (#)) T |- diagx1(t, #) (#) diagx1(t,x2) T |- diagx1(t, #) T |- (#) T |- (x2) T |- x2= # T |- diagx1(t,x2) (x2) T |- x2 (diagx1(t,x2) (x2)) Prof. Edward Hermann Haeusler TECMF-DI-PUC-Rio Provas como Objetos de Estudo: História, 39 Não provabilidade da consistência em Cn() ~Pr(#) Cn() [Diag] se Cn() então Pr (#) Cn() Cn() é inconsistente. se Cn() é consistente então Cn(). ~Pr (#) Cn() ~Pr (#(0=1)) Cn() Cn() Portanto se ~Provavel(#(0=1)) Cn() então Cn() é inconsistente Prof. Edward Hermann Haeusler TECMF-DI-PUC-Rio Provas como Objetos de Estudo: História, 40 Intuição do “Mundo Físico” não concorda com o “Mundo Matemático S = Rotação de 1/10 de radiano v C = n(v) n N SC S C -1(v) = Prof. Edward Hermann Haeusler TECMF-DI-PUC-Rio -1 -1(S C) Provas como Objetos de Estudo: História, 41 Paradoxo de Banach-Tarski (1924) e Paradoxo de Hausdorf (1914) Divisão da esfera em 5 partes (uso do axioma da escolha) Rotações e Translações Prof. Edward Hermann Haeusler TECMF-DI-PUC-Rio Provas como Objetos de Estudo: História, 42 Existência de um conjunto sem medida em Rn - Medida como Comprimento, Área ou Volume (desde a Grécia antiga) - Medida associada a integral de Riemman - Medida de Jordan (contempla somente conjuntos limitados) - 1890 - Medida de Lebesque generaliza a de Jordan e contempla conjuntos ilimitados incluindo os Riemman integráveis - 1902 - Vitali usa o axioma da escolha para mostrar a existência de um conjunto sem medida (1905) - Solovay (1960’s) prova que substituindo-se o axioma da escolha pelo axioma da determinância (“Todo jogo infinito tem estratégia vencedora”) tem-se que todo subconjunto do Rn é mensurável. Prof. Edward Hermann Haeusler TECMF-DI-PUC-Rio Provas como Objetos de Estudo: História, 43 N = < N, 0, <, suc, , +, exp > suc(0) + suc(0) = suc(suc(0)) Th(N) xy(suc(x) + y = suc(x + y)) Th(N) xyzn ((n > suc(suc(0))) (exp(x,n)+exp(y,x))exp(z,n)) Th(N) Prof. Edward Hermann Haeusler TECMF-DI-PUC-Rio Provas como Objetos de Estudo: História, 44 Leitura computacional do teorema de Gödel Todas as funções computáveis são representáveis em [N, <, 0, suc, +, *]. Toda computação pode ser expressa em forma de Dedução a partir de um conjunto de axiomas (A) que defina as operações aritméticas básicas. Gödel define o conceito de função primitivamente recursiva e relaciona com aquelas que são representáveis em aritmética. Prof. Edward Hermann Haeusler TECMF-DI-PUC-Rio Provas como Objetos de Estudo: História, 45 · Í Th( [N, <, 0, suc, +, *]) diag é computável. Como A é r.c. então Ded é computável Ded é representável em Cn(A). Qualquer axiomatização r.c. Apara [N, <, 0, suc, +, * ] é incompleta, i.e, Cn() é incompleta. Existem funções não computáveis Prof. Edward Hermann Haeusler TECMF-DI-PUC-Rio Provas como Objetos de Estudo: História, 46 Seja T = fórmulas válidas T ser r.c Cn(T ) é r.c. fórmula repr. f em Cn(TA) função f computável que reconhece Cn(T) Diag. sobre ~ ~(#) Cn(TA) Contradição Prof. Edward Hermann Haeusler TECMF-DI-PUC-Rio Provas como Objetos de Estudo: História, 47