Consider the following decision problem (for classical Turing machines). Let be a fixed, finite signature.
Input: Two orbit-finite relational structures , over .
Decide: is there a homomorphism from to ?
Question 1. Is the above problem decidable?
Observe that we are not asking for the existence of an equivariant homomorphism. If this were the case, the problem would be clearly decidable, since there are only finitely many equivariant homomorphisms between orbit-finite sets, and they can be effectively scanned. In this problem, the homomorphisms do not even have to be finitely supported! Below is an example where a homomorphism exists, but no finitely supported homomorphism exists.
Example. Consider the equality atoms. Let be the graph whose vertices are pairs of distinct atoms, and in which edges join a pair with its inverse. Let be the -clique. Then maps to , but no finitely supported homomorphism exists.
Following the idea of this post, in order to solve this problem, it might be useful to move to the totally ordered atoms .
Question 2. In the totally ordered atoms, if there is a homomorphism between orbit-finite structures , , is there one which is equivariant?
A positive answer to Question 2 would imply a positive answer to Question 1.
Edit. After reading Bartek’s comment below, I noticed that Question 2 has an even more negative answer. Consider the structures and (orders reversed). There is a homomorphism from to , namely the mapping , but there is none which is finitely supported.
If Question 2 is true, it must use the fact that the signature is finite. Otherwise, even if the signature is equivariant and orbit-finite, there is a counterexample:
Consider a signature with a family of unary predicate symbols indexed by (totally ordered) atoms; this is a single-orbit signature. Then, take a structure with the set of atoms as the universe, where each predicate is interpreted as the singleton . Further, let be a structure over the same universe, but with each predicate interpreted as the complement of .
Homomorphisms from to are exactly those functions on atoms that have no fixpoints. There are many such functions, but none of them is finitely supported over totally ordered atoms.
Oh wait a minute. Question 2 is false for a trivial reason, mentioned already at the beginning of this entry.
Consider the empty signature, a singleton set and the set of atoms. No function from to is equivariant.
This says nothing about Question 1, because the kind of problem present in this example is very easy to detect: an element with a small support in , which cannot be mapped to anything in .