Lógica de segunda ordem
# Lógica de segunda ordem

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 ideia de universo de 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\land \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 da bivalência). A versão mais geral da lógica de segunda ordem inclui ainda formas de quantificar sobre funções e outros tipos de variáveis como explanado na seção Sintaxe, abaixo.

## 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 expressar na lógica de primeira ordem a existência de um inverso aditivo de cada número real escrevendo $\forall x\in \mathbb {R} (\exists y\in \mathbb {R} :x+y=0)$ mas é necessária a lógica de segunda ordem para expressar a propriedade do menor limite superior para o conjunto dos números reais, onde para cada conjunto não-vazio de números reais limitado superiormente tem um 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 menor limite 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 que "o domínio é finito" ou que "o domínio tem de cardinalidade enumerável" Para dizer que o domínio é finito, use a sentença que diz que toda função injetora do domínio nele mesmo é sobrejetora. Para dizer que o domínio tem cardinalidade enumerável, use a sentença que diz que existe uma bijeção entre quaisquer dois subconjuntos infinitos do domínio. Não é possível caracterizar a finitude ou a enumerabilidade na lógica de primeira ordem.

## Sintaxe

A sintaxe da lógica de segunda ordem diz quais expressões são fórmulas bem formadas. Em adição à sintaxe da lógica de primeira ordem, a lógica de segunda ordem inclui vários novos tipos (ou sortes) de variáveis. São eles:
* O tipo das variáveis que tratam de grupos de indivíduos. Se $S$ é uma variável deste tipo e $x$ é um termo de primeira ordem então a expressão $x\in S$ (também escrita $S(x)$ ou $Sx$) é uma fórmula atômica. Conjuntos de indivíduos podem também ser vistos como relações unárias sobre o domínio.
* Para cada número natural $k$ existe um tipo de variável que trata das relações $n$-árias sobre esses elementos. Se $R$ é uma tal relação n-á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 tipo de variáveis que trata de funções que tomam $k$ elementos do domínio e retornam um único elemento deste domínio. Se $f$ é um tal símbolo de função $n$-ária e $x_{1},\ldots ,x_{k}$ são termos de primeira ordem então a expressão $f(x_{1},\ldots ,x_{k})$ é um termo de primeira ordem.
Para cada um dos tipos de variável definidos acima, pode-se construir fórmulas pelo uso dos quantificadores existenciais e/ou universais. Existem assim os tipos de quantificadores, dois para cada tipo de variável.
Uma sentença na lógica de segunda ordem, assim como na lógica de primeira ordem, é uma fórmula bem formada sem variáveis livres (de nenhum tipo).
Na lógica de segunda ordem monádica, apenas as variáveis para subconjuntos são adicionadas. A lógica de segunda ordem com todos os tipos de variáveis descritas acima é algumas vezes chamada de lógica de segunda ordem full para distingui-la da versão monádica.
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 de segunda ordem particular. Sobre tais símbolos vale, contudo, a seguinte restrição: todos os termos que eles formam devam ser ou termos de primeira ordem (que podem ser substituídos no lugar de uma variável de primeira ordem) ou termos de segunda ordem (que podem ser substituídos no lugar de uma variável de um tipo apropriado).

## Semântica

A semântica da lógica de segunda ordem estabelece o significado de cada sentença. Diferentemente da lógica de primeira ordem, que tem apenas uma semântica, existem duas semânticas diferentes que são comumente usadas para a lógica de segunda ordem: padrão e semântica de Henkin. Em cada uma dessas semânticas, as interpretações dos quantificadores de primeira ordem e dos conectivos lógicos são exatamente como na lógica de primeira ordem. Apenas os novos quantificadores sobre variáveis de segunda ordem precisam ter sua semântica definida.
Nas semânticas padrão, os quantificadores tratam de todos os grupos ou funções do tipo apropriado. Portanto, uma vez que o domínio das variáveis de primeira ordem sejam estabelecidos, o significado dos quantificadores remanescentes são fixados. São estas semânticas que dão à lógica de segunda ordem seu poder de expressão, e elas assumidas conhecidas no restante deste artigo.
Na semântica de Henkin, cada tipo de variável de segunda ordem tem seu próprio domínio de discurso, que pode ser um subconjunto próprio de todos os grupos ou funções daquele tipo. Leon Henkin (1950) definiu essa semântica e demonstrou que o teorema da completude e o teorema da compacidade, que valem na lógica de primeira ordem, podem ser estendidos para a lógica de segunda ordem com a semântica de Henkin. Isto é devido ao fato de a semântica de Henkin ser quase idêntica à semântica de primeira ordem polissortida, na qual tipos adicionais de variáveis são adicionados para simular as novas variáveis da lógica de segunda ordem. A lógica de segunda ordem com semântica de Henkin não é mais expressiva do que a lógica de primeira ordem. A semântica de Henkin é normalmente usada no estudo da aritmética de segunda ordem.

## Sistemas Dedutivos

