Lógica de ordem superior
Este artigo não cita fontes confiáveis. (Junho de 2017) |
Na matemática e na lógica, uma lógica de ordem superior é uma forma de lógica de predicados que se distingue da lógica de primeira ordem por permitir a presença de quantificadores sobre predicados, e por possuir uma semântica mais forte. Lógicas desse tipo, com sua semântica padrão, são mais expressivas, mas suas propriedades na teoria dos modelos são "menos bem-comportadas" do que as da lógica de primeira ordem em relação a certas aplicações.
Um predicado de ordem superior seria um predicado que tem um ou mais predicados como argumentos. Em geral, um predicado de ordem superior de ordem n toma um ou mais predicados de ordem (n − 1) como argumentos, onde n > 1.
Ordem superior simples da lógica de predicados
editarO termo "lógica de ordem superior" (do inglês "higher-order logic", comumente abreviado como HOL) geralmente é utilizado para significar ordem superior simples da lógica de predicados. Onde o "simples" indica que a teoria dos tipos subjacentes é simples, não-polimórfica ou dependente.
Atualmente há duas semânticas possíveis para HOL. Na semântica padrão ou completa, quantificados e objetos do tipo superior variam sobre todos os objetos possíveis tipo. Por exemplo, um quantificador sobre um conjunto de indivíduos varia ao longo de todo o conjunto das partes do conjunto de indivíduos. Assim, na semântica padrão, uma vez que o conjunto de indivíduos é especificado, temos o suficiente para indicar todos os quantificadores.
HOL com semântica padrão é mais expressiva do que a lógica de primeira ordem por, exemplo, admitir axiomatizações categóricas dos números naturais e dos números reais, que são possíveis com a lógica de primeira ordem. No entanto, sabemos através dos resultados de Gödel, que HOL com semântica padrão não admite um efetivo e completo cálculo como prova eficaz.
As propriedades da teoria dos modelos de HOL com semântica padrão também são mais complexas do que as de lógica de primeira ordem. Por exemplo, o número de Löwenheim da lógica de segunda ordem já é maior do que o primeiro cardinal mensurável, se tal cardinal existir. Por sua vez, o número de Löwenheim da lógica de primeira ordem é o ℵ0, o menor cardinal infinito.
Na semântica de Henkin, um domínio separado está incluído em cada interpretação para cada tipo de ordem superior. Assim, por exemplo, usando o mesmo exemplo dado anteriormente, os quantificadores sobre conjuntos de indivíduos podem variar ao longo de apenas um subconjunto do conjunto das partes do conjunto de indivíduos. HOL com essa semântica é equivalente a lógica de primeira ordem tipada (do inglês "many-sorted first-order logic, que permite que as variáveis e termos tenham vários tipos, ou sortes), ao invés de ser mais forte do que a lógica de primeira ordem. Em particular, HOL com semântica de Henkin tem todas as propriedades da teoria dos modelos, é completo, e tem um eficaz sistema de provas herdado da lógica de primeira ordem.
Exemplos
editarComo exemplos da utilização da ordem de lógica superior temos os cálculos de Thierry Coquand e o cálculo lambda simplesmente tipado de Alonzo Church, que suporta ambos os tipos: dependentes e polimórficos.
Críticas
editarQuine classificou a lógica de ordem superior (com semântica padrão) como "teoria dos conjuntos em pele de cordeiro". Esse crítica incide sobre a falta de uma prova eficaz e completa da teoria. Ele argumenta que isso não faz da HOL uma "lógica". Por sua vez, Saphiro respondeu essa crítica argumentando que a expressividade semântica adicional pode compensar a falta de uma prova teórica, e complementou dizendo que a "lógica" só necessita de um sistema dedutivo ou um sistema semântico, mas que, talvez, não possa ter ambos.
