Five stages of accepting constructive mathematics (Andrej Bauer)
18 views
Skip to first unread message
Joao Marcos
Oct 11, 2016, 3:40:56 PM10/11/16
to Lista acadêmica brasileira dos profissionais e estudantes da área de LOGICA
You've seen the video, now you can read the paper:
"On the odd day, a mathematician might wonder what constructive
mathematics is all about. They may have heard arguments in favor of
constructivism but are not at all convinced by them, and in any case
they may care little about philosophy. A typical introductory text
about constructivism spends a great deal of time explaining the
principles and contains only trivial mathematics, while advanced
constructive texts are impenetrable, like all unfamiliar mathematics.
How then can a mathematician find out what constructive mathematics
feels like? What new and relevant ideas does constructive mathematics
have to offer, if any? I shall attempt to answer these questions."
http://math.andrej.com/2016/10/10/five-stages-of-accepting-constructive-mathematics/
"On the odd day, a mathematician might wonder what constructive
mathematics is all about. They may have heard arguments in favor of
constructivism but are not at all convinced by them, and in any case
they may care little about philosophy. A typical introductory text
about constructivism spends a great deal of time explaining the
principles and contains only trivial mathematics, while advanced
constructive texts are impenetrable, like all unfamiliar mathematics.
How then can a mathematician find out what constructive mathematics
feels like? What new and relevant ideas does constructive mathematics
have to offer, if any? I shall attempt to answer these questions."
http://math.andrej.com/2016/10/10/five-stages-of-accepting-constructive-mathematics/
Marcelo Finger
Oct 11, 2016, 6:36:08 PM10/11/16
to logi...@dimap.ufrn.br
Como seria uma prova construtiva do resultado de Turing sobre a existência de números (rrais) não compatí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.
Se alguém puder me esclarecer, agradeço.
[]s
--
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+unsubscribe@dimap.ufrn.br.
Para postar neste grupo, envie um e-mail para logi...@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/CAO6j_LhejdBgPtY%2BCc6Gd2s72xqVKOG5K4Nae0Rnuv3oDLapew%40mail.gmail.com.
Marcelo Finger
Oct 11, 2016, 6:40:16 PM10/11/16
to logi...@dimap.ufrn.br
Quis dizer: número real não computável.
Em 11 de out de 2016 19:36, "Marcelo Finger" <marcelo...@gmail.com> escreveu:
Como seria uma prova construtiva do resultado de Turing sobre a existência de números (rrais) não compatí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.
Se alguém puder me esclarecer, agradeço.
[]s
Em 11 de out de 2016 16:47, "Joao Marcos" <boto...@gmail.com> escreveu:
You've seen the video, now you can read the paper:
"On the odd day, a mathematician might wonder what constructive
mathematics is all about. They may have heard arguments in favor of
constructivism but are not at all convinced by them, and in any case
they may care little about philosophy. A typical introductory text
about constructivism spends a great deal of time explaining the
principles and contains only trivial mathematics, while advanced
constructive texts are impenetrable, like all unfamiliar mathematics.
How then can a mathematician find out what constructive mathematics
feels like? What new and relevant ideas does constructive mathematics
have to offer, if any? I shall attempt to answer these questions."
http://math.andrej.com/2016/10/10/five-stages-of-accepting-constructive-mathematics/
--
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+u...@dimap.ufrn.br.
Joao Marcos
Oct 12, 2016, 4:45:05 AM10/12/16
to Lista acadêmica brasileira dos profissionais e estudantes da área de LOGICA
> Como seria uma prova construtiva do resultado de Turing sobre a existência
> de números (reais) não computáveis?
Há de fato pelo menos uma seita do construtivismo que rejeita
inteiramente a "existência" de números não-computáveis...
Em abordagens construtivistas mais brandas, contudo, talvez possamos
nos safar simplesmente com um argumento de cardinalidade? Há
demonstrações construtivas bem conhecidas de que os números reais não
são contáveis. Supondo, além disso, que a contabilidade dos números
computáveis possa ser estabelecida intuicionisticamente (bastaria
enumerar "alfabeticamente" todas as máquinas de Turing?), então temos
aí um buraco onde viveriam os reais não-computáveis.
Que tal?
Joao Marcos
--
http://sequiturquodlibet.googlepages.com/
Hermógenes Oliveira
Oct 12, 2016, 7:32:48 AM10/12/16
to logi...@dimap.ufrn.br
Marcelo Finger <marcelo...@gmail.com> escreveu:
> Como seria uma prova construtiva do resultado de Turing sobre a
> existência de números (reais) não computáveis?
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
> Como seria uma prova construtiva do resultado de Turing sobre a
>
> 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
> 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.
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
Marcelo Finger
Oct 13, 2016, 7:44:11 AM10/13/16
to logi...@dimap.ufrn.br
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
--
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+unsubscribe@dimap.ufrn.br.
Para postar neste grupo, envie um e-mail para logi...@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
Departament of Computer Science, IME
University of Sao Paulo
http://www.ime.usp.br/~mfinger
Reply all
Reply to author
Forward
0 new messages