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