Caros João Marcos e Hermógenes. Muito obrigado pela clarificação. O que o Hermógenes aponta vai na direção de elucidar as diferenças. A prova de [Turing 1936] sobre a existência de nũmeros não computáveis, esboçada pelo João, realmente demonstra que "Nem todo número real é computável".
Em lógica clássica, isso equivale a existência de números-não computáveis, mas em lógica intuicionista essa equivalência não vale. E isso independe de qual vertente do intuicionismo está se falando. Portanto a existência de números não computáveis não é um teorema intuicionista, só deve (pode?) ser um teorema o fato de que nem todo número real é computável, uma vez que não se pode apresentar recursivamente um tal número. []s Marcelo 2016-10-12 8:32 GMT-03:00 Hermógenes Oliveira < hermogenes.olive...@student.uni-tuebingen.de>: > Marcelo Finger <marcelo.fin...@gmail.com> escreveu: > > > Como seria uma prova construtiva do resultado de Turing sobre a > > existência de números (reais) não computáveis? > > > > A prova clássica é fortemente não construtiva e não apresenta um tal > > número. E nem poderia apresentar pois se houvesse um algoritmo que o > > gerasse, o número seria construtivo. > > > > Mas uma prova construtiva deveria apresentar um tal número. Mas como? > > Fico com a impressão de que este resultado não é provável na lógica > > intuicionista. > > Superficialmente, isto é, no âmbito puramente lógico, a demonstração > intuicionista mostraria que nem todos os números reais são computáveis > (¬∀x C(x), x ∈ ℝ) o que, intuicionisticamente, *não* é equivalente a > mostrar que existem números reais não computáveis (∃x ¬C(x), x ∈ ℝ). > > No âmbito matemático mais fino, contudo, deve-se atentar ainda para a > presença de noções baseadas em definições intuicionisticamente > inadimissíveis. Assim, a noção de número real intuicionista não > coincide com a noção de número real clássica, na medida em que podem > haver definições e especificações clássicas de números reais que não são > admissíveis para um intuicionista. De fato, é na análise real que as > peculiaridades da matemática intuicionista se revelam com maior vigor. > > Porém, eu suspeito que a noção *clássica* de número real não seja > essencial ao argumento de Turing. Não sei exatamente a qual trabalho de > Turing você se refere, mas presumo que esteja se referindo ao artigo > clássico de 1936. Ali, se não me falha a memória, Turing mostra que as > sequências e números computáveis são enumeráveis. Bem, como os números > reais não são enumeráveis, segue que nem todos os números reais são > computáveis, isto é, classicamente, existem números reais não > computáveis. Do ponto de vista intuicionista, a última parte, incluindo > o apelo ao resultado de Cantor sobre a não enumerabilidade dos números > reais, *pode* ser problemática. Mas o argumento de Turing que mostra a > enumerabilidade dos números computáveis me parece em ordem. > > Ademais, intuicionistas normalmente não possuem reservas quanto à > argumentos diagonais. Porém, como lembrou o João Marcos, sentimentos > podem variar dentro da grande família construtivista: finitistas, > predicativistas e etc. podem ter lá suas desconfianças. > > -- > Hermógenes Oliveira > > -- > Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" > dos Grupos do Google. > Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie > um e-mail para logica-l+unsubscr...@dimap.ufrn.br. > Para postar neste grupo, envie um e-mail para logica-l@dimap.ufrn.br. > Visite este grupo em https://groups.google.com/a/ > dimap.ufrn.br/group/logica-l/. > Para ver esta discussão na web, acesse https://groups.google.com/a/ > dimap.ufrn.br/d/msgid/logica-l/878tttn6oy.fsf%40camelot.oliveira. > -- Marcelo Finger Departament of Computer Science, IME University of Sao Paulo http://www.ime.usp.br/~mfinger -- Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos Grupos do Google. Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+unsubscr...@dimap.ufrn.br. Para postar neste grupo, envie um e-mail para logica-l@dimap.ufrn.br. Visite este grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/. Para ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CABqmzx2X2fovqdcck-rgWAaP6oZX9y74BPn%2BQNBemCqk2pMvUQ%40mail.gmail.com.
