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$
$\endgroup$
9
-
$\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$– PhylliidaCommented Aug 13, 2020 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. GoucherCommented Aug 13, 2020 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 SteinbergCommented Aug 13, 2020 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 ♦Commented Aug 14, 2020 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 GoldbergCommented Aug 19, 2020 at 18:29
|
Show 4 more comments
1 Answer
$\begingroup$
$\endgroup$
4
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.
answered Aug 19, 2020 at 20:46
-
$\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$ Commented Aug 19, 2020 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$ Commented Aug 19, 2020 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$ Commented Aug 19, 2020 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$ Commented Aug 20, 2020 at 2:53