Implication is not associative. This results in quite a bit of structure that can be used in set theory with things like ZFC, but I’m curious if it is necessary, as the parentheses can be annoying to deal with. While prefix and postfix forms are options, they often aren’t very readable.
Are there any sets of axioms that seem to have enough structure to act as a mathematical foundation while having only associative operators?
Because multiple associative operations can be composed to simulate implication (and thus not be associative), I think I’m looking for a single associative operator that is sufficient to simulate ZFC. If we are going that route, we might as well require inverse and identity as well so we can use group theory. This results in the formal question (thanks to @NoahSchweber):
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$?
I could imagine that question being answered in a non-constructive way, so a constructive answer is preferred. In words, I’m asking for an infinite group that has enough structure to correspond to the standard kinds of things discussed in mathematics. Unlike the classification of finite simple groups, we still don’t have a good handle on all infinite groups, and there are plenty of infinite groups with undecidable decision problems on them (for example), so it’s conceivable that there are some that are expressive enough to work.
I’ve been looking through alternate metamath axiom sets, but all of them so far seem to require some form of implication or other operator that isn’t associative.
EDIT: The followup question below/above was asked and answered affirmatively at mathoverflow.
In classical logic, implication doesn't need to be included as a primitive operation: we can define it in terms of the operations of negation and disjunction, which are respectively unary and associative, as $$A\rightarrow B\quad:\equiv\quad (\neg A)\vee B.$$ Indeed, the set of Boolean operations $\{\neg,\vee\}$ is functionally complete. So we can rewrite (say) all the $\mathsf{ZF}$ axioms using only disjunction and negation.
(You may also be interested in cylindrical algebras, which provide an algebraic semantics for first-order logic whose basic operations are all either unary or associative.)
Of course, taht doesn't actually solve the notation problem you mention: we still need parentheses to distinguish between e.g. $(\neg A)\vee B$ and $\neg(A\vee B)$. Basically, the problem is that associative operations can be combined to produce non-associative operations. If what we actually want is to avoid parentheses, then instead of changing our basic logical connectives we should instead (as Asaf Karagila comments) adopt something like Polish notation. For instance, the parentheses-laden expression $$p\rightarrow\neg(q\rightarrow r)$$ would be written as $$CpNCqr.$$ This, though, has the drawback of (at least in my experience) generally being less readable for long expressions, especially when quantifiers enter the picture.
You separately ask, however, a question about structures, e.g. whether there is
It's unclear to me exactly what this means, but there are certainly some observations we can make which seem relevant. Most obviously, we have on the one hand the set of first-order formulas modulo $\mathsf{ZFC}$-provable equivalence, and on the other hand - given a computably presentable group $G$ - the set of words on the generators of $G$ modulo equality given the presenting relations of $G$, and we could ask for an appropriate correspondence. The coarsest question is:
The answer is yes: we can in fact find a finitely presentable group $G$ such that the halting problem is many-one reducible to the word problem for $G$, and $\mathsf{ZFC}$-provable equivalence is many-one equivalent to the halting problem.
On a more algebraic note, we could ask:
I believe that the answer is yes - and in fact that we can use the same $G$ as before - but I don't know.
I added the "finitely generated" bit since without it the question is trivial: take a generator $a_\sigma$ for each formula $\sigma$ and consider an appropriate set of relations making $a_\sigma=a_\tau$ iff $\mathsf{ZFC}\vdash\sigma\leftrightarrow\tau$.