Você não prova em PA que o algoritmo converge. Mas numa teoria com uma sentença verdadeira ∏2 adequada a mais, fica fácil. Basta, p.e., supor que a sentença ``F_\epsilon_0 é total'' é um novo axioma. Esta sentença é equivalente a PH, e implica (estritamente!) Consis PA.
No algoritmo dá pra ver exatinho onde PA falha, e onde está a ``inducão transfinita'' - na verdade, finitista, mas... 2009/8/7 Carlos Gonzalez <[email protected]> > O artigo de Kunen me parece bem interessante, sobre tudo a verificação > de enunciados combinatórios usando demonstradores de teoremas (mas com > um humano por perto, para o demonstrador não se perder). > > Entretanto, eu gostaria de ouvir opiniões do pessoal da lista sobre a > novidade lógica e filosófica do resultado. Porque o demonstrador > permite definir funções por recursão em \epsilon_0 . Por exemplo, > gostaria de saber se alguem acha que tem alguma diferença essencial > com a velha prova de consistência de Gentzen usando recursões sobre > esse ordinal. > > Kunen oferece mais uma prova de Paris-Harrington usando recursão > \epsilon_0 (de maneira essencial, pois Paris-Harrington no pode ser > provado em PA, se PA for consistente). Mas, qual é a importãncia do > trabalho de Kunen para os fundamentos da matemática? > > (Estou chamando de "Paris-Harrington" ao enunciado aritmético > combinatório que aparece no artigo deles no Handbook of Mathematical > Logic, que é uma versão finita do Teorema de Ramsey) > > ------------------------------------------------ > Do artigo de Kunen (citações curtas) > ----------------------------------------------- > > We use the Boyer-Moore Prover, Nqthm, to verify the Paris-Harrington > version of Ramsey's Theorem. The proof we verify is a modification of > the one given by Ketonen and Solovay. The Theorem is not provable in > Peano Arithmetic, and one key step in the proof requires \epsilon_0 > induction. > (...) > The Boyer-Moore theorem prover, Nqthm, is a Lisp-based system for > computational logic. It allows the user to define functions > recursively and to prove theorems about these functions. It is, to > first approximation, an implementation of PRA, but it extends PRA in > two important ways. > (...) > The second way is essential Nqthm allows definition of functions by > recursion on the ordinal \epsilon_0, and proofs by induction on > \epsilon_0 . Until now, the full strength of this extension has not > been utilized. In this paper, we show how to utilize it. > (...) > Conclusion. This work demonstrates that one may use Nqthm to verify > some rather complex combinatorial statements. It also demonstrates one > of the dificulies in doing so. Human mathematicians recognize > immediately when various representations of a concepts are essentially > the "same". > (...) > We also recognize, by experience, that these identifications are only > correct in certain contexts but it is not trivial to explain formally > what these contexts are. Thus, making use of these identifications is > a difficult challenge for future generations of verification systems. > > Carlos > > 2009/8/7 Marcelo Finger <[email protected]>: > > Então este algoritmo tem de deixar alguns casos de fora. > > > > 2009/8/7 Francisco Antonio Doria <[email protected]> > >> > >> O algoritmo, caso a caso, não. E' algoritmo mesmo. > >> > >> 2009/8/7 Marcelo Finger <[email protected]> > >>> > >>>> Provar que existe um algoritmo para o prblema da parada é simples; > >>>> descrevê-lo, complicado paca. > >>> > >>> ESte algoritmo tem que usar alguma chamada a um procedimento > indecidível. > >>> > >>> []s > >>> > >>>> > >>>> 2009/8/7 Francisco Antonio Doria <[email protected]> > >>>>> > >>>>> Continuando encurtado porque ficou muito grande: > >>>>> > >>>>> ------------------------------- > >>>>> > >>>>> Três coisas: > >>>>> > >>>>> - Tem provas muito simples (usando sentenças ∏2) para incompletude. > >>>>> > >>>>> - Tem algoritmos fáceis de implementar que provam a consistência de > PA. > >>>>> > >>>>> - Existe um algoritmo (complicado) para resolver o problema da > parada. > >>>>> > >>>>> Como é que vocês me explicam isso? > >>>> > >>>> > >>>> _______________________________________________ > >>>> Logica-l mailing list > >>>> [email protected] > >>>> http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l > >>>> > >>> > >>> > >>> > >>> -- > >>> Marcelo Finger > >>> Departamento de Ciencia da Computacao > >>> Instituto de Matematica e Estatistica > >>> Universidade de Sao Paulo > >>> Rua do Matao, 1010 > >>> 05508-090 Sao Paulo, SP Brazil > >>> Tel: +55 11 3091-9688, 3091-6135, 3091-6134 (fax) > >>> http://www.ime.usp.br/~mfinger <http://www.ime.usp.br/%7Emfinger> > >>> > >> > > > > > > > > -- > > Marcelo Finger > > Departamento de Ciencia da Computacao > > Instituto de Matematica e Estatistica > > Universidade de Sao Paulo > > Rua do Matao, 1010 > > 05508-090 Sao Paulo, SP Brazil > > Tel: +55 11 3091-9688, 3091-6135, 3091-6134 (fax) > > http://www.ime.usp.br/~mfinger <http://www.ime.usp.br/%7Emfinger> > > > > > > _______________________________________________ > > Logica-l mailing list > > [email protected] > > http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l > > > > >
_______________________________________________ Logica-l mailing list [email protected] http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
