Kurt Gödel and the mechanization of mathematics

[Joao Marcos]

Kurt Gödel and the mechanization of mathematics
- Juliette Kennedy discusses Kurt Gödel’s Incompleteness Theorems: the
ingenious proofs and enduring impact
https://www.the-tls.co.uk/articles/kurt-godel-incompleteness-theorems/


JM

[Joao Marcos]

Os comentários sobre o *racionalismo otimista* ("platonismo ingênuo"?)
de Gödel, no artigo, são filosoficamente interessantes.

Das três observações que faço abaixo, as duas primeiras são críticas e
a terceira é um questionamento para os colegas.

###

(0)

Entre outras coisas, como observação parentética, parece-me um pouco
_out of the ordinary_ que se escreva algo assim:

"The axioms of PA include the commutative law of addition, for
example, which states that it doesn’t matter in which order two
numbers are added to each other, the result is the same. They also
include the single rule of proof called Modus Ponens: “if A implies B,
and A, then B”.

Suponho, contudo, que tais frases se tratem de uma espécie de
simplificação, _for the sake of the exposition_...

###

(1)

Formular o teorema de incompletabilidade de Gödel da seguinte maneira
também me parece razoavelmente _misleading_:

"Given any axiom system which is both consistent and sufficiently
strong computationally, in the sense of being able to encode finite
sequences (see below), there is a statement in the language of the
system that is true, but cannot be proved from the axioms."

Em particular, o sistema axiomático (não-recursivamente enumerável)
que contêm como axiomas todas as sentenças verdadeiras da Aritmética é
obviamente completo...

###

(2)

A pergunta que deixo aqui para os colegas é: qual é, na opinião de
vocês, o grau de verdade da asserção

"The proofs for both theorems depend on the concept of an encoding, or
in technical terms the arithmetization of syntax"?

Em outras palavras, qual o real grau de "dependência" do "conceito de
codificação" para as demonstrações de incompletude?

###

Joao Marcos

--
http://sequiturquodlibet.googlepages.com/

[Famadoria]

Me parece que o teorema da incompletude de Kleene prescinde de uma codificação.

Sent from my iPhone

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

[Joao Marcos]

> Me parece que o teorema da incompletude de Kleene prescinde de uma codificação.

Bem lembrado, Doria. O teorema de incompletabilidade de Gödel
realmente segue como corolário do resultado de Forma Normal de Kleene,
que não apenas prescinde de auto-referência mas que pode ser
demonstrado sem codificação. Com a minha pergunta, contudo, eu
pretendia inquirir a respeito da _necessidade_ de usar *aritmetização*
(ou recursos aritméticos, em geral) em demonstrações de
incompletabilidade (em particular, à la Gödel). Intuitivamente, a
resposta me parece ser negativa, isto é, não me parece que tais
_demonstrações_ "dependam da aritmetização da sintaxe", como afirma a
autora do artigo. Mas é fato também que, por um motivo ou por outro,
não tenho visto demonstrações do teorema gödeliano que evitem a
burocracia da aritmetização...

Abraços,
Joao Marcos

--
http://sequiturquodlibet.googlepages.com/

[Famadoria]

Vê o teorema de Kleene, de novo.

Sent from my iPhone

[Valeria de Paiva]

JM, 

Eu achei q vc queria ter uma medida de quao dependente de codificao uma prova e’. Eu acho q o Joyal tem uma prova de incompletude usando categories, q nao depende muito de codificacao. 

mas eu nunca vi ninguem tentando medir quao dependente de codificacao uma prova 'e. voce ja' viu algum assim?

abracos,

Valeria

Para ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/63B5BA64-530F-4B5F-8D55-2EB8C1CEC58D%40gmail.com.

[Joao Marcos]

Nunca vi, Valeria...

Você teria uma referência para a demonstração do Joyal?

Abraços, JM

[Valeria de Paiva]

bom, eu achei que tinha uma escrita pois a Milly  Maietti me disse que tinha, mas procurando no math overflow  vi isso:

https://mathoverflow.net/questions/132797/is-there-a-categorical-proof-of-g%C3%B6dels-incompleteness-theorem

depois procuro nos meus preprints, mas estou viajando

Boas Festas a todos,

abs

Valeria

--

Valeria de Paiva
http://vcvpaiva.github.io/
http://www.cs.bham.ac.uk/~vdp/

[Jorge Petrucio Viana]

Olá para todos,

não li esse artigo em detalhes, mas numa passada de olhos, não vi nem aritmetização, nem o predicado Bew, nem autoreferência na prova da incompletude.

https://projecteuclid.org/euclid.ndjfl/1027953483

abraços

P

--
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+u...@dimap.ufrn.br.

Para ver essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAESt%3DXvpJgzVJ7JEXjXvbtYnzqOrkSD30KHbzgwBH%2BOOs_6sOw%40mail.gmail.com.

[Carlos Gonzalez]

Eu não estou entendendo muito bem qual é o eixo desta discussão.

Suponha que trabalhamos em AP. 

Se demonstrar que o conjunto das fórmulas que não são teoremas não é recursivamente enumerável, então o conjunto dos teoremas não é recursivo, E isso pode ser provado de maneira finitária. Certo?

Também pode usar técnicas de teoria de modelos para construir modelos standard e outras, como ultraprodutos, para modelos não standard. Técnicas matemáticas não finitárias.

Um recurso divertido é acrescentar a AP uma constante nova "c" e um conjunto infinito de axiomas:

(s é a função sucessor)

não ( c = 0)

não ( c = s0)

não ( c = ss0)

não ( c = sss0)

.

.

não ( c = s...s0)

.

.

Por   compacidade essa teoria tem modelo. Claro, não standard.

Tudo isso é muito conhecido.

Carlos

Para ver essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CACRvmVQhtWnD6EW%2BbnyYqArdKpMVpsrnTgispR0%2BjyvO%2BHpGFA%40mail.gmail.com.

[Valeria de Paiva]

Legal esse paper to Putnam, Petrucio! obrigada por mandar.

Boas Festas pra todos!

Valeria

[Rodrigo Freire]

[Também não sei se entendi muito bem qual é a direção da questão, e o que eu vou escrever aqui pode não ter a ver com o problema intencionado.]

 Vou tentar explicar o que entendo pela codificação presente no teorema e como essa codificação está diretamente ligada à ideia fundacional de representar a matemática formalmente. É assim que está no meu livro, Tópicos em lógica de primeira ordem, que pode ser baixado livremente. 

