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.