How do we construct the Gödel’s sentence in Martin-Löf type theory?

[Bruno Bentzen]

Olá pessoal,

Venho acompanhando a thread "How do we construct the Gödel’s sentence in Martin-Löf type theory?" no MathOverflow 

https://mathoverflow.net/q/272982/58734

que tem sido bem popular desde os últimos dias (e contado com a participação da Valéria e do Dana Scott).

Penso que talvez a discussão seja de interesse para alguns dos colegas da lista.

Abraços,

Bruno

--

Bruno Bentzen

https://sites.google.com/site/bbentzena/

[Rodrigo Freire]

Olá Bruno,

Parabéns para a Valeria e para você pela ótima participação. 

Como é sabido por nós, Martin Loef afirma que verdade não pode ser identificada com demonstrabilidade em um sistema específico devido ao teorema de Godel. Por isso a identificação dele seria: verdade é demonstrabilidade "em geral" (o que também não é claro que muda muita coisa, mas não esse o ponto da discussão). Ao que parece, ninguém duvida que qualquer sistema recursivamente enumerável razoavelmente forte pode ser diagonalizado para produzir uma sentença de Godel, mas um dos problemas seria como poderíamos dizer construtivamente que a sentença de Godel é verdadeira. 

A sentença de Godel pode ser canonicamente interpretada como a afirmação que uma determinada máquina de Turing (que busca uma demonstração da própria sentença de Godel) nunca para. Você menciona em um comentário que a sentença de Godel não pode ser dita verdadeira construtivamente, apenas podemos dizer que ela não é falsa. Usando a interpretação acima, construtivamente poderíamos dizer então que não é o caso que não é o caso que aquela máquina de turing não para. Mas isso não seria o mesmo que dizer que aquela máquina de Turing não para pela eliminação da tripla negação? E isso não é o mesmo que dizer que G é verdadeira?

Abraço

Rodrigo

Enviado do meu iPhone

--
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 postar nesse grupo, envie um e-mail para logi...@dimap.ufrn.br.
Acesse esse grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
Para ver essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/c155c92b-0bce-4012-aa97-6b79c44e769d%40dimap.ufrn.br.

[Anderson Nakano]

Boa tarde, pessoal.

Obrigado, Bruno, pelo link; tenho interesse na discussão aí contida. Gostaria de aproveitar o assunto, para trazer algumas questões que me ocuparam algum tempo atrás (para quem se interessar).

1. Como o primeiro teorema da incompletude poderia ser construído em sistemas formais da aritmética sem negação? Refiro-me, em particular, ao sistema introduzido por Krivtsov em "A Negationless Interpretation of Intuitionistic Axiomatic Theories".
2. E quanto ao segundo, já que neste sistema há apenas uma implicação quantificada, com a propriedade de que o antecedente sempre é satisfeito para um certo x (devido ao critério de syntactical non-nullity)?
3. Além disso, a prova do primeiro teorema demonstra a indecidibilidade da sentença G levando a hipótese da decidibilidade (seja de G ou de ¬G) a uma contradição. Para um intuicionista que não aceita que a refutação (P → ⊥) seja de fato o sentido da negação na matemática (penso na linha de Freudenthal, Griss, ...) e que vão trabalhar com axiomas para a relação de diferença (no lugar da negação), não me é claro qual seria a interpretação correta do teorema neste caso. Se alguém tiver algo a dizer, sou grato desde já.

Abraços,

Anderson
FFLCH/USP

