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