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