Um teorema bem conhecido de Liouville nos permite enunciar o seguinte: - Existe uma infinidade de reais entre 0 e 1 tais que seus dígitos são descritos recursivamente, mas a sentença ``r é transcendente'' é indecidível em ZFC, se consistente, onde r é um desses reais. (r é transcendente no modelo standard, se ZFC tiver um modelo com aritmética standard, etc)
Esse exemplo é simples, mas posso facilmente generalizá-lo para outros domínios da matemática. 2011/10/2 Valeria de Paiva <valeria.depa...@gmail.com> > aonde esta' o post? > valeria > > 2011/10/2 Francisco Antonio Doria <famado...@gmail.com>: > > Claus, Valeria, vejam o post que acabei de fazer. > > > > 2011/10/1 Francisco Antonio Doria <famado...@gmail.com> > >> > >> Penso nalgo como uma versão fraca da regra omega de Shoenfield. > >> > >> 2011/10/1 Claus Akira Horodynski Matsushigue <claus...@mat.unb.br> > >>> > >>> Caro Dória e demais.... > >>> > >>> Quando se entende porque a Teoria da Computação > >>> não pode ser bem-expressa em sistemas formais > >>> (seja PA, ZFC, ou qualquer outro de Fundamentos), > >>> entende-se imediatamente que um sistema formal > >>> para tal não pode ter provas finitas. Não é uma > >>> questão de gosto ou não. > >>> > >>> > >>> Entretanto, para se propor um sistema formal para > >>> fundamentar a Teoria da Computação (englobando > >>> ou não o restante da Matemática ordinária/mainstream, > >>> este é outro problema!) precisa haver um compromisso > >>> filosófico com os seus fundamentos. Não se pode colocar > >>> uma regra tão forte como o Teorema de Hahn-Banach > >>> ou CH, e.g.. > >>> > >>> > >>> O meu gosto seria continuar mantendo a Metamatemática > >>> na parte finitária da Matemática. Por isso é importante se > >>> analisar o significado de finitário. Finitário **não** é finito. > >>> Na verdade significa só ser permitido/autorizado utilizar > >>> processos finitos (computações!) de construção. > >>> > >>> > >>> Basta perceber que qualquer teoria (razoável) já > >>> é R.E. e não Rec, menos ainda finita, e.g. PA. > >>> > >>> > >>> O que precisamos é a nós ser possível verificar > >>> finitariamente a correteza cada prova de uma > >>> teoria. Ora, em toda prova finita, isso sempre é > >>> possível. Mas não só! Esta é a questão! > >>> > >>> Uma prova é na verdade uma árvore, que hoje em > >>> dia pensamos finita. Verificar a sua correteza é > >>> verificar se a sua relação filiação/paternidade sempre > >>> é condizentes com as regras do sistema formal. > >>> > >>> Entretanto, também podemos pensar (minha > >>> sugestão) em árvores infinitas em largura, com > >>> regras finitárias (mas não finitas), mas todos os > >>> ramos folha-raiz finitos. Ou seja, um nó pode ser > >>> pai de infinitos (enumeráveis) filhos. > >>> > >>> Entretanto, precisamos continuar a verificar a correteza > >>> da prova de forma finita. Então esta prova/árvore > >>> (infinita mas finitária) precisa ser construída por uma > >>> computação não-determinística (leia-se Máquina de > >>> Turing) muito bem comportada. Nós precisamos > >>> programá-la corretamente de modo a construir a árvore > >>> da prova, em que, a cada nível da árvore, a relação > >>> paternidade/filiação da árvore respeite rigorosamente > >>> a uma regra do sistema formal. > >>> > >>> Como verificamos a correteza da prova? Analisando > >>> a Máquina de Turing não-determinística (seu algoritmo) > >>> e provando que ela é correta, ou seja, constroi a árvore > >>> em que a relação paternidade/filiação sempre respeita > >>> uma regra de inferência do sistema. > >>> > >>> Na Teoria da Computação estamos cansado de > >>> demonstrar FINITARIAMENTE a correteza de um algoritmo, > >>> mesmo nos casos em que as possíveis computações são > >>> infinitas (por ser não-deterministica, ou por conta de um > >>> parâmetro de entrada). Note que as possíveis computações > >>> são infinitas, porém toda computação é sempre finita, > >>> representada por um ramo folha-raiz na árvore da prova. > >>> > >>> > >>> A regra de inferência finitária estou chamando de omega-Z > >>> rule. É uma adaptação recursiva da omega regra de Hilbert. > >>> > >>> > >>> Dá para entender? > >>> > >>> Abraços, Claus > >>> > >>> > >>> > >>> > >>> > >>> 2011/10/1 Francisco Antonio Doria <famado...@gmail.com>: > >>> > Tô devendo essa - mais tarde hoje, pode deixar. > >>> > > >>> > 2011/10/1 Valeria de Paiva <valeria.depa...@gmail.com> > >>> > > >>> >> Doria, > >>> >> >muitos fatos simples e intuitivamente claros resultam, na versão > >>> >> > formal, em sentenças indecidíveis. > >>> >> Essa 'e certamente a minha impressao, mas seria bom ter alguma coisa > >>> >> escrita "pra dummies" com o minimo possivel de pre-requisitos > formais, > >>> >> explicando uns tres exemplos do fenomeno. > >>> >> > >>> >> eu nao conheco tres. eu costumava ter dois exemplos de resultados > que > >>> >> nao fazem sentido pra mim, agora so' lembro de um: a complexidade de > >>> >> "typechecking ML programs". > >>> >> > >>> >> Mas eu nao concordo com: > >>> >> >Me parece que a teoria da computação exige algum tipo de regra > >>> >> > infinitária > >>> >> na >sua axiomatização > >>> >> nao me parece que nenhuma regra infinitaria seja necessaria nao. so' > >>> >> mais investigacao de o que 'e usado aonde. > >>> >> > >>> >> Valeria > >>> >> > >>> >> 2011/9/30 Francisco Antonio Doria <famado...@gmail.com>: > >>> >> > Muitos dos problemas que têm sido assinalados nessa discussão > sobre > >>> >> Nelson > >>> >> > resultam de um fato simples: sistemas axiomáticos como os usuais > >>> >> > (consistentes, incluem bastante aritmética, possuem um conjunto > r.e. > >>> >> > de > >>> >> > teoremas, têm por linguagem a lógica clássica) não se prestam à > >>> >> > teoria da > >>> >> > computação: muitos fatos simples e intuitivamente claros resultam, > >>> >> > na > >>> >> versão > >>> >> > formal, em sentenças indecidíveis. Me parece que a teoria da > >>> >> > computação > >>> >> > exige algum tipo de regra infinitária na sua axiomatização, se > >>> >> > desejarmos > >>> >> > que nossas intuições a respeito se reflitam em teoremas da teoria. > >>> >> > > >>> >> > -- > >>> >> > fad > >>> >> > > >>> >> > ahhata alati, awienta Wilushati > >>> >> > _______________________________________________ > >>> >> > Logica-l mailing list > >>> >> > Logica-l@dimap.ufrn.br > >>> >> > http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l > >>> >> > > >>> >> > >>> >> > >>> >> > >>> >> -- > >>> >> Valeria de Paiva > >>> >> http://www.cs.bham.ac.uk/~vdp/ > >>> >> http://valeriadepaiva.org/www/ > >>> >> > >>> > > >>> > > >>> > > >>> > -- > >>> > fad > >>> > > >>> > ahhata alati, awienta Wilushati > >>> > _______________________________________________ > >>> > Logica-l mailing list > >>> > Logica-l@dimap.ufrn.br > >>> > http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l > >>> > > >>> > > >> > >> > >> > >> -- > >> fad > >> > >> ahhata alati, awienta Wilushati > >> > > > > > > > > -- > > fad > > > > ahhata alati, awienta Wilushati > > > > > > > > -- > Valeria de Paiva > http://www.cs.bham.ac.uk/~vdp/ > http://valeriadepaiva.org/www/ > -- fad ahhata alati, awienta Wilushati _______________________________________________ Logica-l mailing list Logica-l@dimap.ufrn.br http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
