Caro Hermógenes, Também agradeço pela discussão em um tema que é de interesse. É raro.
Podemos resumir a situação assim: Seja X o conjunto das sentenças (em uma linguagem apropriada de primeira ordem) verdadeiras em todas as estruturas. Seja Y o conjunto das sentenças (em uma linguagem apropriada de primeira ordem) verdadeiras em todas as estruturas finitas. 1) X é recursivamente enumerável (teorema da completude, Godel, Henkin, Mal'cev) 2) X não é recursivo (teorema da indecidibilidade, Church, Turing) 3) Y não é recursivamente enumerável (Trakhtenbrot) 4) Y não é recursivo (Trakhtenbrot) Visto desse modo, 3) é a negação do correlato natural de 1) para estruturas finitas, por isso dizem que o teorema da completude não vale para a validade lógica *finita*. Abraço Rodrigo 2016-09-24 11:16 GMT-03:00 Hermógenes Oliveira < hermogenes.olive...@student.uni-tuebingen.de>: > Rodrigo Freire <freires...@gmail.com> escreveu: > > > Salve Hermógenes, > > Olá, Rodrigo. Obrigado pelo seu interesse na discussão. > > > Vamos tentar de novo. Você copiou a definição errada do Ebbinghaus, > > essa não é a 2.6. Você pegou o item (b) da 2.5, página 160, que > > corresponde a register-decidable (R-decidable), não > > register-enumerable (R-enumerable), e trocou as palavras > > register-decidable por register-enumerable. > > Você está certo. Na hora do copie-e-cole, eu acabei selecionando a > passagem errada. > > > Vou copiar aqui a definição correta de R-enumerable por conveniência: > > > > (b) W is said to be register-enumerable (R-enumerable) if there is a > > program which ***enumerates*** W. (Def. 2.6, página 160 ênfase minha) > > > > Aqui está toda a confusão: > > > > - W é recursivamente enumerável (ou R-enumerable, como diz o > > Ebbinghaus) **não** é o mesmo que W é recursivo. > > > > A decidibilidade de W é identificada com W é recursivo, não com W é > > recursivamente enumerável. Se W é recursivo, então W é recursivamente > > enumerável, mas não vale a volta. > > Sim, sim. Claro. Obrigado pelo esclarecimento. > > > Muito bem, agora vamos ao teorema de Trakhtenbrot: As sentenças > > válidas nas estruturas finitas não são todas demonstráveis em um > > sistema dedutivo (qualquer). É exatamente a negação da propriedade do > > teorema da completude: As sentenças válidas (em todas as estruturas) > > são todas demonstráveis em um sistema dedutivo apropriado. Não há esse > > problema que você aponta no parágrafo da wikipedia. O teorema da > > completude é formulado abstratamente nesses termos mesmo: O conjunto > > de sentenças válidas é recursivamente enumerável. > > > > A demonstração do Trakhtenbrot está feita: O conjunto de sentenças > > válidas nas estruturas finitas não é recursivamente enumerável. > > Portanto, não é o caso que toda sentença válida nas estruturas finitas > > seja demonstrável em um sistema dedutivo. Em particular, como um > > corolário *mais fraco*, o conjunto de sentenças válidas nas estruturas > > finitas não é decidível. > > Hum... Acho que entendo agora: > > Trakhtenbrot (estruturas finitas): validade *não é* recursivamente > enumerável (não é semi-decidível). > > Church + Gödel (completude): validade não é recursiva (decidível), porém > *é* recursivamente enumerável. > > Eu realmente havia interpretado o teorema errôneamente como asserindo > que a validade em estruturas finitas fosse indecidível, mas > semi-decidível (algo como um reforço do teorema de Church para estruturas > finitas). > > Obrigado pela aula, professor. > > Abraços, > > -- > Hermógenes Oliveira > > -- > 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/87vaxl5qom.fsf%40camelot.oliveira. > -- 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/CAExWzU%2BpM%2B%2BGm-mbf55E4Y2gCO057bjVEzm7Oip-2Ehi-D7zvQ%40mail.gmail.com.
