Utilisateur:Fabian Pijcke/Théorie des modèles finis

La Théorie des Modèles Finis (FMT, de l'angle Finite Model Theory) est un sous-domaine de la théorie des modèles (MT). La théorie des modèles est la branche de la Logique mathématique qui traite de la relation entre un langage formel (la syntaxe) et ses interprétations (la ou les sémantique). FMT est une restriction de MT aux interprétations utilisant des structures finies, i.e. des structures sur un univers fini.

Preuve: Parce que beaucoup de théorèmes centraux de la théorie des modèles ne s'appliquent pas aux structures finies, FMT est assez différent de MT au niveau des méthodes de preuves. Les résultats centraux qui ne fonctionnent pas incluent le Théorème de compacité, le Théorème de complétude de Gödel, et la méthode des ultraproduits pour la logique du premier ordre (FO). Certains concepts perdent leur sens tels que celui de type (et nécessitent donc d'être redéfinis avec FMT). D'autres méthodes telles que les jeux de Ehrenfeucht-Fraïssé deviennent plus centraux avec FMT.

Finitude: Comme MT est étroitement lié à l'algèbre mathématique, FMT devient un instrument "exceptionnellement efficace" au niveau des sciences informatiques. L'origine de cela vient peut-être du fait que les formules valides en premier ordre sur toutes les structures finies ne sont pas récursivement énumérables, i.e. d'un point de vue mathématique, elles sont 'seulement' finies mais dans scientifiquement en informatique, elles peuvent être vues comme des objets d'étude relativement complexes. En d'autres mots: "Dans l'histoire de la logique mathématique, l'intérêt a toujours été porté sur les structures infinies ... Malgré cela, les objets que les ordinateurs utilisent et conservent en mémoire sont toujours finis. Pour étudier l'informatique nous avons besoin d'une théorie des structures finies."

Applications: Le domaine de la théorie de la complexité descriptive fait le lien entre les classes de complexité et les structures et formules logiques, pour acquérir de nouvelles connaissances et justifications pour la théorie de la complexité informatique. En Théorie des bases de données les langages de requêtes peuvent être formalisés par des sous-ensembles et des extensions de la logique du premier odre. Dans la théorie des langages formels, la puissance d'expression des langages correspond à certaines logiques sur les structures finies.

Caractérisation: Toute structure finie peut être caractérisée par une formule du premier ordre à isomorphisme près. Cela n'est pas possible pour les classes de structures finies. Des méthodes sont donc requises pour déterminer si une classe de structures peut être caractérisée dans un certain langage. Par exemple, les jeux, la localité, les lois 0-1, ainsi que des extensions de FO peuvent être utilisées pour discriminer ces classes. Les logiques point-fixe ou sous-SO, tout

FMT is mainly about discrimination of structures: Every single finite structure can be characterized in a single FO sentence up to isomorphy. This doesn't hold for classes of finite structures. Thus methods are required to determine if a class of structures can be discriminated in a certain language, e.g. games, locality, 0-1 laws, also extensions of FO can be thought of in order to discriminate these classes, fixed point logics,or sub-SO logics, as well as assumptions can be made on the structure, e.g. that it's ordered or is a string. Finite model theory also studies finite restrictions of logic, such as first-order logic with only a fixed limit of k variables as well as hybrid structures, where nonfinite structures are embedded in finite ones.

Basics

Basically FMT is about the discrimination of structures, i.e. can a set of structures be uniquely described in a certain language. We will see that this can be achieved in FO for a single structures always, for a finite set of structures sometimes and for a set containing infinite structures never.

Single Structure