Um sistema dedutivo para uma lógica é um conjunto de regras de inferência e axiomas lógicos que determinam que sequências de fórmulas constituem demonstrações válidas. Muitos sistemas dedutivos podem ser usados para a lógica de segunda ordem, contudo nenhum pode ser completo para a semântica padrão (veja abaixo). Cada um desses sistemas é correto, o que significa que toda sentença demonstrada por eles é logicamente válida na semântica apropriada.
O sistema dedutivo mais fraco que pode ser usado consiste de um sistema dedutivo padrão para a lógica de primeira ordem (tal como dedução natural) ampliado com regras de substituição para termos de segunda ordem. Tais sistemas dedutivos são comumente usados no estudo da aritmética de segunda ordem.
O sistema dedutivo considerado por Shapiro (1991) and Henkin (1950) soma ao esquema dedutivo aumentado da lógica de primeira ordem os axiomas de compreensão e da escolha. Estes axiomas são corretos para a semântica padrão de segunda ordem. Eles são corretos para a semânticas de Henkin se consideram apenas modelos de Henkin que satisfazem os axiomas de compreensão e da escolha.

## Por que a lógica de segunda ordem não é redutível à lógica de primeira ordem

Um otimista pode tentar reduzir da seguinte forma a teoria de segunda ordem dos números reais, com semântica de segunda ordem full, para à teoria de primeira ordem. Primeiro expanda o domínio do conjunto de todos os números reais para um domínio bissortido ( isto é, como dois tipos de indivíduos), tal que o segundo tipo contenha todos os conjuntos de números reais. Adicione um novo predicado binário à linguagem: a relação de pertinência. Assim sentenças que estavam em segunda ordem tornam-se de primeira ordem, só que agora os quantificadores que eram de segunda ordem tratam ao invés do segundo tipo de variáveis. Esta redução pode ser tentada em uma teoria com um único tipo pela adição de predicados unários que dizem quando um elemento é um número ou um conjunto, e tomando o domínio como 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 todos os conjuntos de números reais. Esta exigência pode ser reduzido a uma sentença de primeira ordem, como mostra o teorema de Löwenheim-Skolem. Segundo este teorema, deve existir algum subconjunto infinito enumerável dos número reais, cujos membros chamaremos números internos, e alguma coleção infinita enumerável de conjuntos de números internos, cujos membros poderemos chamar de conjuntos internos, tais que o domínio que consiste de números internos e conjuntos internos satisfaz exatamente as mesmas sentenças de primeira ordem satisfeitas pelo domínio de números-reais-e-conjuntos-de-números-reais. Em particular, ele satisfaz um tipo de axioma de menor limite superior que diz, de fato, que:
    Todo conjunto interno não vazio que tem um limite superior interno tem um limite mínimo superior interno.
O fato de o conjunto de todos os números internos ser enumerável (em conjunção com o fato de que aqueles formam um conjunto ordenado denso) faz com que aquele conjunto não satisfaça inteiramente o axioma de menor limite superior. O fato de o conjunto de todos os conjuntos internos ser enumerável faz com que este conjunto seja 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 enumerável é um conjunto infinito não enumerável). Esta construção está intimamente relacionada ao 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 enumeráveis. Entretanto a teoria de segunda ordem dos números reais tem apenas um modelo. Isto segue de um teorema clássico segundo o qual existe apenas um corpo ordenado completo de Arquimediano, juntamente com o fato de que todos os axiomas de um corpo ordenado completo de Arquimediano são expressáveis na lógica 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 teoria de primeira ordem correspondente tem vários modelos.
Há exemplos mais extremos que mostram que a lógica de segunda ordem com semântica padrão é mais expressiva que a lógica de primeira ordem. Há uma teoria de segunda ordem finita cujo único modelo é o conjunto dos números reais se a hipótese do contínuo vale e que não tem nenhum modelo se a hipótese do contínuo não vale. Esta teoria consiste de uma teoria finita caracterizando os números reais como um corpo ordenado completo de Arquimediano mais um axioma dizendo que o domínio é da primeira cardinalidade não enumerável.
Limitações adicionais da lógica de segunda ordem são descritas na próxima seção.

## Lógica de segunda ordem e resultados metalógicos

Segue como corolário do Teorema da incompletude Gödel que não há sistema dedutivo (isto é, não há uma "demonstrabilidade") para fórmulas de segunda ordem que satisfaça simultaneamente esses três atributos desejados:
* (Correção) Toda sentença demonstrável de segunda ordem é universalmente válida, isto é, verdadeira em todos domínios sob a semântica padrão.
* (Completude) Toda fórmula de segunda ordem universalmente válida, sob a semântica padrão, é demonstrável.
* (Efetividade) Existe um algoritmo que possa verificar e decidir corretamente se uma dada sequência de símbolos é uma demonstração válida ou não.
Este corolário é expresso dizendo-se que a lógica de segunda ordem não admite uma teoria de demonstração completa. Neste aspecto a lógica de segunda ordem com semânticas padrão difere da lógica de primeira ordem, e esta é uma das razões pelas quais os lógicos muitas vezes evitam usar lógica de segunda ordem. (Quine ocasionalmente apontou isto como uma razão para pensar na lógica de segunda ordem como não sendo uma lógica, propriamente dita. )
Como foi mencionado acima, Henkin demonstrou que o sistema dedutivo padrão para o lógica de primeira ordem é correto, completo, e efetivo para a lógica de segunda ordem com semântica de Henkin, e o sistema dedutivo com princípios de compreensão e de escolha são corretos, completos e efetivos para as semânticas de Henkin que usa apenas modelos que satisfazem esses princípios.