0
$\begingroup$

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.

$\endgroup$
8
  • 1
    $\begingroup$ Polish notation requires no parenthesis. $\endgroup$
    – Asaf Karagila
    Aug 1 '20 at 18:06
  • 1
    $\begingroup$ It's unclear to me what your goal is, which makes it hard to decide how to approach an answer to your title question. "Parentheses can be annoying to deal with" makes it sound like maybe you'd be satisfied by a parenthesis-free notation like prefix notation. But taking you at the rest of your words that you do want a foundation with only associative stuff, I'm not sure what it would mean to have a "foundation of mathematics" that can't simulate things like implication or entailment. I'm genuinely curious about your question, but a bit lost. $\endgroup$
    – Mark S.
    Aug 1 '20 at 18:06
  • 4
    $\begingroup$ Well, negation and disjunction are already enough to get all propositional connectives, and disjunction is associative (and negation is unary, so there's nothing to talk about there). Implication is just shorthand: $A\rightarrow B$ is $(\neg A)\vee B$. Keep in mind that associative operations can be combined to produce non-associative operations. $\endgroup$ Aug 1 '20 at 18:29
  • $\begingroup$ @NoahSchweber your last question in your answer is actually what I was asking. It forces identity and inverse as well, but that’s probably okay. Sorry for being unclear. $\endgroup$
    – Phylliida
    Aug 1 '20 at 20:18
  • 1
    $\begingroup$ @Phylliida Also incidentally, you may be interested in this result - it's not about equality of group elements, but still within the broader "can there be a 'computationally rich' group?" topic. $\endgroup$ Aug 1 '20 at 23:20
3
$\begingroup$

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

a certain infinite group that has enough structure to correspond to the standard kinds of things discussed in mathematics.

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:

Is there a finitely generated computably presentable group $G$ whose word problem is as complicated as the problem of telling whether two sentences are $\mathsf{ZFC}$-provably equivalent?

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:

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 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$.

$\endgroup$
3
  • $\begingroup$ Ah yes, you raise a good point that parenthesis matters when you try and simulate implication with multiple different associative primitives. We need to use a single associative operator (or multiple that play nicely, but it’s probably better to just use one). 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. Regardless, I think your final question is a very precise formulation of exactly what I was asking for. $\endgroup$
    – Phylliida
    Aug 1 '20 at 20:12
  • $\begingroup$ As the last question is the one I am interested in and a great formalization of what I’m asking, I’m not going to accept this answer until it is answered, but thank you, this was very insightful $\endgroup$
    – Phylliida
    Aug 1 '20 at 20:23
  • $\begingroup$ @Phylliida Glad to help! (I think you should edit that into your question, then - it will make it much clearer.) $\endgroup$ Aug 1 '20 at 21:03

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.