Salve Hermógenes,
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. 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. 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. Abraço Rodrigo 2016-09-24 7:22 GMT-03:00 Hermógenes Oliveira < hermogenes.olive...@student.uni-tuebingen.de>: > Salve, Rodrigo! > > Rodrigo Freire <freires...@gmail.com> escreveu: > > > Caros, > > > > Corrigindo: > > > > Afinal, a completude semântica da lógica de predicados no caso > > finito é apenas um caso especial da completude semântica para o > > caso geral (infinito), demonstrado por Gödel na sua tese de > > doutorado. > > > > Não. Segundo o teorema de Trakhtenbrot, não há sistema dedutivo cujos > > teoremas são exatamente as sentenças válidas (para uma linguagem > > canônica) em todas as estruturas finitas. Essa propriedade também é > > chamada de incompletude (semântica, como você diz). > > Eu certamente não chamaria isso de incompletude semântica! Para ser > mais claro, o que eu chamo de (in)completude semântica (segundo o que > creio ser a prática mais comum) é a propriedade demonstrada por Gödel em > 1929 e que normalmente é ensinada em cursos de lógica de predicados > juntamente com correção (soundness), embora atualmente se prefira > métodos diferentes daqueles usados por Gödel, como, por exemplo, > conjuntos de Hintikka, no caso do livro conhecido de Smullyan.[1] > > Resumindo, em termos gerais: > > Completude (semântica): Para toda sentença válida há uma demonstração no > sistema dedutivo. Ou, toda sentença válida é demonstrável. > > Embora eu esteja incerto, pois a sua formulação me parece um pouquinho > imprecisa, eu chamaria a propriedade que você enuncia de > *indecidibilidade* mesmo. Isto é, "não há sistema dedutivo cujos > teoremas são exatamente as sentenças válidas em todas estruturas > finitas" significa, assumindo um sistema dedutivo comum (sem indução > transfinita ou qualquer outra regra infinita), que validade é > indecidível em todas estruturas finitas. > > Talvez eu não tenha sido claro o suficiente na minha mensagem original. > Para esclarecer um pouco mais, o problema com o parágrafo da entrada da > Wikipédia inglesa é que ele relaciona o resultado de Trakhtenbrot com > completude no sentido de Gödel (1929), inclusive com um vínculo à > entrada correspondente, apesar do teorema de Trakhtenbrot não ter nada a > ver com completude nesse sentido. Cito novamente: > > "It is considered a very important result, since it implies that the > completeness theorem > [https://en.wikipedia.org/wiki/G%C3%B6del%27s_completeness_theorem] > (that is fundamental to First-Order Logic) does not hold in the finite > case. Also it seems counter intuitive that being valid over all > structures is 'easier' than over just the finite ones." > > O que é pior, o parágrafo sugere que completude valeria para o caso > infinito mas não para o caso finito, o que é completamente absurdo pois > o teorema é demonstrado para o caso geral do qual validade em estruturas > finitas é apenas um caso específico! > > > Se por incompletude sintática você quer dizer o mesmo que negação > > incompletude (não vale que uma entre A e ~A é teorema, para qualquer > > sentença A), então incompletude sintática também não é o mesmo que > > indecidibilidade. Há contraexemplos triviais: a lógica proposicional é > > decidível e não é negação completa, a lógica de primeira ordem com um > > símbolo de propriedade (unário) também é contraexemplo, a teoria dos > > domínios com no máximo k>1 elementos com igualdade apenas, etc. > > Eu estou ciente dessas questões. Veja: > > https://groups.google.com/a/dimap.ufrn.br/d/msg/logica-l/ > Y2ZEqSBL7TQ/doXMXsEMAwAJ > > Com relação à terminologia, eu prefiro chamar o primeiro teorema de > Gödel (1931) de teorema de *indecidibilidade*. E mais, creio que se > referir a este teorema como teorema de *incompletude* arrisca uma > catástrofe comunicativa, pois conecta este resultado de 1931 com o > resultado de completude de 1929 que trata de algo inteiramente distinto. > A distinção está clara para quem compreende os artigos originais de > Gödel e conhece a literatura de base com a qual ele trabalhou > (principalmente o "Grundzüge der theoretischen Logik" de Hilbert e > Ackerman). Porém, Deus sabe lá o porquê, muitos passaram a chamar o > resultado de 1931 de teorema de incompletude... > > Contudo, para poder me comunicar com aqueles que preferem "incompletude" > em vez de "indecidibilidade", costumo distinguir entre (in)completude > semântica e sintática, sendo (in)completude semântica aquela de Gödel > (1929) e incompletude sintática aquilo que gostaria de chamar de > "indecidibilidade". > > O raciocínio para essa imprecisa terminologia de compromisso é > justamente aquela que você indicou acima: Para linguagens calibradas > para a matemática (aritmética), é natural presumir aquilo que você > chamou de "negação incompletude" (uma vez que não há sentenças > contingentes). Reconheço que essa terminologia é completamente > insatisfatória, mas essa é a melhor justificativa que eu conheço para se > usar a terminologia "incompletude" quando aplicada ao teorema de Gödel > (1931). > > > A demonstração do teorema de Trakhtenbrot é simples: > > > > Dada uma máquina de Turing m e uma entrada n, há uma sentença canônica > > A_mn que descreve a operação de m com entrada n na interpretação > > padrão. A sentença A_mn tem modelo finito se e somente se m para com a > > entrada n. De fato, por um lado, A_mn é satisfeita na subestrutura da > > interpretação padrão cujo domínio é o intervalo de operação de m com a > > entrada n. Por outro lado, é fácil ver que se m não para com a entrada > > n então A_mn só tem modelos infinitos. Segue-se do problema da parada > > que a satisfatibilidade em estruturas finitas não é recursiva. Como a > > satisfatibilidade em estruturas finitas é recursivamente enumerável (a > > satisfatibilidade em cada estrutura finita é recursiva), temos que a > > validade em estruturas finitas não é recursivamente enumerável. > > Portando, não há sistema dedutivo (recursivamente enumerável) que > > tenha como teoremas exatamente as sentenças válidas em todas as > > estruturas finitas. Fim. > > Isso demonstra a *indecidibilidade* do conjunto das sentenças válidas em > todas as estruturas finitas. > > > Referências: Alguns livros de lógica "undergraduate" contém os > > detalhes. Ebbinghaus, Flum e Thomas é um deles. Pessoalmente, gosto > > (mais) do Boolos, Burgess e Jeffrey, mas neste o teorema de > > Trakhtenbrot é enunciado em um exercício apenas. > > Eu consultei o livro de Ebbinghaus, Flum e Thomas. Ali, o teorema é > demonstrado como um teorema de indecidibilidade: > > "5.4 Trahtenbrot's Theorem. The set of first-order sentences > valid in all finite structures is not R-enumerable." p. 171 > > onde > > "W is said to be register-enumerable (abbreviated: R-enumerable) , if > there is a program which decides W" p. 160 (Definition 2.6) > > O manuscrito de Stephen Simpson que consta nas referências da entrada na > Wikipédia apresenta o teorema de Trakhtenbrot como um reforço do > resultado de Church (não mencionei isso na mensagem anterior pois > somente agora me dei conta do manuscrito): > > http://logic.amu.edu.pl/images/2/21/Churchtrakhtenbrot.pdf > > Saudações, > > -- > 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/87eg497g1v.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%2BnuwubapddmNq9p_POzQ7DoPnK4GqBW5UPiCWqsVm9bQ%40mail.gmail.com.