Suponha que há uma teoria formal de primeira ordem T que “representa” a matemática. Como a metamatematica de T é parte da matemática, T é capaz de “representar” essa parte também. Isso deve implicar o que entendo por codificação:

1) há uma correspondência unívoca entre fórmulas de T e termos fechados de T (Para poder falar de suas fórmulas e “representar” sua metamatemática, T deve ter nomes não ambíguos para as fórmulas. Por exemplo, T deve ser capaz de dizer de uma fórmula que ela é bem formada. Para isso é preciso nomear a fórmula sem ambiguidade. Usamos ‘F’ como nome de F). 

2) tudo o que é decidido na metamatemática, é decidido por um método de cálculo matemático, portanto deve ser decidido em T: Tudo que é calculável deve ser calculável em T, pois T representa toda a matemática. (T deve representar predicados e funções recursivas, pois qualquer método matemático de cálculo é representável em T). 

1) + 2) é a codificação. Vamos ver o quanto disso é necessário para a demonstração que se T é consistente, a sua teoremicidade não é calculável em T. 

**Da codificação segue que a operação de diagonalização nas fórmulas (a operação que associa a fórmula F(‘F’) a qualquer fórmula F) é calculável em T. **

Se a propriedade metamatemática de ser teorema de T fosse calculável, então seria calculável em T. Isso significa que T seria capaz de deduzir B(‘F’), quando F é teorema, e ~B(‘F’), quando F não é teorema, para alguma fórmula B(x) de T que dizemos representar a teoremicidade. 

Mas como a diagonalização é calculável em T, é possível construir uma sentença G tal que G é equivalente à ~B(‘G’) em T. Portanto, se T não deduz G, então, pela hipótese que a propriedade de ser teorema é calculável, a não dedução de G é calculável em T, ou seja, T deduz ~B(‘G’). Mas ~B(‘G’) é equivalente a G em T, e concluímos que T deduz G. Novamente pela hipótese, a teoremicidade de G é calculável em T, portanto T deduz B(‘G’), que é equivalente a ~G. Portanto, T é inconsistente. 

Para essa demonstração basta supor 1) acima e apenas que a operação de diagonalização é calculável em T. Essa parte da codificação 1) + 2) que é requerida. Daí concluímos que se a teoremicidade for calculável em T, então T é inconsistente. É isso que fiz em meu livro, uma versão abstrata que não menciona funções recursivas. Todos os detalhes podem ser encontrados lá. 

Como já foi dito, há outras demonstrações, mas acho que essa é a que está mais diretamente ligada à ideia fundacional: se é possível uma representação formal da matemática em um sistema formal T, então a teoremicidade de T não é calculável (na metamatemática de T ou na própria T), a menos que T seja inconsistente. 

Em 25 de dez de 2019, à(s) 14:15, Carlos Gonzalez <gonz...@gmail.com> escreveu:



Para ver essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAGJaJ%2B-ekWSPbQ8UHZZhcTq4frt5%3DFTUkfhKtNnZt2-UopjN5A%40mail.gmail.com.

[Joao Marcos]

Petrucio, Carlos, Valeria: agradeço as mensagens!

Rodrigo, a sua resposta ajuda a corroborar a minha afirmação que a
demonstração do teorema de incompletabilidade gödeliano NÃO depende da
"aritmetização da sintaxe" (como defendeu a autora do artigo citado no
começo da presente discussão). Por certo, a necessária "representação
formal da Matemática" pode ser feita de variadas formas alternativas.
(Os detalhes da demonstração original gödeliana são de interesse
apenas para hackers!) Neste sentido, como ainda não tive tempo de
trabalhar com o seu livro, Rodrigo, posso dizer que aprecio
particularmente o interessante livro de Amílcar e Cristina Sernadas,
"Foundations of Logic and Theory of Computation", onde a noção de
computabilidade é definida sobre strings de alfabetos arbitrários;
contudo, a noção formal de _representabilidade_, ali, também recorre
diretamente a teorias da Aritmética --- como de costume.

Abraços,
Joao Marcos

> Para ver essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/BFF24528-233C-4A5C-81C2-EA7B2217B219%40gmail.com.



--
http://sequiturquodlibet.googlepages.com/

[Rodrigo Freire]

Agora entendo melhor. Aritmetização não é necessária, basta a noção formal e mais abstrata de representabilidade. Para citar uma referência muito antiga que já deixa isso bem claro, muito anterior ao meu livro e ao dos Sernadas, cito o clássico Tarski, Mostowski, Robinson, Undecidable Theories. (TMR)

TMR apresenta a seguinte versão do teorema de Godel (citando de memória, pode haver alguma variação inessencial)

-Se T tem nomes para suas fórmulas (item 1 da codificação na minha mensagem anterior) e é consistente, então T não representa simultaneamente a operação de diagonalização nas suas fórmulas e a dedutibilidade em T.

Essa versão é fácil de demonstrar, como tentei explicar na mensagem anterior. Não é preciso passar por funções recursivas para isso. Nada de aritmética.

Essa seria uma versão abstrata, livre de aritmética e de aritmetização, do que chamamos hoje de teorema de Tarski da indefinibilidade da verdade, apesar de Tarski atribuir a Godel em seu livro. No meu livro coloquei essencialmente a mesma coisa, como expliquei no prefácio. Fiz algo similar para o segundo teorema também.

Abraço


> Em 28 de dez de 2019, à(s) 12:52, Joao Marcos <boto...@gmail.com> escreveu:
>
> Petrucio, Carlos, Valeria: agradeço as mensagens!

[Hermógenes Oliveira]

Olá, pessoal.

João Marcos escreveu:

> Rodrigo, a sua resposta ajuda a corroborar a minha afirmação que a
> demonstração do teorema de incompletabilidade gödeliano NÃO depende
> da "aritmetização da sintaxe" (como defendeu a autora do artigo
> citado no começo da presente discussão).

Permitam-me assumir o ultrajante papel de advogado do diabo. :-)

Rodrigo Freire escreveu (ênfase minha):

> TMR apresenta a seguinte versão do teorema de Godel (citando de
> memória, pode haver alguma variação inessencial)

> *Se T tem nomes para suas fórmulas* (item 1 da codificação na minha

> mensagem anterior) e é consistente, então T não representa
> simultaneamente a operação de diagonalização nas suas fórmulas e a
> dedutibilidade em T.

Ora, é fácil se livrar da aritmetização se simplesmente a assumirmos
como hipótese!

