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).

In general the methodology is as follows. Suppose one wants to show that a property P is not expressable in a logic L, i.e. there is at least one pair of structures A and B such that A has P and B doesn't although there is no L-sentence that holds for one but not the other.

One then takes every sentence of L and constructs a pair A, B for it, of the above kind. 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, by expanding A, B inductively over these classes.

This leaves one with three issues: 1. how to classify the L-sentences? 2. how to find such a A, B for each class? 3. how to prove that A, B is not discriminatable by a sentence of the class?

1. The core idea is that whenever one wants to see if a Property P can be expressed in FO, one chooses structures A and B, where A does have P and B doesn't. If for A and B the same FO sentences hold, then P cannot be expressed in FO (else it can). In short:

$A\in P,B\not \in P$ and $A\equiv B$

where $A\equiv B$ is shorthand for $A\models \alpha \Leftrightarrow B\models \alpha$ for all FO-sentences α, and P represents the class of structures with property P.

2. The methodology considers countably many subsets of the language, the union of which forms the language itself. For instance, for FO consider classes FO[m] for each m. For each m the above core idea then has to be shown. That is:

$A\in P,B\not \in P$ and $A\equiv _{m}B$

with a pair $A,B$ for each $m$ and α (in ≡) from FO[m]. It may be appropriate to choose the classes FO[m] to form a partition of the language.

3. One common way to define FO[m] is by means of the quantifier rank qr(α) of a FO formula α, which expresses the depth of quantifier nesting. For example for a formula in prenex normal form, qr is simply the total number of its quantifiers. Then FO[m] can be defined as all FO formulas α with qr(α) ≤ m (or, if a partition is desired, as those FO formulas with quantifier rank equal to m).

4. Thus it all comes down to showing $A\models \alpha \Leftrightarrow B\models \alpha$ on the subsets FO[m]. The main approach here is to use the algebraic characterization provided by Ehrenfeucht–Fraïssé games. Informally, these take a single partial isomorphism on A and B and extend it m times, in order to either prove or disprove $A\equiv _{m}B$ , dependent on who wins the game.