Group presentations defined by logical symbols as generators and logically equivalent wff as relators

Question

Suppose we have a nonempty alphabet $A$ with finitely many variables (for simplicity) $P_1,\dots, P_n$ and a bunch of logical symbols (e.g. $\to, \land$), together with $(,)$ if you so please; suppose we have a logic $\mathscr{L}$. Let $\varphi$ be a well-formed formula in $A$. Consider the group presentation

$$\mathcal{P}_{A}^{\mathscr{L}}(\varphi)=\langle A\mid \{\theta \in A^\ast: \varphi\equiv_{\mathscr{L}}\theta\}\rangle,\tag{$P$}$$

where $A^\ast$ is the Kleene star of $A$, and $\varphi\equiv_{\mathscr{L}}\theta$ reads, "$\varphi$ is logically equivalent to $\theta$ in the logic $\mathscr L$".

Has this been studied before?

---

For example, if $\varphi:=(P\land(P\to Q))\to Q$ under classical logic $\mathscr{L}:={\rm CL}$ and $A:=\{ P,Q, \to, \land, (,)\}$, then

$$R:=\mathcal{P}_{A}^{{\rm CL}}(\varphi)=\langle P,Q, \to, \land, (,)\mid \{(P\land(P\to Q))\to Q, ((P\to Q)\land P)\to Q\}\cup E\rangle,$$

where $E$ is to be considered as the set of "et cetera formula", such as

$$((P\land(P\to Q))\to Q)\land((P\land(P\to Q))\to Q).$$

Let us assume that redundant parentheses can be ignored somehow through some clever definition of wff. For example,

$$(((((P\land(P\to Q))\to Q))))$$

is omitted from our relations.

---

Unless I'm mistaken${}^\dagger$, we have

$$\begin{align} \mathcal{P}_{\{P,Q, \to\}}^{{\rm CL}}(P\to Q)&=\langle P,Q,\to\mid P\to Q\rangle\\ &\cong \langle P,Q,\to\mid P^{-1}=\to Q\rangle\\ &\cong\langle Q,\to\mid \rangle\\ &\cong F_2, \end{align}$$

which is the free group of rank two.

---

$\dagger$: . . . and I'm beginning to think I am . . .

---

It might be interesting to consider these presentations for Polish notation.

Answer 1

There is some work in the Descriptive Complexity of Finite Groups:

• Descriptive Complexity of Finite Abelian Groups (https://www.worldscientific.com/doi/abs/10.1142/S0218196710006047)
• Describing finite groups by short first-order sentences (https://link.springer.com/article/10.1007/s11856-017-1563-2).
• On the Weisfeiler--Leman Dimension of Finite Groups (https://arxiv.org/abs/2003.13745)
• A Systematic Study of Isomorphism Invariants of Finite Groups via the Weisfeiler-Leman Dimension (https://arxiv.org/abs/2111.11908)
• On the parallel complexity of Group Isomorphism via Weisfeiler--Leman (https://arxiv.org/abs/2112.11487)

It is well-known that the Weisfeiler--Leman is equivalent to the logic $\textsf{FO} + \textsf{C}$, which is first-order logic with counting quantifiers.

This doesn't seem to be exactly what you're after, but it might be close enough to be of interest.

While the Descriptive Complexity of Finite Graphs has been well-studied, I believe this is the extent of the literature in the case of Finite Groups.