We show the FO bisimilarity/indistinguishability ≡ is both decidable and first order definable, ie there is a FO formula A(.,.) such that x ≡ y <-> A(x,y) holds for any x,y in the model M We use it to quotient the model M and get a discrete model (based on the finite type pos n) where identity coincides with FO bisimilarity. The idea of the construction is the following. We start from a finitary signature Σ to simplify the explanation but the devel below works in a sub-signature of Σ where the list ls bounds usable terms symbols and the list lr usable bound relations symbols. So given a finitary Σ and a finite and Boolean model M for Σ, we define the operator F : (M² -> Prop) -> (M² -> Prop) transforming a binary relation R : M² -> Prop into F(R). x F(R) y iff t(x) R t(y) for any t(.) = s<v(./p)> and f(x) <-> f(y) for any f(.) = r<v(./p)> Then F(.) is monotonic, ω-continuous, and satisfies I ⊆ F(I), (F(R))⁻ ⊆ F(R⁻) and F(R) o F(R) ⊆ F (R o R) hence Kleene's greatest fixpoint gfp(F) exists, is obtained after ω-steps and is an equivalence relation. Moreover, F preserves decidability and FO-definability. Now we show that gfp(F) ~ F^n(TT) for a finite n which implies that gfp(F) is decidable and FO-definable. Here TT := fun _ => True is the full binary relation over M. The sequence n => F^n(TT) is a sequence of decidable (hence also weakly decidable) relations. If F^a(TT) ⊆ F^b(TT) for a < b then we have F^a(TT) ~ F^i(TT) for any i => a and thus for any i >= a F^i(TT) ~ gfp F. The sequence n => F^n(TT) belongs to the weak power list of binary relations over M (upto equivalence) which contains all weakly decidable binary relations over M. By the PHP, for n greater that the length of this list (which is 2^(m*m) where m is the cardinal of M), we must have F^a(TT) ~ F^b(TT) for a <> b, hence we deduce F^n(TT) ~ gfp F. Hence, gfp F is decidable and FO-definable as well.

fo_bisimilar means no FO formula can distinguish x from y. Beware that two free variables might be needed, see the remarks and counter-example below

Let us assume a finite and Boolean model m

Construction of the greatest fixpoint of the following operator fom_op. Any prefixpoint R ⊆ fom_op R is a simulation for the model

First we show properties of fom_op a) Monotonicity b) preserves Reflexivity, Symmetry and Transitivity c) ω-continuous d) preserves decidability e) preserves FO definability

Monotonicity

Reflexivity, symmetry & transitivity

Now we build the greatest fixpoint fom_eq and show its properties a) it is an equivalence relation b) it is a congruence wrt to the model functions and relations c) it is decidable and FO definable the reason is that it is obtained after finitely many iterations of fom_op

We build the greatest bisimulation which is an equivalence and a fixpoint for the above operator

We show that the greatest bisimulation is equivalent to FOL undistinguishability. This result is purely for the sake of completeness of the description of fom_eq, it is not used in the reduction below It states that x and y are bisimilar iff there is no interpretation of a FO formula that can distinguish x from y

By fom_eq_form_sem above, we know there is a FO formula A(.,.) in two free variables such that x ≡ y <-> A(x,y). One obvious follow up question is can we show x ≡ y <-> A(x) <-> A(y) for any A(.) with one free variable Another obvious follow up question is, for a given x in the model, can one characterize the class of { y | x ≡ y } with a formula Ax(.) with one free variable. Both questions have a negative answer proved in the counter example to be found below. There is a model of Σ = {ø,{=²}} with two distinct values where =² is interpreted by identity and such that A(x) <-> A(y) for any formula with at most one free variable. See theorem FO_does_not_characterize_classes.

And because the signature is finite (ie the symbols and relations) the model M is finite and composed of decidable relations We do have a decidable equivalence here

But we have a much stronger statement: fom_eq is first order definable which follows from the fact that X/M is finite

We build a single FO formula with two variables A.,. such that x ≡ y <-> A(x,y)

And now we can build a discrete model with this decidable equivalence. There is a fo_projection from M to Md where Md is a Boolean model based on the ground type pos n.

Every finite & decidable model can be projected to pos n with decidable relations and such that identity is exactly FO undistinguishability

We show that there is a model over Σ = Σrel 2 = {ø,{=²}} where ≡ is identity but x ≡ _ is not definable by a FO formula with a single free variable There are two non equivalent values that cannot be distinguished when using a single variable Even though ≡ is FO definable by a formula with two free variables, equivalences classes of ≡ are not FO definable

There is a model over Σ2 with two values such that no FO formula with one free variable can distinguish those two values, but there is a FO formula with 2 free variables that distinguishes them