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?

Solution 1:

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.

Solution 2:

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.

Solution 3:

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.