O resultado de Kleene também foi aludido nesta discussão como
evidência em favor da tese de João Marcos. Esse resultado, de fato,
implica uma *versão* do resultado de Gödel que trata de teorias
recursivamente axiomatizáveis nas quais *as funções recursivas
primitivas são representáveis*[1]. Ora, para se chegar ao enunciado
original de Gödel, é necessário ainda estabelecer que as funções
recursivas primitivas são representáveis nas teorias fundacionais tipo
Principia Mathematica. É precisamente isso que é alcançado por meio
da aritmetização. Ainda que seja repertório básico para os lógicos de
carreira contemporâneos, isso não é evidente. Inclusive, pode-se
dizer que Gödel inaugurou com seu artigo os estudos do que hoje
chamamos de funções recursivas primitivas.

Se estamos pensando em demonstrações do enunciado original de Gödel,
com todo seu impacto e consequências, então não creio que seja
possível evitar a tal aritmetização (bem como diagonalização).
Supostas demonstrações livres dela estão fadadas a pressupô-la de
alguma maneira, seja explicitamente, ou embutida em definições.

Certamente, como já foi observado nesta discussão, há uma certa
vagueza em "demonstrações do resultado de incompletabilidade de
Gödel". Não está perfeitamente claro quando um resultado deve contar
como uma demonstração do enunciado gödeliano. Ademais, quando estamos
discutindo o que é ou não necessário para se demonstrar um resultado,
há que se considerar ainda uma certa ambiguidade na noção de
demonstração. Afinal, há boas e más demonstrações. Qual o valor de
se evitar esta ou aquela técnica se o preço é terminarmos com uma má
demonstração?

Assim como qualquer resultado, as demonstrações do teorema da
indecidibilidade do Gödel podem ser inseridas num espectro com relação
a sua perspicácia e poder elucidatório. Num dos extremos está algo
como a demostração do próprio Gödel (talvez com algumas melhorias
inessenciais na codificação) e no outro extremo está aquela em que
simplesmente se assume o enunciado do teorema como hipótese.

Afinal, o resultado é conhecido como teorema de Gödel e não teorema de
Finsler[2]. E, a julgar pela escassa correspondência entre os dois[3],
os detalhes técnicos, inclusive aritmetização, são uma importante
razão para essa nomenclatura. Portanto, não diria que seja matéria
apenas para hackers[3].

Notas:

[1] Em conversa privada, João Marcos indicou a excelente nota de Peter
Smith sobre o assunto:

https://www.logicmatters.net/resources/pdfs/KleeneProof.pdf

[2] Paul Finsler. Formale Beweise und die Entsheidbarkeit. Mathematische
Zeitschrift, Band 25, 1926, S. 676-682.

[3] Kurt Gödel. Collected Works, Volume IV, p. 405-415.

[3] A codificação particular escolhida por Gödel é, de fato,
inessencial, como observou o próprio Gödel, e pode ser substituída,
eventualmente por versões melhores, sem qualquer prejuízo. Porém, a
aritmetização em si me parece desempenhar um papel central.

--
Hermógenes Oliveira

"The competent programmer is fully aware of the strictly limited size
of his own skull; therefore he approaches the programming task in full
humility, and among other things he avoids clever tricks like the
plague." Edsger W. Dijkstra

[Rodrigo Freire]

A hipótese que T tem nomes para suas fórmulas significa apenas que as fórmulas de T e os termos fechados de T estão em correspondência 1-1: a cada fórmula F corresponde um termo fechado ‘F’. Nem precisa mencionar aritmética. Qualquer teoria em que o numero de fórmulas é igual ao número de termos fechados satisfaz isso por definição.

Que T não representa simultaneamente sua diagonalização de fórmulas (a operação que associa F(‘F’) à fórmula F) e sua teoremicidade é a conclusão (em TMR), e também dispensa qualquer menção à aritmética. Não é preciso qualquer menção, por exemplo, às funções recursivas nesse teorema. Onde está a aritmetização como hipótese?



> Em 28 de dez de 2019, à(s) 17:10, Hermógenes Oliveira <oliv...@daad-alumni.de> escreveu:
>
> Olá, pessoal.

> --
> 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.

> Para ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/AM6P192MB0488F538837579BDB703E438E9250%40AM6P192MB0488.EURP192.PROD.OUTLOOK.COM.

[Carlos Gonzalez]

Hermógenes e lista,

Eu , (pura teimosia?) continuo insistindo que a raiz do problema está na definição recursiva que usam as linguagens formais, que passam a ser, como Kleene disse, aritméticas.

Foi Thoralf Skolem, um defensor da teoria de números, que "aritmetizou" a lógica e a matemática quando deu a definição recursiva de fórmula, etc.

Um artigo interessante e profundo teria como nome:

"Thoralf Skolem and the mechanization of mathematics"

Para ser bem claro:
Para mim não tem sentido algum, nem interesse qualquer, falar da influência de Gödel na mecanização da matemática quando "fórmula", "dedução", etc., tem uma definição recursiva. Quero dizer coisas como: a concatenação e uma adição e a substituição é uma multiplicação. Por isso é que funciona a aritmetização de Gödel.

A propósito:
Alguém conhece uma bibliografia sobre o uso geral desse conceito de "mecanização"? "Que comportamento mecânico que tem esse homem", etc.

Carlos

--
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.

Para ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/AM6P192MB0488F538837579BDB703E438E9250%40AM6P192MB0488.EURP192.PROD.OUTLOOK.COM.

[Hermógenes Oliveira]

Rodrigo Freire <freir...@gmail.com> escreveu:

> A hipótese que T tem nomes para suas fórmulas significa apenas que
> as fórmulas de T e os termos fechados de T estão em correspondência
> 1-1: a cada fórmula F corresponde um termo fechado ‘F’. Nem precisa
> mencionar aritmética. Qualquer teoria em que o numero de fórmulas é
> igual ao número de termos fechados satisfaz isso por definição.

> Que T não representa simultaneamente sua diagonalização de fórmulas
> (a operação que associa F(‘F’) à fórmula F) e sua teoremicidade é a
> conclusão (em TMR), e também dispensa qualquer menção à
> aritmética. Não é preciso qualquer menção, por exemplo, às funções
> recursivas nesse teorema. Onde está a aritmetização como hipótese?

Bem, Rodrigo, acho que podemos concordar que a questão em pauta não é
a simples *menção* do termo "aritmetização", ou outro termo que o
valha, mas se a técnica em si não é, de alguma maneira, pressuposta
nas demonstrações alternativas que estamos discutindo.

No caso da sua proposta específica, você pergunta:

> Onde está a aritmetização como hipótese?

