Propriété d'une logique ou d'une théorie formelle qui affirme que toute formule ou phrase satisfiable (ayant un modèle) admet un modèle fini.

Principe

Limiter la réalisabilité aux structures finies : si une formule peut être réalisée, elle peut l'être dans une structure finie ; cela permet souvent de relier la sémantique à des procédures effectives par exploration de domaines finis.

Démonstration

Beaucoup de logiques modales disposent de cette propriété parce que la filtration construit, pour toute formule satisfiable, un modèle de Kripke fini ; concrètement, une formule modale satisfiable admet un cadre fini qui la valide.

Mauvaise application

Supposer que la propriété du modèle fini entraîne systématiquement la complétude ou la décidabilité pour toute théorie : la FMP facilite la décidabilité dans de nombreux cas mais n'en garantit pas l'existence sans énumérabilité effective des axiomes.

Conséquence

En présence de la FMP et d'un langage/axiomatique énumérable, on obtient généralement la décidabilité en recherchant des modèles finis ; la FMP contraint aussi les contre-modèles possibles à un espace de recherche fini.

Inversion

La situation opposée est la propriété du modèle infini : il existe des formules satisfiables qui n'ont que des modèles infinis, si bien qu'aucune structure finie ne les réalise.

Limite

S'applique aux logiques ou théories et à leurs phrases satisfiables ; dépend de la signature et du type de modèles autorisés (par exemple signatures relationnelles vs fonctionnelles) et n'est pas une assertion sur des structures finies particulières ou le comptage de modèles de taille bornée.

Tension sémantique

La tension est entre satisfiabilité finie (existence de modèles finis) et satisfiabilité générale (existence de modèles arbitraires) ; une logique peut être satisfiable sans avoir la FMP si la réalisation requiert des constructions infinies.

Synthèse

La propriété du modèle fini précise que toute satisfiabilité peut être témoinée par des structures finies ; elle organise les procédures de recherche sémantique et se situe entre la satisfiabilité abstraite et la décidabilité effective en restreignant les contre-modèles au domaine fini.