Is there a finitely generated computably presentable group $G$ on generator set $A$ and a computable function $f$ from firstorder 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$– PhylliidaAug 13 '20 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. GoucherAug 13 '20 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 SteinbergAug 13 '20 at 22:27

1$\begingroup$ @BenjaminSteinberg better to also give a humanreadable 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) 457478 and here's a stable doi link: doi.org/10.1016/S0049237X(08)719141 $\endgroup$– David RobertsAug 14 '20 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 GoldbergAug 19 '20 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 NeisSorbi'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.

$\begingroup$ This is impressively nonconstructive. 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$ Aug 19 '20 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$ Aug 19 '20 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$ Aug 19 '20 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$ Aug 20 '20 at 2:53