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 > On 30 Jun 2017, at 14:22, Bruno Bentzen <b.bent...@hotmail.com> wrote: > > 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/ > >> On Thursday, June 29, 2017 at 7:53:09 PM UTC+8, Rodrigo Freire wrote: >> 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 >> >>> Em 29 de jun de 2017, às 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+unsubscr...@dimap.ufrn.br. > Para postar nesse grupo, envie um e-mail para logica-l@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/23459f67-99f7-42db-85b9-87198d98e2ed%40dimap.ufrn.br. -- Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos Grupos do Google. Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+unsubscr...@dimap.ufrn.br. Para postar neste grupo, envie um e-mail para logica-l@dimap.ufrn.br. Visite este grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/. Para ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/E6757D0B-0653-4871-9BAC-48408346741D%40gmail.com.