[Fernando Yamauti]

 Olá a todos,

  Primeiramente, só queria levantar dois pontos.

 1) Eu, como havia comentado aqui ou na HoTT Café (não me lembro ao certo), também achava que \neg \neg G somente poderia ser considerada verdadeira, mas fui chamado a atenção (pelo Matt Oliveri) de que G já é construtivamente verdadeira: uma prova de G leva a uma contradição e, portanto, G não é provável é verdadeiro, logo G é verdadeiro.

 2) Com relação ao comentário do Rodrigo, a melhor definição de verdade no intuicionismo que achei até agora é a dada por realizações através funções parciais recursivas, a realização de Kleene (uma exposição breve usando lambda termos não tipados, https://www.fing.edu.uy/~amiquel/intro-kleene.pdf) ou, mais geralmente, as meaning explanations do ML (http://www.cs.tufts.edu/~nr/cs257/archive/per-martin-lof/constructive-math.pdf), que nunca foi escrita formalmente até onde eu saiba. Lembrando, funções parciais recursivas, lambda termos (untyped) e máquinas de Turing são a mesma coisa. Nesse caso, qualquer \PI_1^0 fórmula é trivialmente verdadeira. Em particular, G é canonicamente verdadeira. Como G é verdadeira, \neg Prov (G) é verdadeira. Isso significa exatamente que qualquer máquina de Turing não realiza Prov (G).

 

 Agora, com relação a questão em geral. Para enunciar e provar a incompletude parece mais fácil provar na categoria sintática. Existe um argumento do Lawvere de diagonalização e e uma prova da indefinibildade da verdade (no caso Booleano) para categorias cartesianas fechadas (http://tac.mta.ca/tac/reprints/articles/15/tr15.pdf). Acho que essa foi a sugestão pelo comentário dos pretopos aritméticos. Mas vale notar que mesmo um topos elementar com números naturais não tem todos os tipos indutivos (ele não precisa ter todas as algebras livres sobre uma teoria algébrica infinitaria), então acho que um pretopos aritmético ainda é insuficiente para um enunciado geral. Também existiriam mais problemas para o caso intensional (por exemplo, deixar tudo fibrante  e requerir quocientes homotópicos e blá, blá , blá...)

  Abs.,

  Fernando

  

--

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

[Francisco Antonio Doria]

Posso fazer uma observação?

Para teorias S com um conjunto recursivamente enumerável de teoremas (e mais outras condições simples, tipo ``aritmética suficiente'') existem infinidades de sentenças indecidíveis. E todas,  se o desejarmos, com significado matemático sensato. Um exemplo (em ZFC, suposto consistente e sound) de que gosto muito: podemos escrever as tábuas de um conjunto infinito X de máquinas de Turing tais que a sentença ``X é um conjunto de máquinas de Turing polinomiais no tempo'' é indecidível em tal ZFC. E é óbvio que esse conjunto só tem máquinas polinomiais. 

Ah, essa sentença não é Pi^0_1. 

Estamos agora catando uma sentença indecidivel em todos esses sistemas S. Simples e com significado matemático óbvio. 

2017-06-29 10:58 GMT-03:00 Fernando Yamauti <fgya...@gmail.com>:

 Olá a todos,

  Primeiramente, só queria levantar dois pontos.

 1) Eu, como havia comentado aqui ou na HoTT Café (não me lembro ao certo), também achava que \neg \neg G somente poderia ser considerada verdadeira, mas fui chamado a atenção (pelo Matt Oliveri) de que G já é construtivamente verdadeira: uma prova de G leva a uma contradição e, portanto, G não é provável é verdadeiro, logo G é verdadeiro.

 2) Com relação ao comentário do Rodrigo, a melhor definição de verdade no intuicionismo que achei até agora é a dada por realizações através funções parciais recursivas, a realização de Kleene (uma exposição breve usando lambda termos não tipados, https://www.fing.edu.uy/~amiquel/intro-kleene.pdf) ou, mais geralmente, as meaning explanations do ML (http://www.cs.tufts.edu/~nr/cs257/archive/per-martin-lof/constructive-math.pdf), que nunca foi escrita formalmente até onde eu saiba. Lembrando, funções parciais recursivas, lambda termos (untyped) e máquinas de Turing são a mesma coisa. Nesse caso, qualquer \PI_1^0 fórmula é trivialmente verdadeira. Em particular, G é canonicamente verdadeira. Como G é verdadeira, \neg Prov (G) é verdadeira. Isso significa exatamente que qualquer máquina de Turing não realiza Prov (G).

 

 Agora, com relação a questão em geral. Para enunciar e provar a incompletude parece mais fácil provar na categoria sintática. Existe um argumento do Lawvere de diagonalização e e uma prova da indefinibildade da verdade (no caso Booleano) para categorias cartesianas fechadas (http://tac.mta.ca/tac/reprints/articles/15/tr15.pdf). Acho que essa foi a sugestão pelo comentário dos pretopos aritméticos. Mas vale notar que mesmo um topos elementar com números naturais não tem todos os tipos indutivos (ele não precisa ter todas as algebras livres sobre uma teoria algébrica infinitaria), então acho que um pretopos aritmético ainda é insuficiente para um enunciado geral. Também existiriam mais problemas para o caso intensional (por exemplo, deixar tudo fibrante  e requerir quocientes homotópicos e blá, blá , blá...)

  Abs.,

  Fernando

  

Em 29 de junho de 2017 07:01, Bruno Bentzen <b.be...@hotmail.com> escreveu:

Olá pessoal,

Venho acompanhando a thread "How do we construct the Gödel’s sentence in Martin-Löf type theory?" no MathOverflow 

https://mathoverflow.net/q/272982/58734

que tem sido bem popular desde os últimos dias (e contado com a participação da Valéria e do Dana Scott).

Penso que talvez a discussão seja de interesse para alguns dos colegas da lista.

Abraços,

Bruno

--

Bruno Bentzen

https://sites.google.com/site/bbentzena/

--
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 postar nesse grupo, envie um e-mail para logi...@dimap.ufrn.br.
Acesse esse grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
Para ver essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/c155c92b-0bce-4012-aa97-6b79c44e769d%40dimap.ufrn.br.

--
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+unsubscribe@dimap.ufrn.br.
Para postar nesse grupo, envie um e-mail para logi...@dimap.ufrn.br.
Acesse esse grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.

Para ver essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAJGvw-2_Lvk%2BxNXTi5a7vx4L_hK-4D_Z%3DyypkKJ%2BRUA3%2BfNp5w%40mail.gmail.com.

--

fad

ahhata alati, awienta Wilushati

[Bruno Bentzen]

Olá a todos,

 

Obrigado pelos excelentes comentários, também acho o assunto fascinante.

 

1) Agradeço em particular ao Rodrigo por me apontar o equívoco. É possível demonstrar sim construtivamente que sentença de Gödel é verdadeira, e não apenas que ela não pode ser falsa. Se vale a informação, o que me levou a sustentar o contrário anteriormente foi o seguinte: como sabemos, quando assumimos que uma proposição A é falsa e chegamos a uma contradição, construtivamente, apenas podemos provar que A não pode ser falsa. Mas isso, claro, vale apenas em geral. Quando A := ¬P ocorre como uma negação, por exemplo, podemos derivar A de volta através de  ¬¬A através da lei da tripla negação de Brouwer. O descuido, então, esta em esquecer que sentença de Gödel é, em essência, uma negação!

 

2) As indagações do Anderson também são muito interessantes. Me pergunto, contudo, se tais teorias formais da aritmética sem negação seriam capazes de satisfazer os requerimentos dos teoremas da incompletude. Em particular, verifica-se que a linguagem de tal teoria não é capaz de expressar todas as relações numéricas decidíveis (por exemplo, R(x,y) := x ≠ y), quer dizer, o conjunto de “verdades básicas de aritmética”  que a teoria pode demonstrar é razoavelmente limitado.

 

