Traduzi e enviei minha questão sobre a "epistemologia intuicionista"
para a lista FOM (http://www.cs.nyu.edu/mailman/listinfo/fom/).
Martin Davis, moderador da lista, consultou o grupo de editores da
lista (William Tait, Harvey Friedman, John Baldwin, Alasdair Urquhart,
Andreas Blass, Steve Simpson), e enviou-me a resposta abaixo, que pode
ser do interesse de quem acompanhou esta discussão aqui na LOGICA-L.

* * *
        
Your message to FOM is being rejected because the example you chose,
Euclid's proof of the infinitude of the primes, is perfectly
acceptable intuitionistically. Below comments by a few of our editors:
1.The proof he sketches is perfectly constructive.
2. [1] is correct. He does need the Lemma that every integer >= 2 is
divisible by some prime. But this has a straightforward constructive
proof.
3. Euclid's argument becomes intuitionistically correct once one
observes that "prime" is decidable, i.e., each positive integer either
is prime or isn't.  (That's provable in Heyting arithmetic.)  I'd
advise Marcos to go back to his intuitionist source and ask whether
she is "unconvinced" by Euclid's proof.  Either Marcos or his source
is overstating intuitionist skepticism.  (It would be different for an
ultra-intuitionist, who wouldn't accept the product p_1 * p_2 * ... *
p_n. But ultra-intuitionists are hard to find, and discussing
finiteness with them is even harder.)

* * *

Atenciosamente,
Joao Marcos

2008/10/4 Joao Marcos <[EMAIL PROTECTED]>:
>> > Um intuicionista não se "convence", a partir da demonstração acima, de
>> > que há infinitos primos.  No entanto, qualquer intuicionista
>> > minimamente educado seria capaz de propor um algoritmo que comece de
>> > um número primo qualquer e "saia à caça" do próximo número primo e que
>> > irá, "surpreendentemente", encontrá-lo sempre em tempo finito (afinal,
>> > a demonstração acima "nos" garante que existe um primo entre os
>> > números p_n e P-1).
>>
>> Sem falsa modéstia, suponho-me um intuicionista até que bem educado :)
>> Não vejo nenhum problema com a prova de Euclides, nem me "surpreendo"
>> pelo fato dela fornecer um algoritmo para achar um primo maior que um
>> outro dado.
>
> Aí é que está.  A demonstração que eu apresentei NÃO fornece um
> algoritmo, mas apenas um intervalo finito onde você poderá buscar o
> próximo primo, com o seu algoritmo preferido.  Como resultado, a
> asserção resultante sobre a existência do "próximo primo" é
> existencial, ou, se você preferir, uma disjunção sobre um conjunto
> finito de opções...
>
>> É exatamente e apenas isso que ela faz. A única coisa que
>> literalmente "não cabe na minha cabeça", por falta de espaço mesmo, é
>> uma infinitude de primos :)
>
> Acho que não me fiz entender bem...  Não tenho nada contra o infinito
> potencial, em oposição ao infinito real (que de fato cabe na cabeça de
> qualquer criança nos nossos dias, pois não temos que nos limitar a
> imaginar apenas coisas que são menores do que a gente).
>
> O problema que eu tentei levantar é o seguinte (pode ser um falso
> problema, mas me deixou intrigado, e ainda não enxerguei bem a saída):
> o lógico clássico não tem problemas com a demonstração "disjuntiva" /
> "existencial" apresentada.  Sabendo como ela funciona, definindo
> intervalos finitos de opções, ele é capaz até de propor um algoritmo
> de busca simples (que também poderia ter sido escrito por um
> intuicionista) para procurar o próximo primo a partir de qualquer
> primo dado, e GRAÇAS à demonstração apresentada anteriormente o lógico
> clássico "sabe" que o seu algoritmo pára para toda entrada.  O lógico
> intuicionista, contudo, NÃO se "convence" em absoluto com a
> demonstração clássica, não-construtiva, e não "sabe" portanto que o
> algoritmo vai parar para toda entrada.  De modo que ele aparentemente
> se surpreende a cada execução do algoritmo e pensa: "que bacana,
> encontrei mais um primo! será que isto vai continuar acontecendo?"  O
> lógico clássico "sabe" que isto vai continuar acontecendo sim (a
> partir da demonstração acima, da qual ele está perfeitamente
> "convencido").
>
> Não nego que possa haver uma OUTRA demonstração da infinidade
> (potencial) dos primos, inteiramente construtiva, que "convença" o
> lógico intuicionista.  A minha questão então é puramente *epistêmica*:
> como é que o intuicionista pode simplesmente ignorar a demonstração
> clássica (pois ele não confia nas regras utilizadas) e insistir que é
> apenas uma grande coincidência o fato de que o algoritmo que ele
> escreveu pára para toda entrada?
>
>> Pense no inferno que seria nossas vidas (dos intuicionistas) se estas
>> coisas nos surpreendessem. Você faz a operação de sucessor e obtém o
>> próximo número natural, maior do que o que tinha antes! Não me
>> surpreende. Você aplica o "algoritmo de Euclides" e obtém o próximo
>> primo, maior do que o que tinha antes! Não me surpreende. Agora, o que
>> me surpreende é que nem eu nem você saibamos qual é a operação de
>> sucessor que nos dá o próximo cardinal infinito maior do que o que
>> "tínhamos antes". Coisa mais estranha essa não? :)
>
> Interessante você falar disso, pois sabemos que o lógico intuicionista
> discorda frontalmente do lógico clássico no que diz respeito ao
> infinito "continuum"...  Na matemática construtiva todas as funções
> totais sobre o "continuum" são contínuas.  Belo, isso, mesmo que algo
> misterioso.
>
> JM

-- 
My homepage:
http://sequiturquodlibet.googlepages.com/
_______________________________________________
Logica-l mailing list
[email protected]
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l

Responder a