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.
, can be described by single structure, like:
, can be described by a set of structures of size 2, like:
, 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(?):
So one can make the definition relative to the domain-size m of FI, that is: