Lógica de segunda ordem

Origem: Wikipédia, a enciclopédia livre.

Na lógica matemática, a lógica de segunda ordem é uma extensão da lógica de primeira ordem, onde a própria lógica de primeira ordem é uma extensão de lógica proposicional .

Tanto a lógica de primeira ordem como a lógica de segunda ordem usam a idéia de universo do discurso ou domínio de discurso (normalmente chamado apenas de “domínio”). O domínio é um conjunto sobre os quais se pode quantificar. A lógica de primeira ordem inclui apenas variáveis e quantificadores sobre elementos individuais do domínio. Por exemplo, na sentença de primeira ordem $\forall x ( x \neq x + 1 )$ a variável $x$ é usada para representar um indivíduo arbitrário.

A lógica de segunda ordem é uma extensão da lógica de primeira ordem pela adição de variáveis e quantificadores sobre conjuntos de indivíduos. Por exemplo a sentença $\forall S\forall x (x \in S \lor x \notin S)$ diz que para todo o grupo $S$ de indivíduos e todo indivíduo x, ou $x$ pertence a $S$ ou não pertence (este é o princípio de bivalência). A versão mais geral da lógica de segunda ordem inclui ainda formas de quantificar sobre funções e outras variáveis como explanado na seção Sintaxe abaixo.

Índice

1 Poder expressivo da lógica de segunda ordem
2 Sintaxe
3 Semântica
4 Sistemas Dedutivos
5 Por que a lógica de segunda ordem não é redutível para a lógica de primeira ordem
6 Lógica de segunda ordem e resultados metalógicos
7 A história e o valor disputado da lógica de segunda ordem
8 Aplicações para a complexidade
9 Força do fragmento existencial
10 References

[editar] Poder expressivo da lógica de segunda ordem

A lógica de segunda ordem é mais expressiva que a lógica de primeira ordem. Por exemplo, se o domínio é o grupo de todos os números reais, alguém pode declarar usando a lógica de primeira ordem a existência de um aditivo inverso de cada número real pela escrita $\forall x \exists y (x + y = 0)$ mas é necessário a lógica de segunda ordem para sustentar a propriedade do limite mínimo superior para o conjunto dos números reais, onde para cada estado limitado, o conjunto dos números reais não vazio tem um limite supremo . Se o domínio é o conjunto dos números reais, a seguinte sentença na lógica de segunda ordem representa a propriedade do limite mínimo superior:

$\forall A [(\exists w (w \in A) \land \exists z\,\forall w ( w \in A \rightarrow w \leq z)) \rightarrow \exists x\,\forall y ([\forall w \in A ( w \leq y)] \leftrightarrow x \leq y)].$

Na lógica de segunda ordem, é possível escrever sentenças formais que dizem “o domínio é finito” ou “o domínio é de cardinalidade contável “ Para dizer que o domínio é finito, use a sentença que diz que toda função injetora que tem a si própria como domínio é sobrejetora. Para dizer que o domínio tem cardinalidade contável, use a sentença que diz que existe a bijeção entre cada dois infinitos subconjuntos do domínio. Isto não possibilita a caracterização da não finitude ou contabilidade na lógica de primeira ordem.

[editar] Sintaxe

A sintaxe da lógica de segunda ordem fala que expressões são fórmulas bem formadas. Em adição a sintaxe da lógica de primeira ordem, a lógica de segunda ordem inclui várias novas classes (algumas vezes chamados tipos) de variáveis. São elas:

A classe de variáveis que engloba grupo de indivíduos. Se “S “ é uma variável desta classe e “x” é um termo de primeira ordem então a expressão $x \in S$ (também escrita $S (x)$ ou $S x$ ) é uma fórmula atómica. Conjuntos de indivíduos podem também ser vistos como relações unitárias no domínio.

Para cada número natural “k” existe um conjunto de variáveis que engloba todas as relação k-árias sobre esses elementos. Se “R “ é uma relação k-ária e $x_1,x_2,\ldots,x_k$ são termos de primeira ordem então a expressão $R(x_1,\ldots,x_k)$ é uma fórmula atômica.

Para cada número natural “k” existe um conjunto de variáveis que engloba funções que pegam “k” elementos do domínio e retornam um único elemento deste. Se “f “ é semelhante a um símbolo de função k-ária e $x_1,\ldots,x_k$ são termos de primeira ordem então a expressão $f(x_1,\ldots,x_k)$ é uma função de primeira ordem.

Para cada das classes de variável bem definida, é permissível construir fórmulas superiores pelo uso dos quantificadores existenciais e/ou universais. Portanto existem várias classes de quantificadores, dois para cada conjunto de variável.

Uma sentença em lógica de segunda ordem, como em lógica de primeira ordem, é uma fórmula bem formada sem variáveis livres (sobre nenhuma classe).

