Deciding isomorphism between graphs which interpret in the pure set

Question

I am interested in the following decision problem:

Given descriptions of two graphs $G,H$ which interpret in the pure set $\mathbb N=(\{0,1,2,\ldots\},=)$, decide whether $G$ and $H$ are isomorphic.

The question is: is this problem decidable at all?

(A graph $G$ is represented by a triple of formulas $(\phi_{\text{dom}},\phi_{\sim},\phi_E)$ describing the interpretation in the usual way (namely, $\phi_{\text{dom}}$ is a formula with $d$ free variables for some $d\in\mathbb N$, defining a set $V\subset \mathbb N^d$, $\phi_{E}$ has $2d$ free variables and defines a symmetric binary relation $E\subset V\times V\subset \mathbb N^{2d}$, and $\phi_\sim$ is a formula with $2d$ free variables defining a binary relation $\sim\subset V\times V$ which is a congruence of the graph $(V,E)$ (i.e. the edge relation is invariant under $\sim$). The graph $G$ is defined as the quotient graph $(V,E)/\sim$ with vertices $V/\sim$ and edges $\{[v],[w]\}$ such that $(v,w)\in E$.)

The graphs $G,H$ are ω-categorical and therefore, whenever they are non-isomorphic, there is a sentence $\phi$ which distinguishes $G$ from $H$. Since it can be effectively tested whether $\phi$ holds in $G$ and in $H$, it follows that non-isomorphicity is recursively enumerable. Therefore, the question which remains is whether there is an effective witness of isomorphicity, which would probably require some form of structure theorem for these graphs.

These graphs are ω-categorical, ω-stable, and moreover they are coordinatized by indiscernible sets, as in the eponymous paper by Lachlan, so perhaps the structure theory developed in this paper could be of use. (In this question I ask if those two classes coincide:ω-categorical, ω-stable structure with trivial geometry not definable in the pure set).

My question could be generalized to graphs which interpret in other structures with decidable first order theory, e.g., the dense linear order.

---

Edit 1: I modified the question so that it talks about graphs rather than arbitrary structures. Those two questions are easily seen to be equivalent.

---

Edit 2: I wrote down some preliminary observations concerning this problem here: http://atoms.mimuw.edu.pl/?p=1063

Answer 1

Update. As noted in the comments, this answer applies only to definable quotients of $\mathbb{N}$, rather than $\mathbb{N}^d$, and so it doesn't answer the question.

---

The answer is yes, your relation is computably decidable.

To see this, observe first that the theory of the structure $\langle\mathbb{N},=\rangle$ admits elimination of quantifiers. This can be easily proved by induction on formulas in the usual elimination-of-quantifiers manner.

If $A$ is a definable structure in $\langle\mathbb{N},=\rangle$, then the domain, quotient relation and fundamental relations of $A$ are each defined by a quantifier-free formula with parameters. Furthermore, given the defining relations of $A$, then since the elimination of quantifiers argument is effective, we can computably find those quantifier-free formulas. You didn't seem to allow parameters in the definitions, but I claim that we can even allow parameters in the definition and it will still be computable.

The quantifier-free definable sets, without parameters, are exactly the empty set and the full set. With parameters $b_0,\dots,b_n$, the quantifier-free definable sets will be the subsets of the parameter list, plus possibly the complement of the parameter set. So, the finite and co-finite sets.

Furthermore, we can tell from the quantifier-free definition which case we are in. So if we are given the definitions of $A$ and $B$, we can tell whether the pre-quotient domains have the same size or not.

The equivalence relation used in the quotient will be similarly trivial, since outside the parameter set, it must either identify all points or none, and we can computably tell exactly which. And on the parameter set, we will be able to read off from the quantifier-free definition exactly what it does on the parameter list. So given the definitions of $A$ and $B$, we can computably decide whether the quotients have the same size or not. Indeed, the quotient is essentially trivial outside the parameter set, since it must either collapse the entire complement of the parameter set or none of it.

Similarly, I claim that we can computably decide the nature of the other relations. Basically, the quantifier-free definition of any relation using parameters is specified in a computably decidable manner on the elements of the parameters themselves, and all distinct elements outside the parameter list are indiscernible for that relation. So there are finitely many types of elements, which can simply be read directly from the definition of the relation.

I claim that this implies that the isomorphism relation for your structures is computably decidable. Each $n$-ary relation has essentially finitely many types of instantiations and non-instantiations, by considering the points of the parameters and then the indiscernibles of the non-parameters. Given pairs of finitely many such relations, we can determine if there is an isomorphism of the quotient structures: the domains should have the same size, and then the relations should be determined by a rearrangement of the parameter set and a matching of the indiscernibility nature of the relations outside the parameter set.