Single graphs (1) and (1') having common properties.

Problem

Given a structure like (1). This structure can be described by FO sentences like

1. every node has an edge to another node: $\forall _{x}\exists _{y}G(x,y).$
2. no node has an edge to itself: $\forall _{x},y(G(x,y)\Rightarrow x\neq y).$
3. there is at least one node that is connected to all others: $\exists _{x}\forall _{y}(x\neq y\Rightarrow G(x,y)).$

Now do these properties describe the structure uniquely (up to isomorphism)? Obviously not since for structure (1') the above properties hold as well. Simply put, the question is, if one adds enough properties, is it possible that these properties (all together) describe exactly (1) and are valid (all together) for no other structure (up to isomorphy).

Approach

For a single finite structure this is always possible. The principle is quite simple (here for single binary Relations and without constants):

1. say that there are at least n elements: $\varphi _{1}=\bigwedge _{i\neq j}\neg x_{i}=x_{j}$
2. say that there are at most n elements: $\varphi _{2}=\forall _{y}\bigvee _{i}x_{i}=y$
3. state every element of the Relation R: $\varphi _{3}=\bigwedge _{(a_{i},a_{j})\in R}R(x_{i},x_{j})$
4. state every non-element of the Relation R: $\varphi _{4}=\bigwedge _{(a_{i},a_{j})\notin R}\neg R(x_{i},x_{j})$

all for the same tuple $x_{1}..x_{n}$, i.e $\exists _{x_{1}}...\exists _{x_{n}}(\varphi _{1}\land \varphi _{2}\land \varphi _{3}\land \varphi _{4})$.

Moreover

This can easily be extended for any fixed number of structures. For, say 2, structures a unique description can easily be obtained by disjunction of the single descriptions, i.e.

$\exists _{x_{1}}...\exists _{x_{n}}(\varphi _{1}\land \varphi _{2}\land \varphi _{3}\land \varphi _{4})\lor \exists _{x_{1}}...\exists _{x_{n}}(\varrho _{1}\land \varrho _{2}\land \varrho _{3}\land \varrho _{4})$

Writing down a sequence of, say 67, descriptions is easy in theory, but quite impractical. This is a well known problem from programming, where one would use a for loop from 1 to 67 instead. This isn't dealt with in depth here, but mentioned to show that there are more issues to a language than just its expressiveness.

Finite Number of Structures

Set of up to n structures.

Problem

The descriptions so far had in common that they strictly define the number of elements of the universe. Unfortunately most of the interesting sets of structures are not restricted to a certain size, like all graphs that are trees, are connected or are acyclic. Thus to discriminate a finite number of structures is of special importance.

A finite number of structures cannot always be discriminated by an FO sentence. Examples that can be discriminated are structures of even size, ... . The following can be discriminated: ... . We always talk about discrimination up to isomorphy here.

Approach

The next best thing to a general statement, that we cannot make here, is to give a criterion to differentiate between structures that can and cannot be discriminated. This criterion is given by: a class of structures cannot be discriminated in FO iff for every m there are structures A in K and B not in K and A and B satisfy the same FO sentences of quantifier rank* up to m.

${\mathfrak {A}}\in K,{\mathfrak {B}}\notin K,{\mathfrak {A}}\equiv _{m}{\mathfrak {B}}$

for some m and all structures A and B.

Set of infinitely many structures.

Moreover

An infinite number of structures can only be achieved by allowing structures of infinite size. Thus this is, by definition, no issue of FMT, but for the sake of understanding we consider this case here briefly. We had single structures, that can always be discriminated in FO. We had finite numbers of structures, that in some cases can be discriminated in FO in some cases not. Now for infinite structures, we can never discriminate a structure in FO, i.e. for every infinite model a non-isomorphic one can be found, having exactly the same properties in FO.

The most famous example is probably Skolem's theorem: there is a countable non-standard model of arithmetic.

History

1. Trakhtenbrot 1950: failure of completeness theorem in FO,
2. Scholz 1952: characterisation of specra in FO,
3. Fagin 1974: the set of all properties expressible in existential second-order logic is precisely the complexity class NP,
4. Chandra, Harel 1979/ 80: fixed-point FO extension for db query languages capable of expressing transitive closure -> queries as central objects of FMT.
5. Immerman, Vardi 1982: fixed point logic over ordered structures captures PTIME -> descriptive complexity (... Immerman–Szelepcsényi theorem)
6. Ebbinghaus, Flum 1995: First comprehensive book "Finite Model Theory"
7. Abiteboul, Hull, Vianu 1995: Book "Foundations of Databases"
8. Immerman 1999: Book "Descriptive Complexity"
9. Kuper, Libkin, Paredaens 2000: Book "Constraint Databases"
10. Darmstadt 2005/ Aachen2006: first international workshops on "Algorithmic Model Theory"

External links

• R. Fagin. Finite model theory-a personal perspective. Theoretical Computer Science 116, 1993, pp. 3-31.
• Leonid Libkin: The finite model theory toolbox of a database theoretician Also very suitable as general introduction and overview.
• Leonid Libkin: Intro chapter of "Elements of Finite Model Theory". Motivation of 3 main application areas: databases, complexity and formal languages.
• Jouko Väänänen. A Short Course on Finite Model Theory. Department of Mathematics, University of Helsinki. Based on lectures from 1993-1994.
• Finite Model Theory Homepage at Aachen University of Technology, including a list of open problems
• Finite Model Theory References, a database of references related to finite model theory
• (en) H.-D. Ebbinghaus, Finite Model Theory, Berlin Heidelberg, Springer, 1995 (ISBN 3-540-65758-4)