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 >>> >> > > > > -- > 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 > > > _______________________________________________ > 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
