Is there a finitely generated computably presentable group $G$ on generator set $A$ and a computable function $f$ from first-order formulas to words on $A$ such that $\mathsf{ZFC}\vdash\sigma\leftrightarrow\tau$ iff $f(\sigma)$ and $f(\tau)$ represent the same element in $G$?

  • $\begingroup$ Note that is migrated from a question arising from a post on math stack exchange, as recommended by Noah Schweber math.stackexchange.com/q/3776818/155079 $\endgroup$ – Phylliida Aug 13 at 21:01
  • 1
    $\begingroup$ As a response to your comment "Because neither NAND or NOR are associative I was fiddling with trying to come up with a more than two parameter Boolean universal gate that is associative, and considering going into multivalued or ternary logic to achieve that", the group $A_5$ works -- see this discussion of Barrington's theorem: crypto.stanford.edu/~dabo/pubs/papers/barrington.html $\endgroup$ – Adam P. Goucher Aug 13 at 21:50
  • $\begingroup$ Maybe look at sciencedirect.com/science/article/pii/S0049237X08719141 I think it tries something more logic oriented for the word problem $\endgroup$ – Benjamin Steinberg Aug 13 at 22:27
  • 1
    $\begingroup$ @BenjaminSteinberg better to also give a human-readable reference in case that url breaks: Ralph McKenzie and Richard J. Thompson, An Elementary Construction of Unsolvable Word Problems in Group Theory, Studies in Logic and the Foundations of Mathematics 71 (1973) 457-478 and here's a stable doi link: doi.org/10.1016/S0049-237X(08)71914-1 $\endgroup$ – David Roberts Aug 14 at 2:01
  • 3
    $\begingroup$ Isn't it enough to have a finitely generated computably presentable group whose word problem is $\Sigma^0_1$-universal? This paper constructs such a group: arxiv.org/pdf/1609.03371.pdf $\endgroup$ – Gabe Goldberg Aug 19 at 18:29

The relation $\text{ZFC}\vdash\varphi\leftrightarrow \psi$ is a $\Sigma_1^0$-definable equivalence relation on the set $\mathcal L$ of formulas in the language of set theory. It is a corollary of Theorem 3.2 of Neis-Sorbi's "Calibrating word problems of groups via the complexity of equivalence relations" that there is a finitely generated computably presentable group with generator set $A$ whose word problem, viewed as an equivalence relation $\sim$ on the set $W$ of words on $A$, is $\Sigma_1^0$-universal. As a consequence there is a reduction from the former equivalence relation to the latter, and this just means that there is a computable function $f : \mathcal{L}\to W$ such that $f(\varphi) \sim f(\psi)$ if and only if $\text{ZFC}\vdash\varphi\leftrightarrow\psi$, which is what you want.

| cite | improve this answer | |
  • $\begingroup$ This is impressively non-constructive. Thanks, this is great and what I was looking for so I’ll accept it, but I am curious if there are any more natural groups that are \Sigma^0_1 Universal, as that one seemed fairly messy. This links me to the rabbit hole of papers in the domain I was looking for (and did not know existed), so it’s helpful regardless $\endgroup$ – Phylliida Aug 19 at 21:18
  • $\begingroup$ I don't know anything about this topic, I was just feeling lucky on Google. But someone asked a related question here. It seems to me that no one was able to provide a natural group whose word problem is undecidable... $\endgroup$ – Gabe Goldberg Aug 19 at 21:31
  • 5
    $\begingroup$ @Phylliida A minor quibble: it's totally constructive, it's just messy. In fact it's a bit better than merely constructive in this particular instance: the original paper of Miller they build on gives a uniform construction for turning a ceer into a group of the appropriate nature. $\endgroup$ – Noah Schweber Aug 19 at 21:43
  • 1
    $\begingroup$ @NoahSchweber yes I realized that after I made my comment and did more reading, oops. I’ve been going through the construction to get exactly what the function and group is for my other question. $\endgroup$ – Phylliida Aug 20 at 2:53

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.