Lógica de ordem superior - Higher-order logic

Em matemática e lógica , uma lógica de ordem superior é uma forma de lógica de predicado que se distingue da lógica de primeira ordem por quantificadores adicionais e, às vezes, semântica mais forte . Lógicas de ordem superior com sua semântica padrão são mais expressivas, mas suas propriedades teóricas do modelo são menos bem-comportadas do que as da lógica de primeira ordem.

O termo "lógica de ordem superior", abreviado como HOL , é comumente usado para significar lógica de predicado simples de ordem superior . Aqui "simples" indica que a subjacente teoria dos tipos é a teoria dos tipos simples , também chamado de teoria simples de tipos (ver teoria Tipo ). Leon Chwistek e Frank P. Ramsey propuseram isso como uma simplificação da complicada e desajeitada teoria ramificada dos tipos especificada no Principia Mathematica de Alfred North Whitehead e Bertrand Russell . Os tipos simples hoje em dia às vezes também excluem os tipos polimórficos e dependentes .

Escopo de quantificação

A lógica de primeira ordem quantifica apenas variáveis ​​que abrangem indivíduos; a lógica de segunda ordem , além disso, também quantifica sobre conjuntos; a lógica de terceira ordem também quantifica sobre conjuntos de conjuntos e assim por diante.

Lógica de ordem superior é a união de primeira, segunda, terceira, ..., n º de ordem lógica; ou seja, a lógica de ordem superior admite a quantificação sobre conjuntos que são aninhados de forma arbitrária profundamente.

Semântica

Existem duas semânticas possíveis para lógica de ordem superior.

Na semântica padrão ou completa , os quantificadores sobre objetos de tipo superior abrangem todos os objetos possíveis desse tipo. Por exemplo, um quantificador sobre conjuntos de indivíduos abrange todo o conjunto de poderes do conjunto de indivíduos. Assim, na semântica padrão, uma vez especificado o conjunto de indivíduos, isso é suficiente para especificar todos os quantificadores. O HOL com semântica padrão é mais expressivo do que a lógica de primeira ordem. Por exemplo, o HOL admite axiomatizações categóricas dos números naturais e dos números reais , que são impossíveis com a lógica de primeira ordem. No entanto, por um resultado de Kurt Gödel , HOL com semântica padrão não admite um cálculo de prova eficaz , sólido e completo . As propriedades teóricas do modelo de HOL com semântica padrão também são mais complexas do que as da 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. O número de Löwenheim da lógica de primeira ordem, em contraste, é 0 , o menor cardinal infinito.

Na semântica de Henkin , um domínio separado é incluído em cada interpretação para cada tipo de ordem superior. Assim, por exemplo, quantificadores sobre conjuntos de indivíduos podem variar em apenas um subconjunto do conjunto de poderes do conjunto de indivíduos. O HOL com essa semântica é equivalente à lógica de primeira ordem de classificação múltipla , em vez de ser mais forte do que a lógica de primeira ordem. Em particular, HOL com semântica de Henkin tem todas as propriedades teóricas do modelo da lógica de primeira ordem e tem um sistema de prova completo, sólido e eficaz herdado da lógica de primeira ordem.

Exemplos e propriedades

Mais elevados lógicas de ordem incluem as ramificações da Igreja 's simples teoria dos tipos e as várias formas de teoria dos tipos intuitionistic . Gérard Huet mostrou que a unifiabilidade é indecidível em um tipo de teoria de tipo da lógica de terceira ordem, ou seja, não pode haver algoritmo para decidir se uma equação arbitrária entre termos de terceira ordem (muito menos termos arbitrários de ordem superior) tem uma solução .

Até uma certa noção de isomorfismo, a operação do conjunto de potência é definível na lógica de segunda ordem. Usando essa observação, Jaakko Hintikka estabeleceu em 1955 que a lógica de segunda ordem pode simular lógicas de ordem superior no sentido de que para cada fórmula de uma lógica de ordem superior, pode-se encontrar uma fórmula equisatisfatória para ela na lógica de segunda ordem.

O termo "lógica de ordem superior" é assumido em algum contexto para se referir à lógica de ordem superior clássica . No entanto, a lógica modal de ordem superior também foi estudada. De acordo com vários lógicos, a prova ontológica de Gödel é melhor estudada (de uma perspectiva técnica) em tal contexto.

Veja também

Notas

Referências

links externos