Na lógica de segunda ordem “monadic”, apenas as variáveis para subconjuntos são adicionadas. A lógica de segunda ordem com todas as classes de variáveis precisamente descritas é algumas vezes chamada de lógica de segunda ordem total para distingui-la da versão “monadic”.

Exatamente como na lógica de primeira ordem, a lógica de segunda ordem pode incluir símbolos não lógicos em uma linguagem particular de segunda ordem. Estas estão, entretanto, restritas a que todos os termos que eles formam devam ser também, termos de primeira ordem (que podem ser substituídos for uma variável de primeira ordem) ou termos de segunda ordem (que podem ser substituídos for uma variável de uma classe apropriada).

[editar] Semântica

As semânticas da lógica de segunda ordem estabelecem o significado de cada sentença. Diferente da lógica de primeira ordem, que tem apenas um padrão semântico, existem duas semânticas diferentes que são comumente usadas para a lógica de segunda ordem: semânticas padrão e as semânticas de Henkin. Em cada uma dessas semânticas, as interpretações dos quantificadores e dos conectivos lógicos de primeira ordem são tais como na lógica de primeira ordem. Apenas os novos quantificadores sobre variáveis de segunda ordem precisam ter a semântica definida.

Nas semânticas padrão, os quantificadores abrangem todos os grupos ou funções de uma classe apropriada. Portanto, uma vez que o domínio das variáveis de primeira ordem são estabelecidos, o significado dos quantificadores remanescentes são fixados. São estas semânticas que dão a lógica de segunda ordem seu poder de expressão, e elas serão presumidas para o restante deste artigo.

Nas semânticas de Henkin, cada classe de variáveis de segunda ordem tem um domínio particular da sua próprio domínio, que pode ser um subconjunto próprio de todos os grupos ou funções da classe. Leon Henkin (1950) definiu essas semânticas e provou que o teorema incompleto de Gödel e o teorema menos compacto, que sustentam a lógica de primeira ordem, estendem para a lógica de segunda ordem com a semântica de Henkin. Isto é devido as semânticas de Henkin serem quase idênticas para várias semânticas classificadas de primeira ordem, onde classes adicionais de variáveis são adicionadas para simular as novas variáveis da lógica de segunda ordem. A lógica de segunda ordem com semânticas de Henkin não são mais expressivas do que a lógica de primeira ordem. Semânticas de Henkin são comumente usadas no estudo da aritmética de segunda ordem.

[editar] Sistemas Dedutivos

Um sistema dedutivo para a lógica é um conjunto de regras de inferência e axiomas lógicos que determinam que sequência de fórmulas constituem provas válidas. Muitos sistemas dedutivos podem ser usados para a lógica de segunda ordem, contudo nenhum pode ser completo para as semânticas padrão (veja abaixo). Cada um desses sistemas são teoremas, o que significa que nenhuma sentença pode ser usada para provar está logicamente válida na semântica apropriada.

O sistema dedutivo mais fraco que pode ser usado consiste do sistema dedutivo padrão para a lógica de primeira ordem (tais como dedução natural) ampliado com a regra de substituição para termos de segunda ordem.Este sistema dedutivo é comumente usado em estudos de aritmética de segunda ordem.

O sistema dedutivo considerado por Shapiro (1991) and Henkin (1950) soma ao esquema dedutivo de primeira ordem os axiomas de compreensão e axiomas de escolha. Esses axiomas são sólidos para as semânticas padrão de segunda ordem. Eles são teoremas para as semânticas de Henkin apenas se os modelos de Henkin que satisfaçam os axiomas de compreensão e escolha forem considerados.]

[editar] Por que a lógica de segunda ordem não é redutível para a lógica de primeira ordem

Um otimista pode tentar reduzir a teoria de segunda ordem aplicada aos números reais, com semântica de segunda ordem completa, para a teoria de primeira ordem do seguinte modo. Primeiro expandindo o domínio de um conjunto de todos os números reais em domínios classificados em duas classes, tendo a segunda todos os conjuntos de números reais. Somando um novo predicado binário para a linguagem: a relação de associação. Assim sentenças que estão em segunda ordem tornam-se de primeira ordem, com o segunda classe equivalendo ao quantificador de segunda ordem. Esta redução pode ser tentada em uma teoria de classe única pela adição de predicados unários que dizem quando um elemento é um número ou um conjunto, e pegando o domínio para ser a união de conjuntos de números reais e o conjunto das partes dos números reais.

