Une classe de systèmes logiques qui étend la quantification aux prédicats, fonctions et entités de type supérieur (fonctions de fonctions, prédicats de prédicats, etc.), permettant de raisonner sur des objets de type supérieur et de formaliser directement des concepts mathématiques et sémantiques difficilement exprimables en logiques d'ordre inférieur.

Principe

La logique d'ordre supérieur organise les objets dans une hiérarchie typée et permet la quantification à des types arbitrairement élevés ; la sémantique peut être donnée sur des domaines de types supérieurs pleins ou via une sémantique générale de type Henkin, et ce choix détermine les propriétés proof-théoriques et modèle-théoriques.

Démonstration

Dans un cadre d'ordre supérieur on peut quantifier sur des ensembles d'ensembles ou sur des fonctionnelles : par exemple, formaliser la sémantique d'un langage typé de programmation requiert souvent de quantifier sur des prédicats sur des fonctions, ce que la logique d'ordre supérieur exprime directement et proprement dans la discipline des types.

Mauvaise application

Supposer la complétude, la décidabilité ou l'axiomatisabilité effective pour la logique d'ordre supérieur pleine comme si elle était du premier ordre est incorrect ; des axiomes de compréhension non restreints mènent à l'incohérence à moins d'être soigneusement limités ou formulés dans un cadre théorique des types cohérent.

Conséquence

Les cadres d'ordre supérieur offrent une grande commodité d'expression, permettant la formalisation directe des mathématiques, de la sémantique des langages et des constructions catégoriques ou en théorie des ensembles, mais ils sacrifient en général les garanties méta-logiques souhaitables et augmentent la complexité d'interprétation sémantique.

Inversion

Restreindre la logique d'ordre supérieur à des fragments, à un niveau fini de types, ou à la sémantique de Henkin récupère de nombreux avantages proof-théoriques de la logique du premier ordre ; inversement, insister sur une sémantique pleine de types supérieurs maximise l'expressivité au prix d'une fragilité méta-logique.

Limite

La logique d'ordre supérieur présuppose une discipline de types et peut exclure des constructions non typées ou impredicatives sauf autorisation explicite ; ses propriétés méta et les axiomes admissibles dépendent de l'utilisation de la sémantique pleine, de la sémantique de Henkin ou d'une fondation constructive/théorique des types.

Tension sémantique

Il existe une tension entre le désir d'un langage riche qui internalise la pratique mathématique (favorisant une sémantique pleine et expressive d'ordre supérieur) et la demande de contrôle syntaxique et de résultats méta-théoriques (favorisant des fragments restreints ou une approche de type Henkin).

Synthèse

La Logique D'Ordre Supérieur est une extension typée de la syntaxe logique qui porte la quantification et le raisonnement aux prédicats et aux entités de type supérieur, offrant des moyens puissants pour exprimer mathématiques et sémantiques tout en imposant des choix explicites sur les types et la sémantique qui déterminent si l'on privilégie l'expressivité ou le comportement méta-théorique souhaitable.