Eu necessitaria de mais detalhes para fornecer uma resposta mais
enfática, mas faço algumas indicações a seguir.

Você propõe:

> Se o numero de fórmulas de T é igual ao número de termos fechados de
> T, e T é consistente, então T não representa simultaneamente a

> operação de diagonalização nas suas fórmulas e a dedutibilidade em
> T.

Ora, consideremos uma teoria matemática fundamental, numa formulação
qualquer, digamos, nos moldes do Principia Mathematica, como Gödel
fez. Vamos avaliar a sua (in)decidibilidade com base no enunciado
acima.

Suponhamos que essa teoria é consistente. O critério de que o número
de fórmulas seja igual ao número de termos fechados, claramente, não
pode ser suficiente para a indecidibilidade (ex. Aritmética de
Presburger). O outro critério seria que T "*representa* a operação de
diagonalização nas suas fórmulas". O que significa isso? Seria
possível avaliar esse critério para a nossa teoria sem apelar para a
aritmetização?

A minha aposta é que não.

Imagino que você tenha em mente algo similar ao que consta no TMR,
§II, Theorem 1. Ali, o resultado está enunciado em termos da noção de
definibilidade (§II.2), onde, assim eu mantenho, estaria embutido o
apelo à aritmetização. Inclusive, esse termo "definível"
("definierbar") é o mesmo usado por Gödel no artigo original. Porém,
enquanto Gödel meticulosamente constrói as classes definitórias dos
predicados e relações metamatemáticas por meio da aritmetização, TMR
simplesmente substituem uma definição existencial, inserem como
hipótese do enunciado e pronto! Típico matemático clássico! Sempre
que há uma bela e elegante construção, substitui uma definição
existencial e alega um resultado mais geral e abstrato. ;-)

A questão é: Como seria possível demonstrar o existencial ali com
respeito a função D de diagonalização para uma teoria particular, como
o Principia Mathematica (e, assim, obter o resultado original de
Gödel), sem usar aritmetização?

--
Hermógenes Oliveira

[Rodrigo Freire]

Vamos primeiro analisar o teorema em termos da dicotomia: ou T não representa a diagonalização ou T não representa a sua teoremicidade.

A diagonalização é um caso particular de uma operação muito básica da matemática elementar: a substituição de uma variável livre em uma expressão por um termo fechado. Se T não representa a diagonalização, então T não representa a diagonalização, T falha em representar a matemática.

Se T é bem sucedida em representar a matemática (elementar), então T representa a diagonalização (pois essa é sem sombra de dúvida uma operação básica da matemática elementar) e, como consequência do teorema, T não representa sua teoremicidade.

Assim eu responderia a questão de como avaliar esse teorema em um sistema particular. O ponto é que não é necessário avaliar o critério de representar a diagonalização. Se nosso sistema é consistente, então ou ele não serve para representar a matemática elementar, ou não representa a sua teoremicidade. Os dois lados da dicotomia servem para quebrar certas expectativas fundacionais.

Agora a aritmetização: Entendo que esse termo está sendo usado para um tipo de implementação da “representação formal da matemática” em T. Há outros modos de fazer isso que não apelam para números. Acho que essa é a “eliminação” da aritmetização que está em questão. É claro que não se está propondo a eliminação da “representação formal da matemática em T”. Se você identifica essas duas coisas, tudo bem. Mas não acho razoável. “Representação” é muito mais geral que “aritmetização”. Me parece claro que “aritmetização” é um tipo muito particular e restrito de “representação” que remete ao uso de operações aritméticas básicas com números apenas. Mas essa é uma discussão sobre a identificação de dois termos indefinidos.

Abraço



> Em 29 de dez de 2019, à(s) 10:35, Hermógenes Oliveira <oliv...@daad-alumni.de> escreveu:
>
> Rodrigo Freire <freir...@gmail.com> escreveu:

> --
> 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.

> Para ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/AM6P192MB04885CB48E338A7815D3D03EE9240%40AM6P192MB0488.EURP192.PROD.OUTLOOK.COM.

[Francisco Miraglia Neto]

> Car@s,
>
> Me indago porque ninguém parece se lembrar da tese de doutorado do Smulian em Princeton, publicada naquela coleção de Princeton que tinha capa vermelha. Para quem não conhece , recomendo:
> A theory of formal systems
> Princeton Univ Press, 1961.
>
> Há um artigo anterior de 1959, seu primeiro artigo, anterior à tese, em que os argumentos de Godel são analisados e simplificados consideravelmente.
>
> De todo modo, o que chamamos de aritmetizacão , um caso particular de internalização de uma Teoria no sentido que fala o Rodrigo, possui muitas outras aplicações, como todo mundo sabe. O mesmo se aplica à ideia de diagonalização, que trata-se, na minha opinião, de um método , uma ideia e não apenas uma técnica particular.
>
> Um grande abraço a todas e todos e Feliz Ano Novo !!
>
> Chico Miraglia

[Francisco Miraglia Neto]

[Carlos Gonzalez]

Prezado Chico,

Muito esclarecedores os teus comentários.

Eu não conheço e não sei se é pertinente um outro livro de Smullyan:

"Diagonalization and Self-Reference"

Nos últimos tempos da sua vida, Daniel Glushankoff estudo grupos reticulados e me comentava algumas coisas do seu trabalho.

Essa teoria é incompleta. Daniel dizia que haviam encontrado uma maneira de representar a aritmética e daí podiam ser usadas técnicas análogas às do teorema de Gödel para demonstrar a incompletude.

Eu nunca vi essa demonstração, mas deve ter alguma maneira ingeniosa de representar a aritmética.

Carlos

--
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.

Para ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/33AF2F17-CF65-4350-9073-B8BDA52BAA4D%40ime.usp.br.

[Hermógenes Oliveira]

Olá, Chico.

Eu não li a tese de doutorado do Smullyan ou o artigo de 1959, mas
conheço o livro de 1992, Gödel's Incompleteness Theorems. De acordo
com o prefácio, ideias daquelas obras anteriores estão incorporadas
ali.

Dentre a literatura secundária sobre os teoremas de Gödel, esse livro
do Smullyan é o meu predileto. Me lembro de nós termos usado ele,
juntamente com o artigo original do Gödel, num curso do mestrado na
UFG em meados de 2011. Um dos cursos mais divertidos dos quais eu já
participei!

O livro apresenta codificações bem perspicazes que, na minha opinião,
são melhores que as do artigo original. Contudo, ele não abre mão da
aritmetização em momento algum, ainda que em alguns momentos a
pressuponha *explicitamente* quando apresenta formulações abstratas
do resultado gödeliano.

