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 _______________________________________________ Logica-l mailing list Logica-l@dimap.ufrn.br http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
