Formal grammar of first-order Peano arithmetic

Question

I would like to write out the grammar of first-order Peano arithmetic in Backus-Naur Form. The alphabet I am using is $\{0,x,^*,(,),S,+,\times,<,=,\exists,\forall,\neg,\lor,\land\}$, where $x$ is a variable, $^*$ is a symbol used to index new variables, and $S$ is the successor function. Here is what I have so far.

<formula> ::= ( <formula> )
        | ¬ <formula> 
        | ( <term> <relation> <term> )
        | <quantifier> <variable> ( <formula> )
        | ( <formula> <connective> <formula> )

<term> ::= ( <term> )
        | <constant>
        | <variable>
        | S( <term> )
        | ( <term> <operation> <term> )

<constant> ::= 0
        | S( <constant> )
        | ( <constant> <operation> <constant> )

<variable> ::= x
        | <variable> *

<quantifier> ::= ∃ | ∀

<relation> ::= < | =

<operation> ::= + | ×

<connective> ::= ∨ | ∧

Is this the standard grammar for first-order PA?

Answer 1

I would get rid of the $(<term>)$ as an option for $<term>$ ... just use parentheses where needed elsewhere. Same for $(<formula>)$

Second, constant should just be $0$ .. as soon as you apply operations, it's a term.

Actually, most textbooks use 'atomic term' for either a constant or a variable, and 'complex term' for when you start using operations/functions.

So explicitly that would be:

$<term> ::= <atomicterm> | <complexterm>$

$<atomicterm> ::= <constant> | <variable>$

$<complexterm>::= S( <term> ) | ( <term> <operation> <term> )$

$<constant> ::= 0$

or implicitly:

$<term> ::= <constant> | <variable> | S( <term> ) | ( <term> <operation> <term> )$

$<constant> ::= 0$