Mas note que o domínio foi definido para incluir all o conjunto dos números reais. Estes requerimentos não podem ser reduzidos para uma sentença de primeira ordem, como o teorema de Löwenheim-Skolem mostra. Este teorema implica que existe algum subconjunto de número reais infinito contável , cujos membros poderemos chamar “números internos”, e alguma coleção infinita contável de conjuntos de números internos, cujos membros poderemos chamar de “conjuntos internos”, tal que o domínio consistindo de números internos e conjuntos internos satisfaz exatamente a mesma sentença de primeira ordem como o domínio de números-reais-e-conjuntos-de-números-reais. Em particular, isto satisfaz a classe de axioma de limite mínimo superior que diz:

Todo conjunto “interno” não vazio que tem um limite superior “interno” tem um limite mínimo superior “interno”.

O fato de ser contável o conjunto de todos os números internos (em conjunção com o fato de que aqueles formas um conjunto compactamente organizado) implica que aquele conjunto não satisfaz o axioma de limite mínimo superior completo. O fato de ser contável o conjunto de todos os conjuntos “internos” implica que o conjunto de todos os subconjuntos do conjunto de todos os números internos (visto que o teorema de Cantor mostra que o conjunto de todos os subconjuntos de um conjunto infinito contável é um conjunto infinito não contável). Esta construção está intimamente relacionado com o paradoxo de Skolem.

Portanto a teoria de primeira ordem dos números reais e conjuntos de números reais tem vários modelos, alguns dos quais são contáveis. Entretanto a teoria de segunda ordem dos números reais tem apenas um modelo.

Isto segue de um clássico teorema que existe apenas uma sequência ordenada completa de Arquimedes, juntamente com o fato que todos os axiomas de uma sequência ordenado completa de Arquimedes são expressíveis em lógicas de segunda ordem. Isto mostra que a teoria de segunda ordem dos números reais não pode ser reduzida a uma teoria de primeira ordem, no senso que a teoria de segunda ordem dos números reais tem apenas um modelo mas a correspondente teoria de primeira ordem tem vários modelos.

Esses são os exemplos mais extremos que mostram que a lógica de segunda ordem com semânticas padrão é mais expressiva que a lógica de primeira ordem. Esta é uma teoria de segunda ordem finita cujo único modelo são os números reais se a hipótese contínua se mantém a qual não tem nenhum modelo se a hipótese contínua não suporte. Esta teoria consiste de uma teoria finita caracterizando os números reais como uma sequência completa ordenada de Arquimedes mais um axioma dizendo que o domínio é de primeira cardinalidade incontável.

Limitações adicionais da lógica de segunda ordem são descritas na próxima seção.

[editar] Lógica de segunda ordem e resultados metalógicos

Isto é um corolário do Teorema incompleto de Gödel onde não há sistema dedutivo (isto é, sem noção de “probabilidade”) para fórmulas de segunda ordem que simultaneamente satisfaz esses três atributos desejados:

(Sem solidez) Toda provável sentença de segunda ordem é universalmente válida, i.e., verdadeira em todos domínios abaixo das semânticas padrão.

(Incompleto) Toda fórmula de segunda ordem universalmente válida, baixo das semânticas padrão, são prováveis.

(Decibilidade) Existe um algoritmo que checa uma prova e pode corretamente decidir se uma dada sequência de símbolos é a prova válida ou não.

