Talk:Finite model theory

Perhaps we could mention that finite model theory might help us resolve P vs. NP? (See http://www2.ing.puc.cl/~jabaier/iic2212/poll-1.pdf for instance). My understanding is that several finite model theorists are in that field in hopes of conquering this major problem. Any thoughts?

Core

single structure

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

1. every node has an edge to another node: ...
2. no node has an edge to itself: ...
3. there is at least one node that is connected to all others: ...

Now do these properties describe the structure uniquely (up to isomorphism)? Obviously not since for structure (2) 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).

For a single finite structure this is always possible. The principle is quite simple:

1. say that there are at least 5 elements: ...
2. say that there are at most 5 elements: ...
3. state every edge of the graph: ...
4. state every non-edge of the graph: ...

fixed number of structures

We have seen that a single finite structure can be described in FO up to isomorphy. So what about, say 2, structures, like (1) and (3)? A unique description can easily been achieved by joining the single descriptions for (1) and (3). Thus, as long as a finite fixed number of structures is given, a description can be achieved easily.

finite number of structures

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.

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. — Preceding unsigned comment added by Sterling (talk • contribs) 21:19, 16 February 2011 (UTC)

infinite number of structures

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.

Materials

the Craig interpolation lemma, and the Łoś–Tarski preservation theorem — Preceding unsigned comment added by Sterling (talk • contribs) 11:08, 16 January 2011 (UTC)

One important subfield of finite model theory, descriptive complexity, connects the expressivity of various logical languages with the capabilities of various abstract machines. For example, if a language can be expressed in first-order logic with a least fixed point operator added, a Turing machine can determine in polynomial time (see P) whether a given string is in the language. Descriptive complexity allows results to be transferred between computational complexity and mathematical logic and gives additional evidence that the standard complexity classes are "natural." Neil Immerman states Sterling (talk) 12:15, 16 January 2011 (UTC)

Another important result of finite model theory are the zero-one laws, which establish that many types of logical formulas hold for either almost all or almost no finite structures. For example, the proportion of graphs of size n that are connected approaches one as n approaches infinity, while the proportion that contain an isolated vertex approaches zero. In fact the same is true of any graph property that can be defined in first-order logic: it either approaches one or approaches zero. This has ramifications for randomized algorithms on large finite structures.