Propriété algébrique ou logique d'une classe de structures (finies) affirmant que toute sous-structure partielle finie (ou algèbre partielle finie satisfaisant localement le diagramme définitoire de la classe) peut être plongée dans une structure pleine finie de la classe ; en termes informels, des morceaux locaux finis et cohérents s'étendent à des membres globaux finis de la classe.

Principe

L'idée organisatrice est une extension locale-vers-globale finie : la cohérence partielle finie (absence de contradiction locale parmi un nombre fini d'éléments et de relations) doit être réalisable à l'intérieur d'un modèle fini de la classe entière, de sorte que les contraintes locales n'obligent pas à une complétion infinie.

Démonstration

Exemple : certaines variétés d'algèbres finies et quelques classes de structures relationnelles possèdent la propriété de plongement fini : étant donné une table de multiplication partielle finie compatible avec les lois d'une algèbre de Boole, on peut plonger cette table partielle dans une algèbre de Boole finie, montrant que la structure partielle s'étend à une structure pleine finie de la classe.

Mauvaise application

En déduire à tort de la propriété de plongement fini que la classe entière est finiment axiomatisable, décidable ou fermée sous des constructions arbitraires ; la propriété ne concerne que l'immersibilité des structures partielles finies et n'impose pas automatiquement des propriétés algébriques ou algorithmiques globales.

Conséquence

Quand une classe possède FEP, on peut souvent réduire la vérification de la satisfiabilité finie ou des contraintes locales à une recherche de modèles finis, en déduire des propriétés de modèle fini pour des théories universelles et obtenir des résultats de transfert utiles en décidabilité et en complétude pour les modèles finis.

Inversion

L'échec de la propriété de plongement fini signifie qu'il existe des structures partielles finies compatibles avec les relations définitoires qui ne peuvent être plongées dans aucune structure pleine finie de la classe ; la cohérence locale finie ne garantit donc pas une complétion finie et le raisonnement sur modèles finis est entravé.

Limite

S'applique aux sous-structures partielles finies par rapport à une signature et une classe spécifiées ; elle exclut les affirmations concernant des structures partielles infinies, des plongements dans des modèles infinis et la dérivabilité syntaxique hors du cadre algébrique ou relationnel spécifié.

Tension sémantique

Il existe une tension entre FEP et des propriétés de compacité ou de fermeture : FEP est un principe d'extension finitaire qui peut être en conflit avec des constructions infinitaires, et il échange la fermeture modèle-théorique générale contre un contrôle renforcé des modèles finis.

Synthèse

FEP formalise l'idée que des morceaux locaux finis et cohérents d'une structure peuvent être réalisés à l'intérieur de modèles globaux finis de la classe : c'est un pont pragmatique entre spécifications locales finies et réalisations finies, crucial en théorie algébrique des modèles et pour la décidabilité en modèle fini.