--
Hermógenes Oliveira

________________________________________
From: Francisco Miraglia Neto <mira...@ime.usp.br>
Sent: Sunday, 29 December 2019 12:47
Cc: Lista brasileira
Subject: Re: [Logica-l] Kurt Gödel and the mechanization of 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.

Para ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CE2D8CD8-A246-42D6-8622-47C714C61337%40ime.usp.br.

[Francisco Miraglia Neto]

Caro Hermógenes,

Ambos os originais que mencionei, assim como o lembrado pelo Carlos são muito interessantes; considero os dois primeiros melhores que o livro de 1992, que é um ótimo texto.

Um grande abraço,

Chico

> On 29 Dec 2019, at 16:57, Hermógenes Oliveira <oliv...@daad-alumni.de> wrote:
>
> Olá, Chico.

> Para ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/AM6P192MB04885FBB7208427DFED25A43E9240%40AM6P192MB0488.EURP192.PROD.OUTLOOK.COM.

[Carlos Gonzalez]

Prezado Chico e lista,

Já que estamos no problema da representabilidade da aritmética, quero mencionar uma questão que gerou bastante confusão décadas atrás e que talvez alguns lógicos mais novos desconheçam.

Trata-se de teorias de corpos ordenados. Algumas delas (característica zero? corpos algébricos completos?) são completas e não se aplica o Teorema de Incompletude.

Esses corpos tem o zero, o 1, e as operações adição e multiplicação. 

Por exemplo: tem 0, 1, 1+1, 1+1+1, etc.

Não tem um predicado "x é um número natural" e não tem as definições recursivas de adição e produto.

O que poderíamos dizer de por que falha a representabilidade?

Carlos

Para ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/AC31FEF5-DE6D-4BE7-A437-785F49E97810%40ime.usp.br.

[Rodrigo Freire]

Legal, vamos ver como o teorema de Godel na versão que mencionei (TMR) *se aplica* nesse caso sem aritmetização no sentido usual (sequer há um predicado para os números naturais). Depois analiso a falha de representabilidade.

Sim, a teoria dos corpos reais fechados (corpos ordenados tais que todo positivo é quadrado e todo polinômio satisfaz o teorema do valor intermediário) e a teoria dos corpos algebricamente fechados de característica zero são completas e decidiveis. Vou considerar a teoria dos corpos reais fechados, denotada por T.

Os termos fechados dessa teoria são termos para números inteiros. Vamos pensar na seguinte correspondência 1-1 entre termos e fórmulas: enumeramos os teoremas com os números negativos e os não teoremas com os não negativos. Se F é fórmula, ‘F’ será o termo fechado correspondente ao número na numeração acima. Por exemplo, se F é o primeiro teorema, ‘F’ será o termo -1. Se F é o primeiro não teorema, ‘F’ é o termo 0.

Assumida essa correspondência entre fórmulas e termos fechados, temos que a teoremicidade de T é representada pela fórmula x<0.
De fato, se F é teorema, ‘F’ < 0 é teorema de T, e se F não é teorema, ~(‘F’ < 0) é teorema de T.

O teorema de Godel se aplica e T não representa a diagonalização (para a correspondência entre fórmulas e termos). T falha em representar a metamatemática elementar, portanto falha em fornecer uma representação formal exaustiva da matemática.


Poderíamos dizer que a representabilidade falha porque essas teorias admitem eliminação de quantificadores: os quantificadores não adicionam poder de definibilidade dentro dessa teoria. Mas esse não é um resultado óbvio, que está presente desde o início, por isso essa resposta pode não ser satisfatória.

O que é mais básico é que T não é suposta ser uma representação formal exaustiva da matemática. Ao contrário, desde o início se sabe que muita coisa fica de fora. T não é capaz de representar outras funções contínuas elementares (e.g. exponencial) além dos polinômios.

Mas Essa teoria não está sozinha nisso. A dicotomia de Godel implica que, dada uma T consistente e uma correspondência entre fórmulas e termos fechados de T, pelo menos uma entre diagonalização e representabilidade escapa à representação formal em T. Ou seja, não temos uma representação formal exaustiva da matemática.

Abraço
Rodrigo




> Em 29 de dez de 2019, à(s) 23:38, Carlos Gonzalez <gonz...@gmail.com> escreveu:
>
> 

[Tony Marmo]

1. Seria interessante se alguém colocasse aqui uns liames para os artigos originais do Gödel na internet, ou traduções confiáveis. Cotejar o que ele escreveu com o que foi feito por outros depois é um bom método para guiar mais claramente a discussão.

2. A questão de tratar da incompletude num meta-nível qualquer não se restringe a discutir as características do sistema de representação que vai ser usado. O que estava em discussão para Gödel e contemporâneos eram os limites do próprio método axiomático e da própria relação entre matemática e lógica. 

Como sabemos disso? Sabemos disso porque no século XIX esses dois temas tinham dominado os debates lógicos e tinham crescido cada vez mais. Foi nesse período que surgiram as lógicas multivalentes.

Gödel conhecia o trilema de Aristóteles, sabia das limitações do método axiomático e também versões anteriores do paradoxo do mentiroso. Hilbert quando escreveu seu manifesto (que as pessoas podem ler no livro de Carnielli e Epstein) aparentava não estar consciente dessas coisas. 

--
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.

Para ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/5282631B-D946-482D-B751-E0B92D249084%40gmail.com.

[Hermógenes Oliveira]

> Hermógenes e lista,

Olá, Carlos.

> Eu , (pura teimosia?) continuo insistindo que a raiz do problema
> está na definição recursiva que usam as linguagens formais, que
> passam a ser, como Kleene disse, aritméticas.

Bem, eu, particularmente, não vejo nenhum problema com isso.

Você havia observado:

> Se demonstrar que o conjunto das fórmulas que não são teoremas não é
> recursivamente enumerável, então o conjunto dos teoremas não é
> recursivo, E isso pode ser provado de maneira finitária. Certo?

O problema em se abordar o resultado obtido por Gödel em termos da
teoria das funções recursivas é que se perde de vista, ou simplesmente
se pressupõe, a relação entre esses conceitos da teoria da
recursividade e as teorias formais com aspirações fundacionistas.
Hoje isso faz parte do repertório do lógico, e alguns poderiam mesmo
tomar como óbvio ou evidente, porém, foi algo que Gödel precisou
demonstrar! E, se parece tão natural agora, é porque ele o fez!

