Olá Doria e Marcelo. 2009/7/13 Francisco Antonio Doria <[email protected]>
> 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.) Parece haver uma explicação simples para isso. Desde que haja uma demonstração em uma teoria (recursivamente) axiomatizada, então existe uma máquina que pode realizá-la, o que está relacionado à visão de que as teorias formais são como máquinas de demonstrar teoremas. > > - 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. Fazendo uma digressão: se somos máquinas e vemos que a Aritmética (por exemplo, PA) é consistente, será que é porque temos a indução transfinita em nossa programação. :)) Abraços, Ricardo. > > 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 > > -- Dr. Ricardo Pereira Tassinari - Departamento de Filosofia UNESP - Faculdade de Filosofia e Ciências - Marília Homepage: http://www.marilia.unesp.br/ricardotassinari
_______________________________________________ Logica-l mailing list [email protected] http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
