Talk:Finite model theory

Mathematics Start‑class Mid‑priority

	Mathematics portal This article is within the scope of WikiProject Mathematics, a collaborative effort to improve the coverage of mathematics on Wikipedia. If you would like to participate, please visit the project page, where you can join the discussion and see a list of open tasks.MathematicsWikipedia:WikiProject MathematicsTemplate:WikiProject Mathematicsmathematics
Start	This article has been rated as Start-class on Wikipedia's content assessment scale.
Mid	This article has been rated as Mid-priority on the project's priority scale.

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?

Outline

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. Kanellakis, Kuper, Revesz 1995: Constraint Query Languages -> infinite sets in databases -> algorithmic model theory.
7. Book: Ebbinghaus, Flum 1995: Finite Model Theory
8. Book: Immermann 1999: Descriptive Complexity
9. Book: Abiteboul, Hull, Vianu 1995: Foundations of Databases
Character: Discrimination of structures:
1. Every single finite structure can be characterized in a single FO sentence up to isomorphism.
2. This doesn't hold for classes of finite structures.
Methods are required to determine if a class of structures can be discriminated in a certain language, e.g. games, locality, 0-1 laws.
Extensions of FO can be thought of in order to discriminate these classes, fixed point logics, sub-SO logics.
Objects of study: FO, extensions of FO/ restrictions of SO, sub-FO

Sterling (talk) 00:48, 16 January 2011 (UTC)[reply]

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)[reply]

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)[reply]

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.^[1] This has ramifications for randomized algorithms on large finite structures.

^ Immerman, Neil (1999). Descriptive Complexity. New York: Springer-Verlag. p. 6. ISBN 0-387-98600-6.

[Immerman_history-1] Immerman, Neil (1999). Descriptive Complexity. New York: Springer-Verlag. p. 6. ISBN 0-387-98600-6.

[1]