# Do we have to prove how parentheses work in the Peano axioms?

One thing that has bothered me so far while learning about the Peano axioms is that the use of parentheses just comes out of nowhere and we automatically assume they are true in how they work.

For example the proof that $(a+b)+c = a+(b+c)$. Given some base case $(a+b)+0 = a+b = a+(b+0)$ we have for an inductive step:

$(a+b)+S(c) = S((a+b)+c) = S(a+(b+c)) = a + S(b+c) = a + (b+S(c))$

But for some reason this bothers me because we haven't really explained yet at all how the parentheses are meant to be treated in the first place. Do we need an additional axiom or definition for this? Is this mentioned anywhere? Or do we just sort of take them for granted?

• It is simply first-order logic. – Mauro ALLEGRANZA Mar 5 '18 at 16:24
• If you use Polish notation, you don't need parentheses: ${+}{+}abc={+}a{+}bc$. With infix notation, parentheses are part of the language, so you have to “prove” nothing about them. – egreg Mar 5 '18 at 16:33
• ++abSc = S++abc = S+a+bc = +aS+bc = +a+bSc … and now you see why most people don't like to use Polish notation – MJD Mar 5 '18 at 16:54
• The "underlying logic" define the syntax: $a$ is a term (a "name"), $b$ is a term; $+$ is a binary function and thus $+(a,b)$ (usually written: $(a+b)$) is a term. – Mauro ALLEGRANZA Mar 5 '18 at 19:11
• What we have to prove is not "the usage of parentheses" but the fact that $+(a,b)=+(b,a)$. In general, it is not true that $f(a,b)=f(b,a)$, for every binary function. And the same for $+(+(a,b),c)=+(a,+(b,c))$. – Mauro ALLEGRANZA Mar 5 '18 at 19:12

In formal language theory (most relevantly, context-free languages), there is the notion of an abstract syntax tree. A decent chunk of formal language theory is figuring out how to turns flat, linear strings of symbols into this more structured representation. This more structured, tree-like representation is generally what we are thinking of when think about well-formed formulas or terms. For example, when we consider doing induction over all formulas, it is a structural induction over abstract syntax trees, not strings.

For the relatively simple and regular languages often used for simple formal logics, it is relatively easy to describe the syntax with a context-free grammar and/or describe an algorithm that will take a string and parse out the abstract syntax tree if possible. For something like $S(a+(b+c))$ this would produce a tree like:

    S
|
+
/ \
a   +
/ \
b   c


Of course, if I wanted to represent this tree in linear text, i.e. I wanted to serialize it, I would need to pick some textual representation, and in this case the original expression, S(a+(b+c)), would be one possible representation. Another would be Polish notation, S+a+bc. Another would be S-expressions, (S (+ a (+ b c))). Another would be something like standard notation but eschewing infix operators, S(+(a,+(b,c))).

Ultimately, what I would strongly recommend is that you think of the abstract syntax trees as primary and the pieces of text you see in books as just serializations of these trees forced upon us by practical limitations. The need to concern ourselves with parsing at all in logic is, to a large extent, just an artifact of the medium we're using. From the perspective of abstract syntax trees, associativity looks like:

    +          +
/ \        / \
+   c  =   a   +
/ \            / \
a   b          b   c


Humans are rather good at parsing languages, so it's not generally a barrier to understanding. It is obviously unnecessary to understand context-free grammars to confidently and correctly read most formal notation. If you are interested in parsing, by all means read up on it, but parsing isn't too important to logic so I would not get hung up on it. (Formal languages and formal logic do have a decent overlap in concepts and techniques though.) From a philosophical perspective, worrying about parsing formal languages (an impression some books give) while reading sentences in a massively more complicated natural language is a touch silly.