Este corolário é algumas vezes expresso por dizer que a lógica de segunda ordem não admite uma teoria de prova completa. Neste respeito a lógica de segunda ordem com semânticas padrão difere da lógica de primeira ordem, e esta é no mínimo uma das razões lógicas tem amparo fora do seu uso. (Quine ocasionalmente apontou para isto como uma razão para pensar na lógica de segunda ordem como não “lógica”, apropriadamente falando.

Como mencionado acima, Henkin provou que o sistema dedutivo padrão para o lógica de primeira ordem é sólido, completo, e efetivo para a lógica de segunda ordem com semânticas Henkin, e o sistema dedutivo com princípios de compreensão e escolha são sólidos, completos e efetivos para as semânticas de Henkin usando apenas modelos que satisfaçam esses princípios.

[editar] A história e o valor disputado da lógica de segunda ordem

A lógica de predicado foi primariamente introduzida para a comunidade matemática por C. S. Peirce, que cunhou o termo “Lógica de segunda ordem”, e cuja notação é mais parecida com a forma moderna. Contudo, hoje muitos estudantes de lógica estão mais familiarizados com os trabalhos de Frege, que atualmente publicou seus trabalho em vários anos antes para Peirce mas cujos trabalhos permaneceram na obscuridade até Russell e Whitehead tornarem-no famoso. Frege usou variáveis diferentes para distinguir quantificação sobre objetos da quantificação sobre propriedades e conjuntos; mas ele não viu ele mesmo como fazer dois tipos diferentes de lógica. Após a descoberta do Paradoxo de Russel foi percebido que alguma coisa estava errada em seu sistema. Eventualmente lógicos encontravam que restringindo a lógica de Frege de vários modos – o que é agora chamado lógica de primeira ordem – eliminou este problema: conjuntos e propriedades não podem ser quantificados sobre a lógica de primeira ordem .

A nova hieraquia padrão de lógica data deste tempo.

Foi encontrado que a teoria dos conjuntos pode ser formulada como um sistema axiomatizado dentro do aparato da lógica de primeira ordem (ao custo de vários tipos de incompletudes, mas nenhuma tão ruim quanto o paradoxo de Russell), e isto foi feito (ver teoria dos conjuntos de Zermelo-Fraenkel), como conjuntos são vitais para matemática, Aritmética, e uma variedade de outras poderosas teorias lógicas podem ser formuladas axiomaticamente sem apelar para mais nenhum aparato lógico do que quantificação de primeira ordem, e isto, em frente com a adesão de Gödel and Skolem para a lógica de primeira ordem, leva a um declínio geral no trabalho em lógica de segunda ordem (ou alguma mais alta) .

Esta rejeição avançou ativamente para alguns lógicos, mais notavelmente W. V. Quine. Quine avançou a visão de que em sentenças de linguagem de predicado como Fx o "x" é para ser pensado com uma variável ou nome denotando um objeto e daí pode ser quantificado, como em “Para todas as coisas,isto é um caso que ...” mas o “F” é para ser pensado como uma abreviação para sentença incompleta, não o nome de um objeto (não até mesmo de um objeto abstrato como uma propriedade). Por exemplo, isto pode significar “ ...é um cachorro”. But isto não faz sentido para pensar que queremos sobre quantificas alguma coisa como isto. (Como uma posição é um tanto consistente com os próprios argumentos de Frege na distinção do objeto-conceito). Assim para usar um predicado como uma variável é para te-lo ocupando o lugar do nome que apenas variáveis individuais devem ocupar. Este raciocínio foi rejeitado por Boolos.

Recentemente a lógica de segunda ordem tem feito alguma coisa para uma recuperação levada a tona pela interpretação de George Boolos da quantificação de segunda ordem como uma quantificação plural sobre o mesmo domínio de objetos como quantificação de primeira ordem. Boolos aponta além do mais para a nonfirstorderizability (não passáveis para a primeira ordem) de sentenças como “Alguns críticos admiram apenas cada outro” e “alguns homens de Fianchetto ganharam dentro do armazém desacompanhado por ninguém mais” que pode apenas ser expressado pela força completa da quantificação de segunda ordem. (Este é um fato falso como quantificação generalizada e parcialmente-organizada, ou ramificando, quantificação suficiente para expressar uma certa classe de sentenças nonfirstorderizable tão bem e ela não recorre a quantificação de segunda ordem.

[editar] Aplicações para a complexidade

A força expressiva de várias formas de lógica de segunda ordem nas estruturas finitas estão intimamente vinculado a teoria de complexidade computacional. O campo de complexidade descritiva estuda como as classes de complexidade computacionais podem ser caracterizadas pela força de lógica necessária para expressar linguagens nela. Em particular:

NP é o conjunto de linguagens expressíveis pela lógica de segunda ordem existencial.

co-NP é o conjunto de linguagens expressíveis pela lógica de segunda ordem universal.

PH é o conjunto de linguagens expressíveis pela lógica de segunda ordem.

PSPACE é o conjunto de linguagens expressíveis pela lógica de segunda ordem com a adição de operador proximidade transitivo.

EXPTIME é o conjunto de linguagens expressíveis pela lógica de segunda ordem com a adição de um operador de ponto mínimo fixado.

Relacionamentos entre essas classes impacta diretamente a falta de expressividade relativa da lógica; por exemplo, se PH=PSPACE, então somando um operador de proximidade transitiva para o lógica de segunda ordem não faz nada mais expressivo.

[editar] Força do fragmento existencial

O fragmento existencial (EMSO) da lógica de segunda ordem monádica (MSO) é lógica de segunda ordem sem os quantificadores de segunda ordem universais, e sem ocorrências negativas de quantificadores de segunda ordem. Sobre palavra 'w ∈ Σ^*, cada fórmula MSO pode ser convertida em uma máquina de estado finita determinística. Esta novamente pode ser convertida em uma formula EMSO. Portanto EMSO e MSO são equivalentes em outras palavras. Para árvores como entrada, este resultado é mantido também.

Contudo, acima da grade finita Σ⁺⁺, esta propriedade não é mais mantida, visto que as linguagens reconhecidas por sistemas tiling não são fechadas para o complemento inferior. Assim um quantificador universal é equivalente a negação do quantificador existencial, que não pode ser expresso, alternativas dos quantificadores universal e existencial geram classe maiores e maiores de linguagem acima Σ⁺⁺.