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

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

... or ...

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

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.