Fix an -categorical structure . The simplest, and already interesting case is , the pure countable set.
We consider the definable graph isomorphism problem for graphs which are definable (equivalently, interpret in) :
Problem: DefGraphIso
Input: Two definable graphs
Output: Yes, if and are isomorphic, No otherwise.
Below we make some very basic observations concerning this problem.
The input is represented by two expressions defining and , such as the one below, defining the infinite Johnson graph:
(in general, an expression is a nested application of finite unions of set-builder expressions with parameters ranging over using first-order guard formulas in the language of ).
Remark 1. Equivalently, and are specified by two first-order interpretations from , where an interpretation specifies the dimension , a formula with free variables, a formula with free variables, and a formula with free variables, and defines the graph where: is the interpretation of in , is the interpretation of in , which assumed to be contained in , and is the interpretation of in , and is assumed to be a congruence of the graph (otherwise, the graph is undefined).
Remark 2. We assume that the expressions do not contain constants from . This assumption can be dropped without generality if , since in that case, every definable structure whose definition uses constants can be effectively converted into isomorphic structures defined by expressions which do not use constants. I don’t know whether this works for other .
Example 1. Since definable graphs are closed under disjoint unions, the disjoint union of two copies of the Johnson graph is also definable. Clearly embeds into . It is not difficult to see that also embeds into : it is enough to partition all atoms into two disjoint, infinite sets , and then consider the subgraphs of induces by those vertices, which only use atoms from the set (respectively, ). Clearly, both are isomorphic to . However, the graph is not isomorphic to , as is connected, and of diameter (there is a path from the vertex to the vertex , which goes through the vertex ). Therefore, the graphs and can be distinguished by the first-order sentence .
We will use the following, standard result.
Lemma 1. Suppose that is definable over an -categorical structure . Then
- is -categorical,
- Every relation which is invariant under the automorphisms of is also invariant under the automorphisms of (the converse implication does not always hold),
- A relation is -invariant if and only if it is first-order definable in , i.e., it can be defined in the structure .
Below are several simple observations concerning the above decision problem.
Proposition 1. The problem DefIso is co-recursively enumerable.
Proof. Since is -categorical, is isomorphic to if and only it satisfies exactly the same first-order sentences as . For a given sentence , one can effectively test whether it holds in , or in . One can enumerate all sentences , and for each of them test whether it holds in and not in . Such a formula is found if and only if and are non-isomorphic.
We now list several other related problems. Unless stated otherwise, when we say definable we mean definable with respect to , without constants.
- DefStructureIso. The input consists of two definable relational structures and , and the question is whether they are isomorphic.
- DefRel. The input consists of a definable relational structure and a definable relation , and the question is whether is first-order definable in . This problem is basically Problem 29 stated in the paper “Decidability of Definability” by Bodirsky, Pinsker, Tsankov. There, they consider the case when is an ordered, homogeneous, Ramsey, finitely bounded relational structure over a finite signature (this implies -categoricity, in particular), and is a reduct of (i.e., it is definable over and has the same domain as ).
- DefUnaryRel. The same question as above, but restricted to unary relations .
- Orbit. The input consists of a definable structure and a definable unary relation , and the question is whether is a single orbit with respect to , the automorphism group of .
- SameOrbit. The input consists of a definable relational structure and two elements . The question is whether and lie in the same orbit under the group of automorphisms of . The elements and are represented by specifying their orbits and under the action of . It follows from Lemma 1, item 2, that the answer to the question does not depend on the choice of the representatives . (One could also represent the elements using expressions with constants from ; however, in the proof below we will avoid introducing extra constants).
Proposition 2. All the above problems, and the DefIso problem, are inter-reducible.
Proof. The DefGraphIso is a special case of the DefStructureIso problem, and conversely, for any finite relational signature it is standard to construct a first-order transduction converting -structures into graphs, so that and are isomorphic if and only if and are isomorphic. The structures and are computable from and .
The DefStructureIso problem reduces to the SameOrbit problem. Given a structure , construct a structure obtained from by adjoining a new ‘apex’ node , connected to all nodes of by a new relation called . Given two structures and , construct the disjoint union . Then and are isomorphic if and only if the two apices are in the same orbit of .
Conversely, the SameOrbit problem reduces to the DefStructureIso problem: Given , where and are -orbits of , the sets and are contained in a single -orbit if and only if the structure is isomorphic to the structure .
The SameOrbit problem reduces to the Orbit problem. Indeed, assuming the Orbit problem is decidable, one can enumerate all -orbits of a given structure : by the second item of Lemma 1, it suffices to enumerate all unions of -orbits of , and for each such union, test whether it is an orbit of under .
Conversely, the Orbit problem reduces to the SameOrbit problem: one can enumerate all pairs of -orbits contained in , and for each of them test whether they are contained in the same -orbit of .
The Orbit problem reduces to the DefUnaryRel problem: is an -orbit if and only if it is an inclusion-minimal -invariant subset of . All such invariant subsets can be enumerated, since they are unions of -invariant subsets of by the second item of Lemma 1, and a union of -orbits of is -invariant if and only if it is definable in . Minimality can be checked, since containment of two definable sets is decidable.
Conversely, the DefUnaryRel problem reduces to the Orbit problem, since by the third item of Lemma 1, a unary relation is definable if and only if it is a union of -orbits of .
Clearly, the DefUnaryRel problem is a special case of the DefRel problem. Conversely, given a structure and a relation , we expand the structure to the structure , where is treated as a unary relation on , and is treated as a binary relation– the graph of the th projection from to .