3) Acredito que esta seja essa a discussão na HoTT Cafe que o Fernando esteja se referindo, “Can the judgement (A true) be made into a proposition?”

 

https://groups.google.com/d/msg/hott-cafe/jyD2Bhc5GWo/UEzjWj0wAwAJ

 

Abraços,

Bruno

--

Bruno Bentzen

https://sites.google.com/site/bbentzena/

[Famadoria]

A sentença original de Gödel é Pi_1. Se juntarmos à teoria original todas as sentenças verdadeiras Pi_1, não se ganha nada em termos de provabilidade. Mas se juntarmos todas as Pi_2 verdadeiras obtemos uma teoria não r.e. mas completa na aritmética. 

Kleene, que eu saiba, foi quem primeiro estudou essas outras sentenças. 

Sent from my iPhone

Para ver essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/23459f67-99f7-42db-85b9-87198d98e2ed%40dimap.ufrn.br.

[Hermógenes Oliveira]

Anderson Nakano <anderso...@gmail.com> escreveu:

> Boa tarde, pessoal.

Olá, Anderson.

>
> [...]

>
> 1. Como o primeiro teorema da incompletude poderia ser construído em
> sistemas formais da aritmética sem negação? Refiro-me, em particular,
> ao sistema introduzido por Krivtsov em "A Negationless Interpretation
> of Intuitionistic Axiomatic Theories".

