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
On Thu, Dec 19, 2019 at 4:52 AM Famadoria <famado...@gmail.com> wrote:
> Vê o teorema de Kleene, de novo.
>
> Sent from my iPhone
>
> On 19 Dec 2019, at 08:36, Joao Marcos <botoc...@gmail.com> wrote:
>
> >> 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
> >
> >
> >>> On 18 Dec 2019, at 13:03, Joao Marcos <botoc...@gmail.com> wrote:
> >>>
> >>> 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
> >>>
> >>>> On Wed, Dec 18, 2019 at 10:31 AM Joao Marcos <botoc...@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
> >>>
> >>>
> >>>
> >>> --
> >>> http://sequiturquodlibet.googlepages.com/
> >>>
> >>> --
> >>> 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 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
> .
> >
> >
> >
> > --
> > http://sequiturquodlibet.googlepages.com/
>
> --
> 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 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
> .
>
--
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 ver esta discussão na web, acesse
https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAESt%3DXuwXwc4GskKH7VMgikB71uz7BADT9TqVZdvng26HzZn%2BQ%40mail.gmail.com.
