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.

Responder a