Re: [Logica-l] O Guinness assume a Hipótese do Contínuo (e o Axioma da Escolha)

[Marcelo Finger]

O Guinness Book of Records possui uma reputação muito maior do que aquela
que seria compatível com os seus atos.  Ele recebe substancial apoio de
diversas ditaduras que gostam de figurar em seus anais, com
valorosos récordes como as que envolvem manifestação de ciclistas (no caso,
em favor do chefe supremo do Turcomenistão).

Veja o episódio do John Oliver sobre o tal líder (Gurbengully
Burdymohamadoff, em grafia minha) e tenha um dia repleto de risadas.

Feliz 2020!

[]s

PS: E se v gosta do John Oliver, não perca o Episódio com o musical  "Eat
shit, Bob"!

Em sáb., 21 de dez. de 2019 às 07:35, Joao Marcos 
escreveu:

> Smallest infinite number
>
> https://www.guinnessworldrecords.com/world-records/smallest-infinite-number/
>
>
> JM
>
> --
> Você recebeu essa mensagem porque está inscrito 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 ver essa discussão na Web, acesse
> https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAO6j_LjbbCpyUxZM%2Bd%3DhZT2_skKxLPjHW3tdA%2B9q-f_NV%2B4kXg%40mail.gmail.com
> 
> .
>


-- 
 Marcelo Finger
 Departament of Computer Science, IME
 University of Sao Paulo
 http://www.ime.usp.br/~mfinger
 ORCID: https://orcid.org/-0002-1391-1175
 ResearcherID: A-4670-2009

-- 
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 ver esta discussão na web, acesse 
https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAGG7Aw385c18-wPGAm%3DTUiHtTcqUYfa-v%3DMJhgoskbfQzYogdw%40mail.gmail.com.

Re: [Logica-l] Kurt Gödel and the mechanization of mathematics

[Hermógenes Oliveira]

Olá, pessoal.

Carlos Gonzalez  escreveu:

> Más o artigo é muito ruim, um lixo.
> 
> [...]
>
> Mas acho que os mal-entendidos dessa senhora são tão básicos que
> dificilmente seja interessante continuar discutindo esse artigo.
>
> Com relação à senhora Juliette Kennedy, talvez seja conveniente
> pensar seriamente em abandonar a filosofia da matemática.
>
> [...]
>
> Não sei, gostaria de ver a posição dos colegas e que me falem se
> estou exagerando.

Quem acompanha a lista, sabe que eu sou bastante crítico de peças de
divulgação científica[1][2].  Mas nunca sugeri que a publicação de
tais peças fossem motivo para que os(as) autores(as) abandonassem suas
áreas de investigação ou suas profissões.  Afinal, para ficar apenas
nos casos mencionados nesta mensagem, tanto os professores Lynch e
Floridi quanto a professora Kennedy possuem artigos propriamente
acadêmicos, com todo o rigor e citações bonitinhas que isso acarreta.

Nessa parte, Carlos, se me permite ser sincero, acho que você exagerou
um pouco.  O teor do resto de suas críticas, contudo, me parecem
razoáveis e ecoam, num certo sentido, as minhas próprias desconfianças
com peças de divulgação.  Reconheço, porém, que muitos desses
problemas são devidos a limitações dos veículos de publicação e uma
série de pressupostos que normalmente se faz sobre o público alvo
delas (pressupostos esses que, quando não menosprezam abertamente a
capacidade do leitor, acabam se mostrando, pelo menos, um tanto
paternalistas).  Devo dizer, no entanto, que as objeções que faria à
peça de Kennedy seriam certamente menos contundentes do que aquelas
que fiz à peça do Lynch referenciada abaixo, por exemplo.

Dito isso, devo admitir que, com relação à minha participação nesta
discussão até aqui, eu havia me limitado à questão proposta por João
Marcos sobre a possibilidade de se dispensar a "aritmetização" na
*demonstração* do resultado gödeliano e me propus o papel de advogado
do diabo com respeito a essa questão apenas.  Nunca houve, da minha
parte, a intenção de vindicar a peça de Kennedy como um todo.

E, a propósito...

Rodrigo Freire  escreveu:

> O teorema como apresentado abstratamente no clássico TMR não tem a
> alegada hipótese existencial que esconde uma construção. Eles
> demonstram que para *qualquer* nomeação das fórmulas, ou falha a
> representabilidade da diagonalização ou falha a representabilidade
> da teoremicidade. Qual vai falhar, depende da nomeação, como mostrei
> aqui. Não é questão de concordar, só de entender o enunciado. Não há
> uso de codificação na demonstração.

