Penso nalgo como uma versão fraca da regra omega de Shoenfield. 2011/10/1 Claus Akira Horodynski Matsushigue <[email protected]>
> 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 <[email protected]>: > > Tô devendo essa - mais tarde hoje, pode deixar. > > > > 2011/10/1 Valeria de Paiva <[email protected]> > > > >> 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 <[email protected]>: > >> > 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 > >> > [email protected] > >> > 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 > > [email protected] > > http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l > > > > > -- fad ahhata alati, awienta Wilushati _______________________________________________ Logica-l mailing list [email protected] http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