• +1 for the nice point about the complexity of the natural language. As far as I can tell for many(most?) languages we're still figuring out how to do parsing consistently in an automated fashion. – DRF Mar 5 '18 at 20:58
• I too like thinking in terms of the AST, but a lot of logic textbooks still use some linear syntactic format for first-order sentences. Do you recommend instead using tuples (of naturals or tuples) instead of strings to capture the ASTs? – user21820 Mar 6 '18 at 5:52
• @user21820 I personally like working in constructive type theories which usually have an inductive type mechanism which can near perfectly capture ASTs. If I were to make a set-theoretic encoding of such ASTs, I'd likely use and inductively defined set built out of tuples with naturals as the tags in the discriminated unions. For an introductory logic textbook that's unlikely to perform meta-logical operations like induction over formulas, just the idea that the notation written on the page is a representation of this tree-like concept is likely enough. I may have misunderstood your question. – Derek Elkins left SE Mar 6 '18 at 6:19
• @DerekElkins: I see. I was referring to logic textbooks that go beyond the 'introductory logic' to basic proof theory, in which it is crucial to fix some encoding of the syntax into strings or naturals or something like that. I don't see a problem with using tuples in the way we probably are both envisioning, so I'm wondering whether the main reason textbooks still use serialized syntax is just that people don't write formulae using ASTs, or perhaps also that it is 'obviously' syntax 'unlike' the abstract trees. – user21820 Mar 6 '18 at 7:39
• You might be interested in my answer. – Dan Christensen Mar 8 '18 at 19:01

Short version: you're right, there is a serious issue here, and it comes down to the exact rules we use to form terms. You've phrased it in terms of trivialization ("doesn't this reduce the proof of associativity to the reflexivity of "$=$"?"), but it's a more serious problem than that, even: it ultimately will allow us to prove that every (infix) binary operation is associative, which is clearly bonkers$^*$ (see my comments below the OP). So something needs to be resolved here.

Ultimately we want to not consider expressions like "$x+y+z$" to be terms at all (which makes sense, because until we've proved that $+$ is associative there's no reason to expect "$x+y+z$" to unambiguously refer to anything).

So it's not that "$(a+b)+c=a+b+c$" is false, but rather that it's grammatically incorrect.

Unfortunately some presentations gloss over this point in a way which does in fact cause a serious problem. I think the simplest approach is to outlaw infix notation entirely (so that "$x+y$" is a term in the "metalanguage," but not actually in the formal language we use). This has the drawback of being hard to read, but fairly quickly you'll reach the point where you're comfortable using informal infix notation as shorthand for the formal expressions in question.

The syntax I present below is just one option of many:

Given a language $L$ consisting of constant symbols, function symbols (with arities), and relation symbols (with arities), we define the class of $L$-terms as follows:

• Every constant symbol in $L$ is a term. (Note that there may be none of these.)

