Re: [Logica-l] How do we construct the Gödel’s sentence in Martin-Löf type theory?

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.

Re: [Logica-l] How do we construct the Gödel’s sentence in Martin-Löf type theory?

Em 3 de julho de 2017 09:40, jyb 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,

Re: [Logica-l] How do we construct the Gödel’s sentence in Martin-Löf type theory?

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

Re: [Logica-l] How do we construct the Gödel’s sentence in Martin-Löf type theory?

Rodrigo Freire 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. :-) [...]

Re: [Logica-l] How do we construct the Gödel’s sentence in Martin-Löf type theory?

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

Re: [Logica-l] How do we construct the Gödel’s sentence in Martin-Löf type theory?

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

Re: [Logica-l] How do we construct the Gödel’s sentence in Martin-Löf type theory?

Rodrigo Freire 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

Re: [Logica-l] How do we construct the Gödel’s sentence in Martin-Löf type theory?

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

Re: [Logica-l] How do we construct the Gödel’s sentence in Martin-Löf type theory?

Rodrigo Freire 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

Re: [Logica-l] How do we construct the Gödel’s sentence in Martin-Löf type theory?

Anderson Nakano 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

Re: [Logica-l] How do we construct the Gödel’s sentence in Martin-Löf type theory?

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.

Re: [Logica-l] How do we construct the Gödel’s sentence in Martin-Löf type theory?

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

Re: [Logica-l] How do we construct the Gödel’s sentence in Martin-Löf type theory?

Anderson Nakano 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

Re: [Logica-l] How do we construct the Gödel’s sentence in Martin-Löf type theory?

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

Re: [Logica-l] How do we construct the Gödel’s sentence in Martin-Löf type theory?

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,

Re: [Logica-l] How do we construct the Gödel’s sentence in Martin-Löf type theory?

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,

Re: [Logica-l] How do we construct the Gödel’s sentence in Martin-Löf type theory?

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

Re: [Logica-l] How do we construct the Gödel’s sentence in Martin-Löf type theory?

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

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

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