A julgar pelo que o Rodrigo escreveu acima, talvez ainda convenha
destilar algumas minúcias.

Cabe esclarecer que a minha alegação sobre uma "aritmetização"
escondida numa hipótese existencial não diz respeito estritamente ao
resultado abstrato em TMR ou na sua demonstração (e isso já estava
explícito nas minhas mensagens anteriores). Para benefício da
discussão, talvez seja proveitoso listar aqui alguns pontos que eu
*não* disputo, e nunca pretendi disputar:

- O enunciado em TMR é um resultado abstrato.  Ele se aplica
  igualmente a qualquer teoria formal T, seja ela decidível ou
  indecidível.

- A demonstração *do resultado abstrato* em TMR não *depende*,
  explícita ou implicitamente, de qualquer "aritmetização" ou
  "codificação".

Ora, do que se trata então a minha alegação de que haveria uma
"aritmetização" sendo pressuposta em TMR?  Bem, tentarei reconstruir o
argumento de maneira mais detalhada abaixo.

Como o Rodrigo explicou, o resultado de TMR nos apresenta com uma
dicotomia: uma teoria T qualquer, ou bem não é diagonalizável ou bem é
indecidível.  Porém, eis uma tese que eu, de fato, disputo: 

- O resultado abstrato de TMR é equivalente ao resultado original de
  Gödel, o implica, ou pode, de alguma forma, substituí-lo.

Ora, quais seriam as minhas razões para isso?

Ao considerarmos teorias formais *particulares*, o resultado abstrato
não fornece, *por si só*, uma demonstração de (in)decidibilidade (ou,
alternativamente falha/sucesso da diagonalização).  Ele apenas nos
garante a dicotomia (típico matemático clássico, não é mesmo,
Valéria?).  Em contraste, o resultado de Gödel nos fornece, para uma
teoria *particular* que pretende ser uma formalização adequada da
aritmética, que ela é, com efeito, indecidível, resolvendo a dicotomia
para um dos lados.

Como nós poderíamos, contudo, com base no resultado abstrato de TMR,
*demonstrar* o resultado de Gödel para uma formalização particular A da
aritmética?  Seria necessário resolver a dicotomia, a qual, neste
caso, como nós já *sabemos*, mas gostaríamos de *demonstrar*
independentemente de Gödel, pende para um dos lados.  Isto é, seria
necessário demonstrar que a função D de diagonalização é definível em
A. Essa demonstração, juntamente com a dicotomia já demonstrada em
TMR, nos daria então o resultado desejado, que é a indecidibilidade de
A.  Consultando as definições relevantes em TMR, em particular a
definição de "definível", 

Re: [Logica-l] Kurt Gödel and the mechanization of mathematics

[Rodrigo Freire]

Bom esclarecimento do seu entendimento, Hermógenes, mas ainda há pontos que
não estão estritamente corretos.
Por exemplo,


> Como nós poderíamos, contudo, com base no resultado abstrato de TMR,
> *demonstrar* o resultado de Gödel para uma formalização particular A da
> aritmética?  Seria necessário resolver a dicotomia, a qual, neste
> caso, como nós já *sabemos*, mas gostaríamos de *demonstrar*
> independentemente de Gödel, pende para um dos lados.  Isto é, seria
> necessário demonstrar que a função D de diagonalização é definível em
> A. Essa demonstração, juntamente com a dicotomia já demonstrada em
> TMR, nos daria então o resultado desejado, que é a indecidibilidade de
> A.


Na verdade, a diagonalização não é definível (o termo contemporâneo é
representável) em absoluto (independente da nomeação das fórmulas), como já
disse. Isso depende da nomeação das fórmulas. É trivial arrumar uma
nomeação das fórmulas para a qual a diagonalização é definível, e uma para
a qual a diagonalização não é. Apresentei isso. Eis aqui outra nomeação
para a qual a diagonalização é definível:

Nomeie as fórmulas que não são diagonalização com os termos para os números
ímpares. Nomeie as diagonalizações dessas F's com os termos soma 'F' + 'F'.
Nomeie as demais com os termos pares não utilizados. A seguinte fórmula
representa a diagonalização:
(x é par e y = x) ou (x é ímpar e y = x + x).



> Consultando as definições relevantes em TMR, em particular a
> definição de "definível", constatamos que a nossa missão seria
> demonstrar um resultado existencial.  E eis aqui, finalmente, a minha
> alegação:
>
> - Uma *demonstração* de que a função D de diagonalização é definível
>   em A não pode dispensar de aritmetização.
>