Após o teorema demonstrado, fica fácil olhar para trás e formular
enunciados equivalentes ao resultado original de Gödel os quais, ao
menos superficialmente, não fazem uso dos conceitos e métodos
encontrados no original.

Observações semelhantes se aplicam à sua sugestão envolvendo modelos
não-standard.

Imagine que você voltasse no tempo, para 1928, e se encontrasse com
Hilbert, ou Ackermann ou Bernays e dissesse a eles que o programa do
Hilbert não pode triunfar porque "nem toda função recursiva parcial é
potencialmente recursiva" (ou qualquer outro enunciado da teoria da
recursão que o valha) e prosseguisse com as definições dos conceitos
que ocorrem no enunciado e uma demonstração dele. Qual seria a
reação deles?

Ou, se viagem no tempo for ficção científica demais, imagine que
você está *demonstrando* para seus alunos o resultado de Gödel e
explicando seus efeitos sobre o programa de Hilbert. Você usaria
modelos não-standard? Teoria da recursividade?

Uma boa parte desses conceitos, como o de modelos não-standard, só
fazem sentido hoje *por causa* do resultado de Gödel e, portanto, não
podem prescindir dele ou substituí-lo.

Por isso, me parece que algumas alternativas propostas nesta discussão
pressupõe, ainda que implicitamente, o resultado original (ou uma
parte importante dele).

Nós podemos, eventualmente, nos contorcer com considerações informais
baseadas no nosso já solidificado conhecimento de lógica, dizendo que
é evidente a relação entre sistemas formais e recursividade, ou que é
óbvio que qualquer teoria adequada da matemática permite
diagonalização, ou coisas do gênero. Mas quando se trata de
*demonstrar* essas alegações, fazer as continhas mesmo e mostrar o
recibo, acho que é difícil escapar de algo semelhante ao trabalho
meticuloso do original.

Não lembro onde li isso, mas dizem que Gödel considerou o seu teorema
a partir de algumas ideias bastante informais, de ordem semântica,
envolvendo autorreferência. Mas ele sabia que esse tipo de argumento
não convenceria os vovozinhos de Göttingen e sentou para elaborar uma
demonstração completamente sintática. O esforço teria o custado uma
temporada no sanatório. Mas, em troca, recebemos uma bela demonstração.

--
Hermógenes Oliveira

[Hermógenes Oliveira]

Rodrigo Freire <freir...@gmail.com> escreveu:

> Legal, vamos ver como o teorema de Godel na versão que mencionei
> (TMR) *se aplica* nesse caso sem aritmetização no sentido usual
> (sequer há um predicado para os números naturais).

Ora, se a teoria é decidível, ninguém disputa que a aritmetização pode
ser dispensada! Trata-se, porém, de dispensá-la em demonstrações de
*indecidibilidade*!

> [...]

>
> Agora a aritmetização: Entendo que esse termo está sendo usado para
> um tipo de implementação da “representação formal da matemática” em
> T. Há outros modos de fazer isso que não apelam para números. Acho
> que essa é a “eliminação” da aritmetização que está em questão. É
> claro que não se está propondo a eliminação da “representação formal
> da matemática em T”. Se você identifica essas duas coisas, tudo
> bem. Mas não acho razoável. “Representação” é muito mais geral que
> “aritmetização”. Me parece claro que “aritmetização” é um tipo muito
> particular e restrito de “representação” que remete ao uso de
> operações aritméticas básicas com números apenas. Mas essa é uma
> discussão sobre a identificação de dois termos indefinidos.

Bem, então me parece que há uma maneira bastante direta de se resolver
a questão.

Considere o mencionado teorema 1 na seção II.2 do TMR. Tome uma
formalização qualquer T, em primeira ordem, da aritmética. Você
poderia, porventura, *demonstrar*, sem uso da aritmetização, que a
função D é definível em T (sob a hipótese de que T é consistente)?

Sinta-se a vontade para usar qualquer outro tipo de "representação
formal da matemática" que não seja aritmética (que não apele a
números), ou para, alternativamente, apenas indicar uma referência
na literatura onde isto tenha sido realizado.

--
Hermógenes Oliveira

[Rodrigo Freire]

Meu ponto é que a essência do teorema é uma falha de representação (uma entre duas, qual vai falhar depende da nomeação das fórmulas, ou seja, da godelizacao). Indecidibilidade e indefinibilidade da verdade podem ser consequências dessa falha, mas o resultado é geral e se aplica a teorias decidiveis e indecidiveis. Você diz:

> Ora, se a teoria é decidível, ninguém disputa que a aritmetização pode
> ser dispensada! Trata-se, porém, de dispensá-la em demonstrações de
> *indecidibilidade*!

O que eu fiz para a teoria dos corpos reais fechados pode ser feito para teorias indecidiveis, é só escolher uma nomeação adequada. Vamos ver.

> Considere o mencionado teorema 1 na seção II.2 do TMR. Tome uma
> formalização qualquer T, em primeira ordem, da aritmética. Você
> poderia, porventura, *demonstrar*, sem uso da aritmetização, que a
> função D é definível em T (sob a hipótese de que T é consistente)?

Sim. Primeiro é preciso formular a questão apropriadamente, pois a definibilidade é relativa a uma nomeação das fórmulas, não vale em absoluto como veremos. Por nomeação entendo uma atribuição de termos a fórmulas de modo injetivo. Normalmente isso é chamado de godelizacao.

Primeiro, digo novamente que não é necessário mostrar qualquer representabilidade para aplicar o teorema, porque para qualquer nomeação das fórmulas, ele dá como conclusão que ou D não é representável ou a teoremicidade não é representável. O teorema mostra uma falha de representabilidade em qualquer caso, e essa é sua essência como eu entendo.

Segundo, observo que D não é “definível” em absoluto. A representabilidade é relativa a uma nomeação das fórmulas. Vamos ver isso. Vamos representar a teoremicidade de T em T (isso mesmo, a teoremicidade da aritmética). Considere a seguinte nomeação: o conjunto dos teoremas da aritmética é enumerável. Nomeie o primeiro teorema com o termo fechado 0, o segundo com 2, o terceiro com 4, ... Fixe também uma nomeação dos não teoremas com os termos para números ímpares.

A fórmula (Existe y; x = y + y) representa os teoremas em T para a nomeação dada acima! O que acontece, claro, é que a diagonalização não é representável para essa nomeação! Essa nomeação também não é recursiva, nem poderia ser, claro.

Sua questão deve ser entendida assim: mostre que há uma nomeação das fórmulas tal que a diagonalização é representável com essa nomeação. Isso não é necessário para aplicar o teorema e concluir que T tem falha de representabilidade. De qualquer modo, vamos ver o que podemos fazer.