• Every variable is a term. (Here variables exist independently of the language $L$; in other words, variables are "logical symbols" like $\forall$, $\wedge$, $($, and $=$.)

• This is the key: if $t_1, ..., t_n$ are terms and $f$ is an $n$-ary function symbol in $L$, then $f(t_1, ..., t_n)$ is a term.

• No string of symbols is a term unless it is required to be by the rules above.

Note that this syntax does not allow infix symbols: the expression "$x+y$" is grammatically incorrect, and should be written "$+(x, y)$" instead. Note also that "$+$" can only take in as many inputs as its arity: so $+(x, y, z)$ is not a term, since $+$ is $2$-ary. Now the associativity of a binary operation $*$ is expressed as $$\forall x, y, z(*(x, *(y, z))=*(*(x, y), z)),$$ and the issue you raise doesn't crop up here at all since the relevant "ambiguous terms" aren't even well-formed expressions in our syntax.

Incidentally, note that the notation I've described above is redundant: we could write "$ft_1...t_n$" and this would be perfectly unambiguous. But in my opinion this leads to a significant loss of "human readability;" why make your syntax minimal if it's harder to read? You'll pry my unnecessary commas and parentheses from my cold, dead hands!

Now in some sense this can be viewed as dodging the point: what if we do want to allow infix operations? Here again the point is that we need to approach the term-formation rules carefully. My choice would be the following rules (here "$*$" is a binary infix operator):

• If $t_1, t_2$ are terms, then $(t_1*t_2)$ is a term.

Note the addition of parentheses: this prevents (again!) the formation of an "ambiguous term" like $x*y*z$. It does have the drawback of adding "unnecessary parentheses" - e.g. "$x*y$" is not a term, but "$(x*y)$" is - but this winds up not being a problem, only an annoyance.

$^*$Actually, there is a third fix: only allow infix binary operations which are associative! So a language consists of some constant symbols, function symbols, relation symbols, and infix binary operations; and an interpretation of a language has to interpret each infix binary operation symbol as an associative binary function on the domain. This then resolves the difficulties here, since associativity is baked into the choice of notation, and it means we can allow expressions like "$a*b*c$" without causing any problems; however, it seems extremely artificial to me (and goes against mathematical practice as well: we're perfectly happy writing "$x-y$" in the real world, after all), so I wouldn't consider it as anything more than a footnote.

• The programming language Lisp is somewhat infamous for using Polish notation with parentheses: your example could potentially be written (forall (x y z) (= (* x (* y z)) (* (* x y) z))). Saves a little formal language theory, yet certainly better than being parenthesis-free. – Kyle Miller Mar 5 '18 at 21:05
• In the Oxford first-term logic course a significant amount of time is spent on conventions for which brackets may be left out and exercises about replacing the brackets to produce well-formed expressions, in order to enforce exactly this point. – dbmag9 Mar 5 '18 at 21:16
• @KyleMiller Adding parentheses makes a huge difference. Polish notation is ambiguous unless you know the arity of all the operations which you just have to have memorized. It's also not possible to scan through it without mentally simulating a stack in your head. S-expressions have neither of these problems – Derek Elkins left SE Mar 5 '18 at 21:25
• Also S-expressions permit unambiguous variadic functions, which is impossible in standard Polish notation. – MJD Mar 6 '18 at 15:41
• You might be interested in my answer. – Dan Christensen Mar 8 '18 at 19:01

If I understand well, your question is: "how to prove associativity of $+$ in Peano arithmetic?". As you have sketched, the proof is by induction on $c$, see below. You don't need to introduce any specific axiom to define how to handle parentheses, you just need the two Peano axioms that define $+$, i.e. $A_3$ and $A_4$ (see below).

Base case: \begin{align} (a+b)+0 &= a+b &\text{by } A_3 \\ &=a+(b+0) &\text{by } A_3 \end{align}

where $A_3$ is the Peano axiom: \begin{align} \forall x (x + 0 = x). \end{align}

Inductive step: \begin{align} (a+b)+S(c) &= S((a+b)+c) &\text{by } A_4 \\ &=S(a+(b+c)) &\text{by induction hypothesis} \\ &=a+S(b+c) &\text{by } A_4 \\ &=a+(b+S(c)) &\text{by } A_4 \end{align} where $A_4$ is the Peano axiom: \begin{align} \forall x \forall y (x + Sy = S(x + y)). \end{align}

Edit: I think your problems are the definition of terms in a first order language and the distinction between syntax and semantics. In the first order language for Peano arithmetic, terms are defined inductively as follows:

• every variable is a term;
• $0$ is a term;
• if $t$ and $t'$ are terms then $S(t)$, $(t + t')$ and $(t * t')$ are terms.

Note that parentheses are part of the syntax and play an important role in the syntactic formation rules for terms. By convention, the external parentheses in $(t + t')$ and $(t * t')$ are often omitted. This (syntactic) definition of terms is conceived to be unambiguous, in the sense that every term can be read in only one way. This could seem nitpicking but it is really important because it allows us to define operations and prove properties by induction on terms.

Note that according to this definition of terms, $a + (b + c)$ and $(a + b) + c$ are (syntactically) distinct terms, and $a + b + c$ is not a term because an ambiguity arises: which occurrence of $+$ has the priority? Said differently, the expression $a + b + c$ is formally meaningless, it does not denote anything.

Clearly, we have a strong intuition that $a + b + c$ is semantically meaningful, it should denote the same number as $a + (b + c)$ and $(a + b) + c$. But it is only the associativity of $+$ (the proposition that you want to prove) that allows you to consider $a + (b + c)$ and $(a + b) + c$ as terms denoting the same number, which then could sometimes synthetically represented (by abuse of language) by the expression $a + b + c$.

However, if you want to formally prove a statement in Peano arithmetic, you have to respect its syntax and in particular its formation rules for terms, so you are not allowed to use expressions like $a + b + c$. All that you are allowed to use are Peano axioms and logical inference rules. You do not need any special axiom or special definition for parentheses.

• Much like my response to the other poster this isn't what I am asking about, I am asking about the assumption, interpretation, and usage of parentheses. If we are to define $(a+b) = a+b$ then isn't proving associativity no different than "proving $a+b+c=a+b+c$?" – user537069 Mar 5 '18 at 17:08
• @user537069 The point is -- formally -- you don't (can't) define (a+b) = a+b because a+b is not formally part of the language, but you can show ((a+b)+c) is the same as (a+(b+c)). – TripeHound Mar 6 '18 at 9:23
• Would the recent downvoter care to comment on his or her action, which is inexplicable to me? – Taroccoesbrocco Mar 17 '18 at 6:37

You should think of brackets as just explaining what order to carry out operations. So if, for example, $f(x, y) = x + y$, then $(x+y)+z$ is just shorthand for $f \big( f(x,y), z \big)$. There's nothing to prove - it's just notation.

The proof is not using anything about how we can treat parentheses - each step is either a definition or an application of the inductive hypothesis.

We want to show $(a+b)+c=a+(b+c)$. This is true by definition if $c=0$ so we assume $(a+b)+c=a+(b+c)$ and we have to show that $(a+b)+S(c)=a+(b+S(c))$. The definition of $(a+b)+S(c)$ says that $$(a+b)+S(c)=S((a+b)+c).$$We're assuming that $(a+b)+c=a+(b+c)$, hence $$S((a+b)+c)=S(a+(b+c)).$$The definition of $a+S(b+c)$ says that $$S(a+(b+c))=a+S(b+c),$$and finally the definition of $b+S(c)$ says that $S(b+c)=b+S(c)$, hence $$a+S(b+c)=a+(b+S(c)).$$

• I do understand all this already (I had written the proof in my post), my question is what allows us to invoke parentheses like this in the first place. How are we defining their usage and interpretation? – user537069 Mar 5 '18 at 16:38
• Parentheses are just part of the language, allowing us to specify what objects the operators $+$ and $S$ are applied to. For example, $(a+b)+c=a+(b+c)$ is just an abbreviation for "If you start with $a+b$ and then add $c$ the result is the same as if you start with $a$ and then add $b+c$." If you wanted you could write it all out that way with no parentheses. – David C. Ullrich Mar 5 '18 at 16:49
• "If you wanted you could write it all out that way with no parentheses" But isn't removing parentheses no different than "proving $a+b+c=a+b+c$" which we already know is true by reflexivity? – user537069 Mar 5 '18 at 17:59
• Huh? IN the stupid English version I didn't remove the parentheses, I replaced them by clumsy locutions that serve the same purpose. – David C. Ullrich Mar 5 '18 at 18:57
• @user537069: you have a binary operation, so $a+b+c$ is not defined. It is usually taken to be $(a+b)+c$, and in the end it doesn't matter because one can prove (as you did) that the operation is associative. – Martin Argerami Mar 5 '18 at 23:04

Expanding on a point made by Noah, to avoid the problem in your example, we need only define addition with all bracketing made explicit as follows:

$\forall a,b\in N: [(a+b)\in N]$

$\forall a \in N: [(a+0)=a]$

$\forall a,b \in N:[(a+S(b))=S((a+b))]$

$((a+b)+0) = (a+b) = (a+(b+0))$ for some $a, b \in N$
$((a+b)+c)=(a+(b+c))$ for some $c \in N$
$((a+b)+S(c)) = S(((a+b)+c)) = S((a+(b+c))) = (a + S((b+c))) = (a + (b+S(c)))$