O resultado existencial está demonstrado acima em duas linhas usando apenas
a divisão entre pares e ímpares e a soma. TMR + esse resultado nos dá que a
teoremicidade não é representável com essa nomeação. O que faltaria para
concluir que a aritmética é indecidível? Faltaria demonstrar que todas as
propriedades recursivas são representáveis com essa nomeação. Aí sim,
poderíamos discutir se esse tipo de coisa, que aparece pela primeira vez no
artigo do Godel, pode ser demonstrada sem aritmetização. É uma discussão
interessante, podemos aprender algo levando isso para frente.

Em especial, essa alegação *não* pretende ser interpretada das
> seguintes formas:
>
> - Para se compreender o enunciado abstrato de TMR e sua dicotomia
>   subjacente é necessário apelar à aritmetização.
>
> - A noção de "aritmetização", ou "representabilidade da matemática" é
>   uma panaceia que remonta, pelo menos, aos tempos de Pitágoras.
>
> No próprio livro TMR, as demonstrações de indecidibilidade de teorias
> particulares, especialmente no teorema 9, §II, assumem explicitamente
> (nota de rodapé 7, §II) a recursividade da função D, e aqui se aplicam
> as minhas observações anteriores sobre as propostas alternativas nos
> moldes de Kleene.
>
> Em resumo, o enunciado abstrato de TMR nos fornece a dicotomia:
>
> ¬ D (diagonalização) ∨ ¬ T (teoremicidade)
>
> o que, para quem está familiarizado com a lógica proposicional
> clássica, é equivalente a
>
> D → ¬T
>

Certo, inclusive é desse último modo que formulei em meu livro. Mas é
preciso entender que há uma nomeação subjacente à dicotomia, e esta
dicotomia se refere à falha de representabilidade com essa nomeação, para
um lado ou para o outro.


Se o resultado pretendido é, para além da dicotomia abstrata de TMR, a
> indecidibilidade, isto é ¬T,  de uma teoria particular A para a aritmética,
> então, temos ainda que demonstrar D.  Ora, pelas definições em
> TMR, D é um enunciado existencial.  Por isso eu falava de uma hipótese
> existencial embutida.
>

¬T  não é o mesmo que indecidibilidade, é indefinibilidade com a nomeação
subjacente. Isso precisa estar claro, ou o enunciado não será entendido.
Para aplicar o teorema a primeira coisa é apresentar uma nomeação das
fórmulas. Depois podemos mostrar D. Fiz isso acima, trivialmente. Disso não
temos ainda a indecidibilidade, como mencionei, e talvez aqui esteja a sua
alegação:

Alegação do Hermógenes reformulada: A tarefa de (i) apresentar uma nomeação
das fórmulas, (ii) representar a diagonalização com essa nomeação e (iii)
mostrar que todas a propriedades recursivas são representáveis com essa
nomeação para uma teoria T (aritmética? teoria de conjuntos?) não pode ser
totalmente executada sem aritmetização.

Ainda seria preciso esclarecer o que é aritmetização, porque a alegação
acima pode ser verdadeira por definição (de aritmetização)! Mostrei que as
etapas (i) e (ii) podem ser executadas sem aritmetização.



> Está concedido que existem codificações distintas e, porventura,
> melhores do que aquelas utilizadas por Gödel e que, por sua vez, podem
> apelar para as mais variadas propriedades numéricas.  Isso significa
> que qualquer codificação funciona para se aritmetizar a teoria, desde
> a noção de fórmula até a noção de derivação 

Re: [Logica-l] Kurt Gödel and the mechanization of mathematics

[Valeria de Paiva]

Muito obrigada Hermogenes, por explicar de forma racional e embasada os
meus sentimentos de que
> haveria uma  "aritmetização" sendo pressuposta em TMR

obrigada Rodrigo pela clarificacao:
>Alegação do Hermógenes reformulada: A tarefa de (i) apresentar uma
nomeação das fórmulas, (ii) representar a diagonalização com essa nomeação
e (iii) mostrar que todas as propriedades recursivas são representáveis com
essa nomeação para uma teoria T (aritmética? teoria de conjuntos?) não pode
ser totalmente executada sem aritmetização.

Concordo que
>Ainda seria preciso esclarecer o que é aritmetização, porque a alegação
acima pode ser verdadeira por definição (de aritmetização)!
sim, mas isso 'e "bad cheating" e estamos pressupondo que todo mundo quer
ver as coisas da forma mais clara possivel e nao "score points on the pub
discussion".

