User:Modelpractice/sandbox

This is the user sandbox of Modelpractice. A user sandbox is a subpage of the user's user page. It serves as a testing spot and page development space for the user and is not an encyclopedia article. Create or edit your own sandbox here.

Other sandboxes: Main sandbox | Template sandbox

Finished writing a draft article? Are you ready to request review of it by an experienced editor for possible inclusion in Wikipedia? Submit your draft for review!

Trakhtenbrot's Theorem

For every relational vocabulary σ with at least one binary relation symbol, it is undecidable whether a sentence Φ of vocabulary is finitely satisfiable. [i.e. has a finite model]

Corollaries

The set of finitely valid sentences of σ is not recursively enumerable.
There is no recursive function f such that: if Φ has a finite model, then it has a model of size at most f(Φ).

Approach

Instead of a general statement, the following is a sketch of a methodology to show if a set of structures can or cannot be described up to isomorphy in FO.

Prerequisites:

A Ehrenfeucht–Fraïssé game (EFG) is a game on two structures, played two players, the spoiler and the duplicator, that either must win. Its moves can be restricted to a certain number, what makes it easier for the duplicator to win.
The quantifier rank (qr()) of a formula is the maximal depth of its quantifier nesting. Notice that qr() is a concept on languages, not on structures.

Given a property P over a set of structures. The methodology makes use of the correspondence between m-move Ehrenfeucht games (EFG) and FO[m], the FO sentences of quantifier rank less or equal m, like this:

for two structures A, B, where A has P and B doesn't, the so called duplicator wins the m-move EFG on A, B iff A, B can be discriminated in FO[m], else the so called spoiler wins. So, by inductively expanding A, B to higher m and playing EFG on it, it can be shown if P can be described uniquely in FO.

1. One wants to find a FO sentence to discriminate 2 disjoint sets. For example the even (EVEN) and odd elements of a linear oder.

2. Since such a sentence must have a quantifier rank, one checks all FO sentences by induction over their quantifier ranks. Let FO[i] denote the initial step. For example, FO[2] denotes all FO sentences with qr=2, and A₂ = {1, 2, 3, 4} and B₂ = {1, 2, 3, 4, 5} are two sets which cannot be discriminated in FO[2]. The latter is shown by a 2-move EFG. Before A₂ and B₂ have to be found, appropriately.

3. For example, A₂ and B₂ can be discriminated in FO[3]. However, they can be extended to A₃ and B₃ s.t. discrimination in FO[3] always fails.

4. For example, for FO[m] some A_m, B_m can be found (with A_m, B_m of length 2^m, 2^m+1), s.t. in the m-move EFG on A_m, B_m the duplicator always wins, and thus it is shown that EVEN (on linear orders) cannot be described uniquely up to isomprphism in any FO sentence (of any quantifier rank).

In general the methodology is as follows. Suppose we want to show that a property P is not expressable in a logic L. We then partition the set of all sentences of L in countably many classes L[0], L[1], ..., L[k], ... and find two families of structures {A_k | k ∈ ℕ} and {B_k | k ∈ ℕ}, such that every L[k] sentence holds for A_k and B_k although A_k has property P and B_k doesn't (since they were chosen that way).

Text

In general the methodology is as follows. Suppose one wants to show that a property P is not expressable in a logic L. If P were expressible in L, every two structures where one has P and one doesn't would be discriminatable by a L-sentence, thus one has to show there is at least one pair of structures A and B such that on one hand A has P and B doesn't although on the other hand there is no L-sentence that holds for A but not for B (or for B and not for A).

What kind of evidence can one expect? As shown above, a fixed pair A, B could always be described and thus discriminated in FO. Thus, an aproach to look for a single pair A, B must fail (at least in FO or higher languages) Thus, a basic approach has to look for a pair A, B for each L-sentence. Fortunately, this can be simplified by two ideas. Firstly, partitioning all L-sentences into classes, s.t. a single pair A, B is sufficient for each. Secondly, expanding A, B inductively over these classes.

This leaves one with two issues:

how to classify the L-sentences?
how to construct such A, B inductively?

Prerequisites:

A Ehrenfeucht–Fraïssé game (EFG) is a game on two structures, played by two players, the spoiler and the duplicator, that either must win. Its moves are restricted to a certain number.
The quantifier rank (qr()) of a formula is the maximal depth of its quantifier nesting. Notice that qr() is a concept on languages, not on structures.

For classification (1.), the main idea in FO (and also higher languages) is to use the correspondence between Ehrenfeucht–Fraïssé game (EFG) and quantifier rank (qr()). A, B are not discriminateable in FO[m] (all FO-sentences of qr()=m) iff the duplicator in an m-move EFG has a winning strategy. For induction (2.) the approach has to be chosen individually for each structure.

So, we get the following proof schema:

define a language L, a kind of structures S, and a property P.
choose a initialy qr()=1 construct a pair A₁, B₁ of S-structures, where A has P and B doesn't.
prove that A₁, B₁ cannot be discriminated in L[1], by employing a 1-move EFG on A₁, B₁ (in case of FO).
pick an arbitrary A_m, B_m and define an extension rule for it to A_m+1, B_m+1
show that if the duplicator wins the m-move EFG on A_m, B_m it also wins the m+1-move EFG on A_m+1, B_m+1.

Notice, that since winning the i-move EFG for the duplicator implies that it wins the i-1-move EFG as well, the proof can be simplified, by 'overleaping' some of the increments (not necessary for basic understanding).