A brincadeira do Marcelo mostra que não expliquei tudo sobre o algoritmo de Kunen. Mea culpa. Vai aqui, então.
- Pode-se provar a consistência de PA? Sim. Você parte dos axiomas de PA e, numa etapa crucial, introduz uma indução transfinita a \epsilon_0, como um axioma extra. Daí sai Consis PA. (Há outros modos de fazê-lo.) - Kunen mostra como provar Paris-Harrington. Parte dos axiomas de PA, usa num determinado momento a indução transfinita, e prova PH. Como PA prova PH ---> Consis PA, tira-se por modus ponens Consis PA. - A indução transfinita é a coisa. Fazê-la envolve o uso de um ordinal construtivo simples. A operação em causa é recursiva. Pode-se então mecanizar tudo. Qual o galho? PA não prova que este algoritmo converge adequadamente. ``Do lado de fora,'' meta, a gente vê que há a convergência, mas PA não consegue fazê-lo. 2009/7/13 Francisco Antonio Doria <[email protected]> > No comment :)) > > 2009/7/13 Marcelo Finger <[email protected]> > > Dória. >> >> 2009/7/13 Francisco Antonio Doria <[email protected]> >> >>> A gente tem que tomar muito cuidado com esses resultados de >>> indecidibilidade e incompletude, porque frequentemente seu alcance é >>> exagerado ou confundido. Por exemplo: o segundo teorema de incompletude de >>> Gödel diz que (slight handwaving...) se PA é consistente, então a sentença >>> de Gödel que diz da sua consistência não pode nem ser provada nem >>> desprovada. >>> >>> Ora, em 1995 Ken Kunen publicou um algoritmo que, trivialmente, prova >>> Consis PA. Vou repetir: ***Um algoritmo que prova Consis PA***. Como pode? >> >> >> Em Java ficaria assim: >> >> public static main( String []args) { >> System.out.println("A Aritmética de Peano é decidível?"); >> System.out.println("Sim"); >> } >> >> :-)))) >> >> >>> Outra coisa: é trivial (menos, menos, mas quase...) mostrar que, dado um >>> conjunto finito de instâncias sendo investigadas para o Problema da Parada, >>> ***existe*** um algoritmo que as decide. (Ênfase no ***existe***.) >> >> >> Uéu. Aqui v precisa ordernar os N algoritmos na mão, dar para alguém >> mostrar se eles páram ou não e criar um vetor de N posições chamado de >> VEREDITO. Então, v faz um algoritmo assim: >> >> Entrada: TEXT: string contendo um dos N algoritmos contemplados >> Saída: veredito >> >> if( TEXT.equals(algo0) ) >> System.out.println( VEREDITO[0]); >> else if( TEXT.equals(algo1) ) >> System.out.println( VEREDITO[1]); >> >> etc; >> >> Fácil, né! >> >>> >>> >>> Mais complicado (mas factível) é explicitar tal (tais) algoritmo(s). >>> >> >> Feito! >> >> ;-))))) >>> >> >> >> >> -- >> 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
