(In)decidibilidade e (In)completude

52 views
Skip to first unread message

Hermógenes Oliveira

unread,
Sep 23, 2016, 4:06:57 AM9/23/16
to logi...@dimap.ufrn.br
Recentemente, João Marcos escreveu:

> Não são todos que podem se gabar de ter um teorema que leva o seu nome
> (https://en.wikipedia.org/wiki/Trakhtenbrot%27s_theorem).

Corrijam-me se estiver errado, mas parece que o parágrafo seguinte é
muito problemático (retirado da entrada sobre o teorema na Wikipédia
inglesa):

"It is considered a very important result, since it implies that the
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 parágrafo parece confundir (in)completude semântica com in(completude)
sintática, isto é, (in)decidibilidade. 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.

O teorema de Trakhtenbrot, por outro lado, apenas reforça para o caso
finito o resultado obtido por Church no que concerne a indecidibilidade
da lógica de predicados.

Ultimamente, tenho encontrado muitas confusões envolvendo
completude/incompletude. Na maioria das vezes, implícitas em
formulações enigmáticas como a do parágrafo citado acima.

Estaria muito agradecido se algum colega pudesse me passar informações
ou referências históricas sobre como a "indecidibilidade"
(unentscheidbare Sätze) de Gödel se tornou incompletude (estou à procura
de alguém em quem jogar a culpa).

--
Hermógenes Oliveira

taxinomia

unread,
Sep 23, 2016, 10:13:19 AM9/23/16
to LOGICA-L, hermogene...@student.uni-tuebingen.de
Caro Hermógenes,

Conhece este artigo?
http://www.tandfonline.com/doi/pdf/10.1080/01445340.2013.816555

Acredito que ele diz respeito à sua questão.

Abraço,
Bruno M..

Alfio Ricardo de B Martini

unread,
Sep 23, 2016, 2:49:35 PM9/23/16
to LOGICA-L, hermogene...@student.uni-tuebingen.de

Olá Bruno,


Uma leitura das primeiras páginas sugere  ser este um artigo excelente.

Claro, preciso o suficiente,  e de fácil leitura. Thanks a lot!


Prof. Alfio Martini
Coordenador do Curso de Ciência da Computação


From: taxinomia <taxi...@gmail.com>
Sent: 23 September 2016 11:13:19
To: LOGICA-L
Cc: hermogene...@student.uni-tuebingen.de
Subject: [Logica-l] Re: (In)decidibilidade e (In)completude
 
--
Você recebeu essa mensagem porque está inscrito 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+u...@dimap.ufrn.br.
Para postar nesse grupo, envie um e-mail para logi...@dimap.ufrn.br.
Acesse esse grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
Para ver essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/6de1f197-e877-41d0-b672-ced86db92ae9%40dimap.ufrn.br.

Rodrigo Freire

unread,
Sep 23, 2016, 6:48:02 PM9/23/16
to LOGICA-L, hermogene...@student.uni-tuebingen.de
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). Claro que também temos, como corolário, que a validade em estruturas finitas não é recursiva (decidível). 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.

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.

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. 

Abraço
Rodrigo



Hermógenes Oliveira

unread,
Sep 24, 2016, 6:23:00 AM9/24/16
to logi...@dimap.ufrn.br
Salve, Rodrigo!

Rodrigo Freire <freir...@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

Rodrigo Freire

unread,
Sep 24, 2016, 7:03:37 AM9/24/16
to Lista acadêmica brasileira dos profissionais e estudantes da área de LOGICA
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






 









--
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+unsubscribe@dimap.ufrn.br.
Para postar neste grupo, envie um e-mail para logi...@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.

Hermógenes Oliveira

unread,
Sep 24, 2016, 10:16:17 AM9/24/16
to logi...@dimap.ufrn.br
Rodrigo Freire <freir...@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

Rodrigo Freire

unread,
Sep 24, 2016, 11:00:13 AM9/24/16
to Lista acadêmica brasileira dos profissionais e estudantes da área de LOGICA
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





















--
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+unsubscribe@dimap.ufrn.br.
Para postar neste grupo, envie um e-mail para logi...@dimap.ufrn.br.
Visite este grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
Reply all
Reply to author
Forward
0 new messages