Finite Model Theory/FO BFP

Discrimination, Subtask: How to describe a set of structures independent from a logic? Easy for finitely describable structures: by a finite set of structures.

Difficult: Infinite set of structures. Approach: the notion of pattern, i.e. Partial Isomorphisms that can be enhanced by induction.

$\exists _{x}\exists _{y}xRy$, can be described by single structure, like:

$\exists _{x}\exists _{y}\neg xRy$, can be described by a set of structures of size 2, like:

$\neg \exists _{x}\exists _{y}xRy$, requires infinitely many structures, since ...

In the latter case it is important how the pattern is extended, thus we need a rule for it. This can be achieved by induction, i.e. a structure for which the pattern holds is extended by a single element s.t. the pattern applies for x and y (i.e. all unified variables) with this element.

So, finally we get a structure where the pattern is applied to each single combination of elements (for the unifier case) - i.e. for all elements - and this is where FO comes in here.

In the basics section we defined the notion of finite (partial?) isomorphism. Now one can ask for a reasonable definition of two structures being finitely isomorphic. We discuss miscellaneous approaches here and will see that - on finite relational structures - one is equivalent to the concept of elementary equivalence.

Loosely Finite Isomorphic Structures

All or Any

i.e. there is any subset of A with a FI to B, what is trivial in most cases, since one can pick a single element from each A and B. But on the other hand requiring that for all subsets of A there is a FI would demand a total FI from A to B i.e. would include the notion of Isomorphism(?):

Total

So one can make the definition relative to the domain-size m of FI, that is:

(shallow)

(deep)