Enumere as fórmulas que não são diagonalização com os termos para os números primos. Para cada fórmula F, o termo para a diagonalização de F será ‘F’.’F’. (O termo produto do termo ‘F’ com ele mesmo).

A fórmula y=x.x representa a diagonalização com essa nomeação.

Abraço
Rodrigo






> Em 30 de dez de 2019, à(s) 10:59, Hermógenes Oliveira <oliv...@daad-alumni.de> escreveu:

[Carlos Gonzalez]

Prezado JM e lista,

Só agora que li o artigo em questão. O lado bom é que gerou uma discussão muito interessante na lista.

Más o artigo é muito ruim, um lixo.

Por exemplo:

"Gödel’s own position. In remarking that “My theorems only show that the mechanization of mathematics . . . is impossible” (italics mine), Gödel was expressing the view that while the activity of the mathematician cannot be reduced to a set of computational rules, mathematics is nevertheless still decidable, meaning that the truth of any mathematical proposition can, at least in principle, be decided one way or another, by human beings"

:-) Deve estar usando a famosa regra super-indutiva: "se existe um x tal que P(x), então para todo x vale P(x)"

-----> como a atividade do matemático não pode ser reduzida a um conjunto de regras computacionais, nunca é decidível, de modo que a verdade de 2+2=4 deve ser decidida por seres humanos <-----

Non sequitur!

"In ordinary language, consider, say, a system with a fixed finite alphabet together with some simple axioms describing the behaviour of the natural numbers 0, 1, 2 . . "

"In ordinary languaje" os números naturais são bem, mas muito bem comportados. A aritmética de Presburger descreve ou não o comportamento dos número naturais?

Só para evitar outro erro comum: as fórmulas indecidíveis tem de ter variáveis e o seu prefixo mínimo é "para todo x existe y para todo z". Para as fórmulas sem variáveis, AP é completa e decidível. Também para fórmulas com prefixo "para todo x existe y" e "existe x para todo y". Ackermann trabalhou muito para mostrar fragmentos da lógica de primeira ordem que são decidíveis, dando início ao que depois foi o método de eliminação de quantificadores de Tarski.

"The axioms of PA include the commutative law of addition"

Por favor, me ajudem a encontrar a lei da comutatividade da adição!

P. ex., na página 94 do livro de van Heijenoort.

Eu nunca vi na minha vida alguém escrever os axiomas de AP e colocar a comutatividade da adição.

Várias outras críticas foram feitas por colegas na discussão desse artigo.

Mas acho que os mal-entendidos dessa senhora são tão básicos que dificilmente seja interessante continuar discutindo esse artigo.

Repito, entretanto, que várias contribuições da discussão nesta lista são muito esclarecedoras e devem ser tomadas em séria consideração.

Com relação à senhora Juliette Kennedy, talvez seja conveniente pensar seriamente em abandonar a filosofia da matemática.

O capítulo 10 do livro "Imposturas intelectuais" de Sokal e Bricmont trata sobre os abusos usando o Teorema de Gödel e a Teoria de Conjuntos. Mas parece que isso é um história de nunca acabar.

Colegas: sintam-se a vontade para assinalar erros e mal-entendidos meus.

Carlos

Off topic: Décadas atrás, Roberto Cignoli era diretor da Revista da Uniión Matemática Argentina. Pediu-me para fazer uma resenha do livro "El Teorema de Gödel", de Emilio Díaz Estévez.

Eu tomei o trabalho muito seriamente, anotando num caderno muitos erros básicos de lógica que continha o livro.

Mostrei para Cignoli, que falou: "Si ese tipo no entendió nada de lógica, entonces no vale la pena publicar una reseña."

Nunca foi publicada la resenha na revista de UMA e longas horas de trabalho minhas foram perdidas.

On Wed, Dec 18, 2019 at 1:32 PM Joao Marcos <boto...@gmail.com> wrote:

Kurt Gödel and the mechanization of mathematics

- Juliette Kennedy discusses Kurt Gödel’s Incompleteness Theorems: the
ingenious proofs and enduring impact
https://www.the-tls.co.uk/articles/kurt-godel-incompleteness-theorems/


JM

--
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.

Para ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAO6j_Lgzncc2mR5dGtvf717cHoHJ-1aaZgncPnS6VwHeu64cpw%40mail.gmail.com.

[Valeria de Paiva]

Alo Carlos, e todos,

Desculpe, mas eu nao acho que o artigo seja ruim nao.

De novo, 'e escrito pra gente que nao 'e da area. 

Os "erros" nesse caso sao bem menores do que os do caso do paper sobre o axioma da escolha. (comutatividade da adicao nao 'e necessaria? pecado pequeno!)

Sao simplificacoes para facilitar o entendimento, me parece. como disse o JM.

A pergunta original do JM me parece bem interessante e a discussao que se seguiu tb.

concordo completamente com o Hermogenes que

>Típico matemático clássico! Sempre que há uma bela e elegante construção, substitui uma definição

existencial e alega um resultado mais geral e abstrato. ;-)

E' claro que a uma certa altura, estamos discutindo o que individualmente achamos mais claro ou mais elucidativo ou mais razoavel e ai as pessoas as vezes nao convergem.

eu concordo com o Rodrigo que:

>A representabilidade é relativa a uma nomeação das fórmulas.

e tb tambem q

> Por nomeação entendo uma atribuição de termos a fórmulas de modo injetivo. Normalmente isso é chamado de godelizacao.

mas discordo de

>Sua questão deve ser entendida assim: mostre que há uma nomeação das fórmulas tal que a diagonalização é representável com essa nomeação.

quando a "prova" prossegue com

>Enumere as fórmulas que não são diagonalização com os termos para os números primos. 

e eu vou explicar pra um aluninho o que sao numeros primos, eu ja' uso a aritmetica tradicional, como de costume.

dai que concordo mais com:

>A codificação particular escolhida por Gödel é, de fato, inessencial, como observou o próprio Gödel, e pode ser substituída,

eventualmente por versões melhores, sem qualquer prejuízo.  Porém, a aritmetização em si me parece desempenhar um papel central.

Enfim, sempre bom saber de maneiras de reformular as coisas que sejam ou nao equivalentes. 

aprendemos todos mais algumas coisas, ou pelo menos eu aprendi.

mas a pergunta que o JM fez, que me parece a mais interessante 'e como a gente define o que 'e uma codificacao melhor ou uma pior?

