Lógica de ordem superior
Origem: Wikipédia, a enciclopédia livre.
Na matemática, a lógica de ordem superior se distigue da lógica de primeira ordem em vários aspectos. 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 sistemas nos quais isto é permitido.
Uma outra diferença da lógica de ordem superior com relação a lógica de primeira ordem está nas construções permitidas pela teoria dos tipos subjacente. Um predicado de ordem superior é 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.
A lógica de ordem superior é mais expressiva, mas suas propriedades, em particular, no que diz respeito à teoria dos modelos, a tornam menos bem comportada para muitas aplicações. Tendo em vista um resultado de Gödel, sabemos que a lógica de ordem superior não admite uma axiomatização recursiva correta e completa sobre modelos padrão. Existe contudo uma tal axiomatização correta e completa sobre modelos de Henkin.
