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 differentiate between structures that can and cannot be discriminated.

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, and so takes the initial step FO[i]. 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].

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.