Não conheço o sistema de Krivtsov, mas gostaria de observar o seguinte.

A demonstração de Gödel não depende de nenhuma noção semântica, seja a
noção *semântica* de "negação" ou "verdade".

Dado que a lógica clássica pode ser interpretada na lógica mínima[#],
via lógica intuicionista, imagino que não seria difícil ajustar a noção
Gödeliana de representabilidade à um sistema "sem negação", por exemplo,
à um sistema no qual ¬A ≡ A → (1=0), com a noção de igualdade e
desigualdade (diferença) determinada por axiomas construtivos
adicionais.

Desde que o sistema formal em questão seja poderoso o suficiente para
representar sua própria sintaxe, é possivel diagonalizar e obtair daí
uma sentença indecidível.

Algo similar acontece com o teorema de Church: a tradução da lógica
clássica na lógica intuicionista é comumente usada para transferir o
resultado de indecidibilidade da lógica clássica de primeira ordem para
o caso intuicionista.

>
> [...]

>
> 3. Além disso, a prova do primeiro teorema demonstra a
> indecidibilidade da sentença G levando a hipótese da decidibilidade
> (seja de G ou de ¬G) a uma contradição. Para um intuicionista que não
> aceita que a refutação (P → ⊥) seja de fato o sentido da negação na
> matemática (penso na linha de Freudenthal, Griss, ...) e que vão
> trabalhar com axiomas para a relação de diferença (no lugar da
> negação), não me é claro qual seria a interpretação correta do teorema
> neste caso.

A interpretação sintática do teorema permanece inalterada.

Na minha hulmide opinião, interpretações semâmticas do teorema, que
apelam a noções semânticas como "verdade" ou alguma noção semântica de
"negação", *não fazem o menor sentido*. Mesmo no caso clássico.

Nota:

[#] Interpretações da lógica clássica na lógica intuicionista e mínima
foram exploradas por Kolmogorov, Bernays, Gentzen e Gödel, dentre
outros. Um apanhado geral dos resultados e traduções pode ser
encontrado em: D. Prawitz and P. E. Malmnäs. A survey of some
connections between classical, intuitionistic and minimal logic. In
H. Arnold Schmidt, K. Schütte, and H. J. Thiele, editors, Contributions
to Mathematical Logic, Proceedings of the Logic Colloquium, Hannover
1966, pages 215-229. North-Holland Publishing Company, 1968.

--
Hermógenes Oliveira

[Anderson Nakano]

Olá, Hermógenes. Muito obrigado pela resposta!

Uma pequena observação: nestes sistemas sem negação, não se trata apenas de tratar a negação como conectivo derivado (def., p. ex., ¬A ≡ A → (1=0)), mas de banir toda e qualquer "suposição não realizável" e, com isso, até mesmo o raciocínio hipotético (o "p → q") da matemática. Isso porque, vai alegar, digamos, o Freudenthal, uma suposição não realizada não é um "material construtivo" a partir do qual se poderia partir.

Além disso, salvo engano, nesses sistemas (chamemos de NA) não faz muito sentido a noção de ω-inconsistência (separada da de inconsistência), pois é possível provar que, se NA ⊢ ∃xA(x), então, para algum numeral n, NA ⊢ A(n).

[Rodrigo Freire]

Olá Hermógenes,

> A interpretação sintática do teorema permanece inalterada.
>
> Na minha hulmide opinião, interpretações semâmticas do teorema, que
> apelam a noções semânticas como "verdade" ou alguma noção semântica de
> "negação", *não fazem o menor sentido*. Mesmo no caso clássico.

Imagino que a "interpretação sintática do teorema" para um sistema S
(digamos, para a aritmética de Peano) seja: há (construtivamente) uma
sentença G tal que se S é (omega-)consistente, então G não é teorema e
~G não é teorema. É isso?

O problema é que só com essa "interpretação sintática do teorema" é
impossível distinguir o teorema de Godel de uma trivialidade
irrelevante como, por exemplo: Há uma sentença G da teoria de grupos
(suposta consistente) tal que G não é teorema e ~G também não. De
fato, sintaticamente, como sistemas formais sem algum tipo de
"interpretação semântica", a aritmética de Peano e a teoria de grupos
são o mesmo tipo de coisa. Onde estaria a diferença? De onde viria a
pretensão de completude da aritmética de Peano, e por que isso estaria
ausente na teoria de grupos, por exemplo?


Abraço
Rodrigo

[Hermógenes Oliveira]

Anderson Nakano <anderso...@gmail.com> escreveu:

> Olá, Hermógenes. Muito obrigado pela resposta!

Por nada.

> Uma pequena observação: nestes sistemas sem negação, não se trata
> apenas de tratar a negação como conectivo derivado (def., p. ex., ¬A
> ≡ A → (1=0)), mas de banir toda e qualquer "suposição não
> realizável" e, com isso, até mesmo o raciocínio hipotético (o "p →
> q") da matemática. Isso porque, vai alegar, digamos, o Freudenthal,
> uma suposição não realizada não é um "material construtivo" a partir
> do qual se poderia partir.

Isso me parece exatamente a situação que temos no caso da lógica
mínima onde não temos o princípio ECQ (ex contradictione quodilibet)
que nos permitiria extrair conseqüências de "suposições não
realizáveis".

Em resumo, o enredo da minha sugestão seria o seguinte.

A negação clássica pode ser interpretada na lógica intuicionista por
meio da conhecida tradução de Gentzen-Gödel. Porém, ainda resta o
princípio ECQ, característico da negação nos sistemais intuicionistas
usuais, mas que não é aceito por construtivistas como Freudenthal e
Griss.

Contudo, ECQ pode ser interpretado numa lógica mínima por meio da
disjunção. Aqui, em termos gerais, traduzimos uma sentença A por A∨⊥.
Grosso modo, isto significa que, tendo em vista a regra de introdução
da disjunção, A pode ser obtido pelas vias mínimas normais *ou por
meio de ⊥*, simulando assim os raciocínios por ECQ. Note que "⊥" não
precisa ser considerada uma constante lógica, mas pode ser uma
sentença refutável qualquer (de acordo com os axiomas aritméticos
subjacentes) como, por exemplo, 1=0.

É claro, resta saber ainda se os sistemas sem negação aos quais você
se refere permitem alguma noção de refutação, ou se há apenas a noção
de demonstração. Isto é, resta saber se uma demostração de 1≠0
significa o mesmo que uma refutação de 1=0, ou se as noções de
igualdade e desigualdade (diferença) são *completamente independentes*
(i.e. não há nenhum axioma aritimético subjacente conectando, ou
contrastando, as duas noções, o que seria bastante estranho).

Enfim, ao que me parece, a aplicação dos resultados de Gödel a esses
sistemas sem negação dependeria mais da teoria aritmética subjacente
do que dos conectivos lógicos disponíveis.

Não estou certo se a minha sugestão estaria correta, mas, independente
disso, a questão que você levanta é bastante interessante.

--
Hermógenes Oliveira

[Hermógenes Oliveira]

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

> Olá Hermógenes,

Olá, Rodrigo.

> Imagino que a "interpretação sintática do teorema" para um sistema S
> (digamos, para a aritmética de Peano) seja: há (construtivamente)
> uma sentença G tal que se S é (omega-)consistente, então G não é
> teorema e ~G não é teorema. É isso?

Sim. Em linhas gerais, foi isso o que Gödel demonstrou em 1931, não?

> O problema é que só com essa "interpretação sintática do teorema" é
> impossível distinguir o teorema de Godel de uma trivialidade
> irrelevante como, por exemplo: Há uma sentença G da teoria de grupos
> (suposta consistente) tal que G não é teorema e ~G também não. De
> fato, sintaticamente, como sistemas formais sem algum tipo de
> "interpretação semântica", a aritmética de Peano e a teoria de
> grupos são o mesmo tipo de coisa. Onde estaria a diferença? De onde
> viria a pretensão de completude da aritmética de Peano, e por que
> isso estaria ausente na teoria de grupos, por exemplo?

O estado medíocre do meu atual conhecimento de álgebra não me permite
comentar com precisão o exemplo que você citou. Mas eu me interessei
pelo exemplo e também planejo remediar a minha ignorância de álgebra,
portanto referências pontuais são bem-vindas (pode enviar em privado).

O que posso comentar no momento, assumindo aqui que o exemplo
algébrico não é essencial à questão, é que, no caso de sistemas como
AP (aritmética de Peano), no qual o vocabulário é exclusivamente
matemático e os axiomas são tomados como determinantes exaustivos das
noções matemáticas envolvidas, haveria sim a pretensão de que o
sistema formal possa decidir qualquer sentença matemática A por meio
de uma derivação de A ou de uma refutação de A.

--
Hermógenes Oliveira

[Rodrigo Freire]

Ok, Hermógenes, então podemos focar na questão levantada.

 

O problema é que só com essa "interpretação sintática do teorema" é
impossível distinguir o teorema de Godel de uma trivialidade
irrelevante como, por exemplo: Há uma sentença G da teoria de grupos
(suposta consistente) tal que G não é teorema e ~G também não. De
fato, sintaticamente, como sistemas formais sem algum tipo de
"interpretação semântica", a aritmética de Peano e a teoria de
grupos são o mesmo tipo de coisa. Onde estaria a diferença? De onde
viria a pretensão de completude da aritmética de Peano, e por que
isso estaria ausente na teoria de grupos, por exemplo?

O estado medíocre do meu atual conhecimento de álgebra não me permite
comentar com precisão o exemplo que você citou.  Mas eu me interessei
pelo exemplo e também planejo remediar a minha ignorância de álgebra,
portanto referências pontuais são bem-vindas (pode enviar em privado).

Considere G a sentença 'para todos x e y, x.y=y.x'. Essa sentença é indecidível na teoria de grupos, mas ninguém chama isso de teorema da incompletude da teoria de grupos.

 

O que posso comentar no momento, assumindo aqui que o exemplo
algébrico não é essencial à questão, é que, no caso de sistemas como
AP (aritmética de Peano), no qual o vocabulário é exclusivamente
matemático e os axiomas são tomados como determinantes exaustivos das
noções matemáticas envolvidas, haveria sim a pretensão de que o
sistema formal possa decidir qualquer sentença matemática A por meio
de uma derivação de A ou de uma refutação de A.

O vocabulário da teoria de grupos é exclusivamente matemático, e os axiomas são tomados como determinantes exaustivos das noções matemáticas envolvidas (operação de grupo), muito mais que no caso da aritmética. Ainda assim, não há pretensão de completude.

Essa "leitura sintática" trivializa o teorema de Godel. 

Abraço

Rodrigo

[Hermógenes Oliveira]

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

>
> [...]

>
> Essa "leitura sintática" trivializa o teorema de Godel.

Isso é obviamente falso, pois a demonstração de Gödel no artigo de
1931 é completamente sintática, mas *não* é trivial.


--
Hermógenes Oliveira

[Hermógenes Oliveira]

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

>
> [...]
>

> O vocabulário da teoria de grupos é exclusivamente matemático, e os
> axiomas são tomados como determinantes exaustivos das noções
> matemáticas envolvidas (operação de grupo), muito mais que no caso
> da aritmética.

Não sei se compreendi muito bem a analogia.

Normalmente, a noção de grupo é definida como *uma* operação sob um
conjunto de elementos que satisfazem determinados axiomas. Porém,
diversas operações *distintas* satisfazem os axiomas de grupo. Em que
sentido poderíamos dizer que os axiomas determinam exaustivamente a
operação?

Em contraste, você conseguiria ver como os axiomas de AP determinariam
exaustivamente (ou pelo menos, possuem a pretensão de determinar
exaustivamente) a noção de número natural?


--
Hermógenes Oliveira

[jyb]

Gostaria de apontar que o Saul Kripke apresentou em Paris uma prova semantica do teroema de Gödel

"A Model Theoretic Approach to Gödel's Theorem"

http://www.logic-in-question.org/

Bem detalhada mas ainda não publicada, todavia a palestra foi gravada ...

Saudações

JYB

[Rodrigo Freire]

>>
>> [...]
>>
>> O vocabulário da teoria de grupos é exclusivamente matemático, e os
>> axiomas são tomados como determinantes exaustivos das noções
>> matemáticas envolvidas (operação de grupo), muito mais que no caso
>> da aritmética.
>
> Não sei se compreendi muito bem a analogia.
>
> Normalmente, a noção de grupo é definida como *uma* operação sob um
> conjunto de elementos que satisfazem determinados axiomas. Porém,
> diversas operações *distintas* satisfazem os axiomas de grupo. Em que
> sentido poderíamos dizer que os axiomas determinam exaustivamente a
> operação?
>

> Em contraste, você ver como os axiomas de AP determinariam

> exaustivamente (ou pelo menos, possuem a pretensão de determinar
> exaustivamente) a noção de número natural?
>

Não. Não há um predicado para "número natural" que ocorre nos axiomas da aritmética, assim como não há predicado para "elemento de grupo" ou "permutação" na teoria de grupos. Alem disso, apelar para uma "noção de número natural" que aritmética pretende capturar já é introduzir um elemento semântico que vai além da sintaxe, justamente para avaliar a "limitação do formalismo". Não há diferença puramente formal entre o caso aritmético e o caso da teoria de grupos, o que trivializaria sim a relevância fundacional do teorema na ausência de algum elemento semântico (pois o caso da incompletude dos grupos é irrelevante).

[Bruno Bentzen]

Oi Hermógenes,

Em linhas gerais, acho que o ponto é que muitas teorias são também incompletas de uma forma “boring”.

 

Há até mesmo casos em que a sentença indecidível em questão é falsa na interpretação pretendida. Aqui é interessante observar que, na aritmética de Robinson, Q, por exemplo, a sentença falsa ‘∃x (s(x) = x)’ é indecidível.¹

 

Diria que privar os teoremas da incompletude de seu aspecto semântico, é, de certa forma, desmembrar um de seus aspectos mais fascinantes: não se trata apenas de demonstrar a incompletude, de apresentar uma sentença indecidível; trata-se de construir uma sentença verdadeira mas indemonstrável, provando assim que em tais teorias da aritmética “razoáveis”,  como PA, nunca poderão cumprir a ambição de capturar o conjunto de sentenças verdadeiras de sua interpretação pretendida.

 

Abraços,

Bruno

 

¹Construa uma interpretação não-standard cujo domínio compreenda os números naturais e um único elemento intruso, c (digamos, Julío César). Agora defina a função sucessor da seguinte forma: s’(n)=s(n) para n ∈ ℕ, onde ‘s’ denota a função sucessor usual, e, sobretudo, s’(c)=c. Além disso, defina: m +’ n = m + n para todo m,n ∈ ℕ, onde ‘+’ denota a adição usual, mas n +’ c = c +’ n = c. Similarmente, estipulemos o seguinte (além da definição usual da multiplicação para números naturais): n ×’ c = c ×’ n = 0 se n for 0; n ×’ c = c ×’ n = c caso contrário, para n ∈ ℕ. Essa interpretação respeita todos os axiomas de Q, contudo a sentença ‘∃x (s(x) = x’ é verdadeira, visto que s’(c)=c.

--

Bruno Bentzen

https://sites.google.com/site/bbentzena/

[Hermógenes Oliveira]

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

> Não. Não há um predicado para "número natural" que ocorre nos

> axiomas da aritmética [...]

????

Então eu não sei o que você entende por axiomas de Peano. No meu
livro, o primeiro axioma já reza:

1. O zero é um número natural.

:-)

>
> [...]

>
> Alem disso, apelar para uma "noção de número natural" que aritmética
> pretende capturar já é introduzir um elemento semântico que vai além

> da sintaxe [...]

Eu concordo com isso (talvez trocando "introduzir" por "reconhecer" ou
"aceitar").

> [...] justamente para avaliar a "limitação do formalismo".

Mas *não* concordo com isso, ao menos da forma como está expresso.

O fato de que reconhecemos noções pré-teóricas (supostamente de
caráter semântico, embora não exatamente num sentido técnico do termo
"semântico", e.g. Teoria dos Modelos) que nos guiam na formulação de
sistemas formais não implica, *por si só*, limitações inerentes do
formalismo.

> Não há diferença puramente formal entre o caso aritmético e o caso
> da teoria de grupos, o que trivializaria sim a relevância
> fundacional do teorema na ausência de algum elemento semântico (pois
> o caso da incompletude dos grupos é irrelevante).

Bem, o teorema, conforme demonstrado em 1931, é puramente sintático e
responde a uma importante questão de *decidibilidade formal* que havia
sido formulada e estudada no contexto da Escola Hilbertiana desde o
início do século passado. Portanto, acho que podemos concordar que o
teorema, mesmo na sua formulação original sintática, *não* é trivial.

Quanto à uma suposta "relevância fundacional" que só poderia ser
reconhecida numa interpretação semântica do teorema, eu não saberia
dizer. Como observei anteriormente, as interpretações semânticas do
teorema, assim como tentativas de formular e demonstrar o teorema em
termos semânticos não fazem o menor sentido para mim. Claro, esta
observação pode ser tomada como nada além de evidência da minha
própria ignorância e/ou incapacidade. Para mim, contudo, ela
constitui evidência de que a interpretação semântica do teorema,
juntamente com seus usos e abusos em alegações sobre os "limites da
matemática" (ou formalismo) e "existência de sentenças verdadeiras
indemonstráveis", não passam de histórias pra boi dormir. Porém, eu
continuo sinceramente buscando evidências contrárias, e, em vista das
informações do JYB, estou curioso para saber o que Kripke tem a dizer
sobre o assunto. Até agora, contudo, apresentações "semânticas" do
teorema de Gödel tem me decepcionado, inclusive aquelas presentes no
excelente livro de Smullyan sobre o assunto.


--
Hermógenes Oliveira

[Rodrigo Freire]

Olá Bruno e Hermógenes,

O Bruno explicou bem, mas ainda vou resumir o meu ponto de modo direto. 

Acho que estamos desviando da questão central, Hermógenes. Meu ponto é muito simples:

- Não há como distinguir a incompletude da aritmética da incompletude da teoria de grupos sem reconhecer um elemento semântico. 

Você pode chamar ou conceber esse elemento semântico de modo diverso: Pode chamar de noção de número, de modelo standard, de verdade, etc. Tanto faz.

Aceitando o ponto acima, e sabendo da irrelevância da incompletude trivial da teoria de grupos, concluímos que, quando desprovido do aspecto semântico, o teorema da incompletude não tem relevância. Isso está em oposição com o que foi dito que interpretações semânticas do teorema não querem dizer nada.

Não. Não há um predicado para "número natural" que ocorre nos
axiomas da aritmética [...]

????

Então eu não sei o que você entende por axiomas de Peano.  No meu
livro, o primeiro axioma já reza:

1. O zero é um número natural.

:-)

Entendo a axiomatização como sistema formal de primeira ordem de tipo usual, tal como se encontra no livro do Shoenfield, página 204. Os símbolos primitivos são 0, S, +, ., <. Não há predicado para número. O nome da teoria encontra-se nessa mesma página: Aritmética de Peano.

Abraço

Rodrigo

[Fernando Yamauti]

Em 3 de julho de 2017 09:40, jyb <jyb.lo...@gmail.com> escreveu:

Gostaria de apontar que o Saul Kripke apresentou em Paris uma prova semantica do teroema de Gödel

"A Model Theoretic Approach to Gödel's Theorem"

http://www.logic-in-question.org/

Bem detalhada mas ainda não publicada, todavia a palestra foi gravada ...

Saudações

JYB

  Oi Jean-Yves,

  A gravação está disponível em algum lugar online? Eu falhei em encontrar videos no site da conferencia. Slides já seriam o suficiente (caso ele tenha usado), mas também não achei algo do tipo.

  Abs.,

  Fernando

[Marcelo Finger]

Caros.

Quando o Kripke esteve na Unicamp há alguns anos, acho que ele
apresentou um esboço desta prova. SE não me engano, naquela época p
único escrito sobre isso era um relatório de outro pesquisador sobre a
prova de Kripke. Ele começava contando o que se sabia sobre o assunto
ANTES de Goedel.

Alguém mais se lembra disso?

[]s

> --
> 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 postar nesse grupo, envie um e-mail para logi...@dimap.ufrn.br.
> Acesse esse grupo em
> https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
> Para ver essa discussão na Web, acesse

> https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAJGvw-2VBAoYxTAtVz9NOBUe8uQ77Yuxe30tR-wKiqQkYX1asg%40mail.gmail.com.



--
Marcelo Finger
Departament of Computer Science, IME
University of Sao Paulo
http://www.ime.usp.br/~mfinger