Talk:Finite model theory

P vs. NP

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? — Preceding unsigned comment added by Fermat2001 (talk • contribs)

That's basically speculation. It depends who you ask. Tijfo098 (talk) 08:43, 8 November 2012 (UTC)

Core

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

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.

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.

Sterling (talk) 22:00, 16 February 2011 (UTC)

The construction of a single formula doesn't work if there are infinitely many predicate symbols. The claim that a given model can be described by a single formula doesn't appear to hold in that case. 2603:3024:184B:C100:B4CD:B680:D0D:5DD6 (talk) 18:30, 21 March 2023 (UTC)

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.

Libkin 2004: Textbook "Elements of Finite Model Theory" with computational focus, especially embedded finite models — Preceding unsigned comment added by Sterling (talk • contribs) 22:51, 16 February 2011 (UTC)

References

FO

The article uses the abbreviation "FO" but doesn't define it.Linguistatlunch (talk) 21:34, 22 April 2011 (UTC)

Fixed. 81.131.5.211 (talk) 22:21, 10 July 2011 (UTC).

Database old example

Think of an online-forum. It consists of postings that can have child postings answering them. All together this forms a tree structure with the forum main page seen as a root posting. Thus we have a table "posting" with a relation "answers" from posting to posting. Here all answers of a posting with id "1234" can easily be queried as follows:

SELECT *
FROM posting
WHERE posting.answers = '1234';

To obtain the children and grandchildren of "1234" we write:

SELECT * FROM posting
WHERE posting.answers = '1234' OR posting.answers = 
(
 SELECT id FROM posting
 WHERE posting.answers = '1234';
)

For a fixed number of generations this can be extended in SQL (although writing a query for 67 generations is not really a nice job). However we don't know how long a single thread can get. All we know is it must be of finite length. This cannot be expressed in the SQL expressions used above. Therefore we need an extension such as "START WITH ... CONNECT BY ...":

SELECT * FROM posting
START WITH posting.id = '1234'
CONNECT BY PRIOR posting.id = posting.answers;

All the above correspond to logic expressions. The 1st and 2nd query can be expressed in FO, whereas the 3rd query requires some extension like fixed-point-logics.

answers( x, 1234 )

answers( x, 1234 ) ∨ ∃_y ( answers( x, y ) ∧ answers( y, 1234 ) )

... — Preceding unsigned comment added by Modelpractice (talk • contribs) 17:26, 30 May 2012 (UTC)

I've linked to Codd's theorem now. You're right that not all the queries in SQL can be described in FO. The Oracle extension you mention in your last example is discussed in the article on transitive closure (vis-a-vis of logic expressiveness). Tijfo098 (talk) 08:29, 8 November 2012 (UTC)

Intro old

Proofs:Since many central theorems of MT do not hold when restricted to finite structures, FMT is quite different from MT in proof methods. Failing central results include the compactness theorem, Gödel's completeness theorem, and the method of ultraproducts for first-order logic. Some concepts become meaningless like that of types (and thus need to be redefined in FMT). Other methods like Ehrenfeucht games become more central in FMT.

Finiteness: As MT is closely related to mathematical algebra, FMT became an "unusually effective" instrument in computer science. This may have its origin in the fact that the valid first order (henceforth FO) sentences over all finite structures are not recursively enumerable, i.e. from a mathematical point of view they are 'just' finite but computer scientifically they can be seen as quite complex objects of study. In other words: "In the history of mathematical logic most interest has concentrated on infinite structures....Yet, the objects computers have and hold are always finite. To study computation we need a theory of finite structures."

Applications: The area of descriptive complexity theory connects complexity classes with structures and sentences of logics, to gain new insights and justifications to computational complexity. In database theory query languages can be formalized by parts and extensions of FO. In formal language theory the expressive power of languages corresponds to certain logics on finite structures.

Character: 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.

--Modelpractice (talk) 15:39, 5 June 2012 (UTC)

References