qual deve ser o criterio pra codificacoes?

Acho que chamar a professora no caso de uma "impostora intelectual" 'e pegar pesado.

mas de novo, isso 'e so' mimha opiniao.

Meus melhores votos pra 2020,

Valeria

--
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+u...@dimap.ufrn.br.

Para ver essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAGJaJ%2B9U73qCYx8bt0Q4Myw9sB5-tYQXKp38Uj0SPWc2HmTZTg%40mail.gmail.com.

[Rodrigo Freire]

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. 

No que me concerne, foi me perguntado se eu poderia, porventura, representar a diagonalização *na aritmética* sem usar aritmetizacao. Pois bem, posso resolver o problema sem usar a divisão em primos e compostos. Se eu usasse só a divisão entre pares e ímpares estaria bom? Ou a dicotomia pares e ímpares ainda conta como aritmetizacao? Se for por esse caminho, qualquer representação matemática na aritmética é aritmetizacao por definição, e devo supor que aritmetizacao começou com Pitagoras, ou antes dele, não com Godel. Entendo que aritmetizacao não é um termo definido, como já disse, mas supõe-se que o lema da função beta de Godel e a definibilidade das funções recursivas são parte dessa técnica. Não preciso usar nada disso. 

Abraço

Em 2 de jan de 2020, à(s) 19:28, Valeria de Paiva <valeria...@gmail.com> escreveu:



Para ver essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAESt%3DXsQDdKFtXARM%3DfoUkR6TBWT5N5dKW8xVTiLRQ_AtzaWCw%40mail.gmail.com.

[Carlos Gonzalez]

Valeria,

Obrigado pelos comentários.

Primeiro:

" sao bem menores do que os do caso do paper sobre o axioma da escolha"

Desculpa, mas eu não sei a que paper você está se referindo. Agradeço se especificar.

Segundo:

Existem em filosofia sérias discordâncias metodológicas.

Queria colocar uma delas e gostaria de saber a posição dos membros da lista, em público ou em privado.

Vamos lá.

A prof. Kennedy afirma:

"The axioms of PA include the commutative law of addition".

E eu assinalo que essa afirmação é falsa, citando van Heijenoort.

Verdade que a gente fala "axiomas de AP" como formando parte do folclore e aparecendo em manuais introdutórios.

A autora não faz citação. Tratando-se de um artigo filosófico deveria citar alguma fonte, eu acho. Eu sou um pouco fanático de citações bem feitas: livro, número de página, por exemplo.

Não estou discutindo se é ou não necessária, pois você fala:

"comutatividade da adicao nao 'e necessaria?"

Estou dizendo que não é enunciada como axioma na AP.

Como se alguém falasse: "tem uma lata de cerveja na geladeira", mas não tem.

Será um "pecado menor"?

Então se eu falar, "existe um cardinal inacessível está entre os axiomas de ZF", também é um erro não muito sério?

Para mim, é melhor citar de mais, que citar de menos. E facilita o trabalho científico e a crítica.

Mas onde eu sou radical, é que um trabalho sério não pode fazer afirmações falsas porque esqueceu de verificar a citação.

Não sei, gostaria de ver a posição dos colegas e que me falem se estou exagerando.

Carlos

[Valeria de Paiva]

oi Carlos

>Desculpa, mas eu não sei a que paper você está se referindo. Agradeço se especificar.

Eu estava me referindo a discussao comecada pelo Rodrigo em

https://groups.google.com/a/dimap.ufrn.br/forum/#!topic/logica-l/KGfQ33Pp-7w

8 de outubro "a pior tentativa de explicar a hipotese do continuo"

abs

Valeria

[Hermógenes Oliveira]

Olá, pessoal.

Carlos Gonzalez <gonz...@gmail.com> 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 <freir...@gmail.com> 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", 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.

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

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.

> No que me concerne, foi me perguntado se eu poderia, porventura,
> representar a diagonalização *na aritmética* sem usar
> aritmetizacao. Pois bem, posso resolver o problema sem usar a
> divisão em primos e compostos. Se eu usasse só a divisão entre pares
> e ímpares estaria bom? Ou a dicotomia pares e ímpares ainda conta
> como aritmetizacao?

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 formal, e que basta
mencionar números para que se tenha aritmetização? Não me parece
razoável.

Agora, nós poderíamos, eventualmente, fornecer critérios gerais (por
exemplo, por meio de definições) que uma codificação precisa obedecer
para desempenhar o papel pretendido na aritmetização. Isso não
significa, porém, prescindir da aritmetização. Seria apenas o mesmo
que dizer, em termos coloquiais: "Não enche o saco! Gödel já mostrou
que dá pra fazer! Ninguém tem tempo ou interesse nessas continhas.
Com exceção, talvez, dos hackers. Vá amolar um construtivista!"

Referências:
[1] https://groups.google.com/a/dimap.ufrn.br/d/msg/logica-l/3r3JuY79Ojc/r-G5sBKzBgAJ
[2] https://groups.google.com/a/dimap.ufrn.br/d/msg/logica-l/dAbP6w2kx8w/VawkJgKnBwAJ

--
Hermógenes Oliveira

»Die Mathematiker sind eine Art Franzosen: Redet man zu ihnen, so
übersetzen sie es in ihre Sprache, und dann ist es alsobald ganz etwas
anderes.« Johann Wolfgang von Goethe

[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 formal, e que basta
mencionar números para que se tenha aritmetização?  Não me parece
razoável.

Agora, nós poderíamos, eventualmente, fornecer critérios gerais (por
exemplo, por meio de definições) que uma codificação precisa obedecer
para desempenhar o papel pretendido na aritmetização.  Isso não
significa, porém, prescindir da aritmetização.  Seria apenas o mesmo
que dizer, em termos coloquiais: "Não enche o saco! Gödel já mostrou
que dá pra fazer!  Ninguém tem tempo ou interesse nessas continhas.
Com exceção, talvez, dos hackers.  Vá amolar um construtivista!"

Sim, a nomeação das fórmulas (codificação) precisaria ser tal que a diagonalização e todas as propriedades recursivas são representáveis com ela, como eu disse na minha primeira mensagem lá atrás. Com isso, TMR fornece as consequências desejadas (indecidibilidade, incompletude). Para ver se isso é possível sem aritmetização, é preciso explicar melhor o que é aritmetização.

 

[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

--

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+u...@dimap.ufrn.br.

Para ver essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAExWzUJcvMewz%2B3MTjT2MopP8Me4XEnAn2OdMKVkJeVLxnegZQ%40mail.gmail.com.