Tambem acho que a gente precisa pensar um pouco mais sobre o que  significa
"ser representavel" (ou pelo menos eu preciso, pois a nocao que eu
conheco e' limitada a categorias)

De qualquer forma acho que ganhamos um tanto com essa conversa!

 obrigada Joao Marcos pela pergunta na mensagem inicial sobre as
dependencias da prova original do Goedel, que pode ser entendida como uma
questao de "reverse mathematics", que acho que foi a conversa que rolou por
aqui.

e pra terminar numa nota um pouco menos fraternal, tb foi bom ver o que o
Hermogenes estava escrevendo em 2016, pois discordo completamente dele na
tese de  se se deve ou nao
"estimular o interesse por ciência".
 Concordo com o JM que isso 'e nao somente "bonitinho e bacaninha --- e
quiçá até útil", mas acho que e' na verdade essencial no mundo atual.
logicos e matematicos so' existem se a sociedade decide sustenta-los, se a
sociedade nao sabe *pra que* eles existem, eles podem deixar de existir.
Vivemos numa economia de atencao e reputacao, precisamos cuidar da nossa.
e divulgacao cientifica boa e honesta e' dificil pacas! Mas isso 'e um novo
"can of worms", pra  uma outra ocasiao.

abracos logicos,
Valeria

On Sat, Jan 4, 2020 at 8:37 AM Rodrigo Freire  wrote:

>
> Bom esclarecimento do seu entendimento, Hermógenes, mas ainda há pontos
> que não estão estritamente corretos.
> Por exemplo,
>
>
>> Como nós poderíamos, contudo, com base no resultado abstrato de TMR,
>> *demonstrar* o resultado de Gödel para uma formalização particular A da
>> aritmética?  Seria necessário resolver a dicotomia, a qual, neste
>> caso, como nós já *sabemos*, mas gostaríamos de *demonstrar*
>> independentemente de Gödel, pende para um dos lados.  Isto é, seria
>> necessário demonstrar que a função D de diagonalização é definível em
>> A. Essa demonstração, juntamente com a dicotomia já demonstrada em
>> TMR, nos daria então o resultado desejado, que é a indecidibilidade de
>> A.
>
>
> Na verdade, a diagonalização não é definível (o termo contemporâneo é
> representável) em absoluto (independente da nomeação das fórmulas), como já
> disse. Isso depende da nomeação das fórmulas. É trivial arrumar uma
> nomeação das fórmulas para a qual a diagonalização é definível, e uma para
> a qual a diagonalização não é. Apresentei isso. Eis aqui outra nomeação
> para a qual a diagonalização é definível:
>
> Nomeie as fórmulas que não são diagonalização com os termos para os
> números ímpares. Nomeie as diagonalizações dessas F's com os termos soma
> 'F' + 'F'. Nomeie as demais com os termos pares não utilizados. A seguinte
> fórmula representa a diagonalização:
> (x é par e y = x) ou (x é ímpar e y = x + x).
>
>
>
>> Consultando as definições relevantes em TMR, em particular a
>> definição de "definível", constatamos que a nossa missão seria
>> demonstrar um resultado existencial.  E eis aqui, finalmente, a minha
>> alegação:
>>
>> - Uma *demonstração* de que a função D de diagonalização é definível
>>   em A não pode dispensar de aritmetização.
>>
>
> O resultado existencial está demonstrado acima em duas linhas usando
> apenas a divisão entre pares e ímpares e a soma. TMR + esse resultado nos
> dá que a teoremicidade não é representável com essa nomeação. O que
> faltaria para concluir que a aritmética é indecidível? Faltaria demonstrar
> que todas as propriedades recursivas são representáveis com essa nomeação.
> Aí sim, poderíamos discutir se esse tipo de coisa, que aparece pela
> primeira vez no artigo do Godel, pode ser demonstrada sem aritmetização. É
> uma discussão interessante, podemos aprender algo levando isso para frente.
>
> Em especial, essa alegação *não* pretende ser interpretada das
>> seguintes formas:
>>
>> - Para se compreender o enunciado abstrato de TMR e sua dicotomia
>>   subjacente é necessário apelar à aritmetização.
>>
>> - A noção de "aritmetização", ou "representabilidade da matemática" é
>>   uma panaceia que remonta, pelo menos, aos tempos de Pitágoras.
>>
>> No próprio livro TMR, as demonstrações de indecidibilidade de teorias
>> particulares, especialmente no teorema 9, §II, assumem explicitamente
>> (nota de rodapé 7, §II) a