Lógica de ordem superior
Origem: Wikipédia, a enciclopédia livre.
Na matemática, a lógica de ordem superior é distinta da lógica de primeira ordem em várias maneiras. Uma dessas diferenças diz respeito ao tipo de variáveis que aparecem nos quantificadores. Na lógica de primeira ordem não é permitido quantificar sobre predicados. Veja a lógica de segunda ordem para saber quando isto é permitido.
Uma outra diferença da lógica de ordem superior para a lógica de primeira ordem está nas construções permitidas no tipo subjacente da teoria. Um predicado de ordem superior é um predicado que faz um ou outros predicados como argumentos. No general, um predicado de ordem superior da ordem n faz um ou mais (n − 1) predicados como argumentos, onde n > 1.
A lógica de ordem superior é mais expressiva, mas suas propriedades, em particular, no que diz respeito à teoria dos modelos, fazem-na menos bem-formadas para muitas aplicações. Pelo resultado de Gödel, a lógica de ordem superior clássica não admite o estilo de (recursividade axiomática) e não completa o cálculo da prova; entretanto, tal cálculo da prova existe, é aceita e completa com respeito aos modelos de Henkin.