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.
