# Definition:Formal Grammar

## Definition

<section notitle="true" name="tc"> Let $\mathcal L$ be a formal language whose alphabet is $\mathcal A$.

The **formal grammar** of $\mathcal L$ comprises of rules of formation, which determine whether collations in $\mathcal A$ belong to $\mathcal L$ or not.

Roughly speaking, there are two types of **formal grammar**, top-down grammar and bottom-up grammar.

### Top-Down Grammar

A **top-down grammar** for $\mathcal L$ is a formal grammar which allows well-formed formulas to be built from a single metasymbol.

Such a grammar can be made explicit by declaring that:

- A metasymbol may be replaced by a letter of $\mathcal A$.

- A metasymbol may be replaced by certain collations labeled with metasymbols and signs of $\mathcal A$.

From the words thus generated, those not containing any metasymbols are the well-formed formulas.

### Bottom-Up Grammar

A **bottom-up grammar** for $\mathcal L$ is a formal grammar whose rules of formation allow the user to build well-formed formulas from primitive symbols, in the following way:

- Letters are well-formed formulas.
- A collection of specified collations of well-formed formulas, possibly labeled with additional signs, are also well-formed formulas.

In certain use cases, the first clause is adjusted to allow for more complex situations, for example in the bottom-up specification of predicate logic

#### Extremal Clause

The **extremal clause** of a bottom-up grammar is the final rule which excludes all collations other than those specified in the formation rules from being well-formed formulas.

</section>

## Also known as

The **formal grammar** may also be called **syntax**; however, a convenient viewpoint is to think of the **formal grammar** as explicating the syntax for the associated formal language.

Thus the **formal grammar** is a means to obtain a syntax for $\mathcal L$, and multiple **formal grammars** may yield the same syntax.

Some sources call this merely a **grammar**, the term **formal** being taken for granted by the fact that a formal language is under discussion.

## Sources

- 1993: M. Ben-Ari:
*Mathematical Logic for Computer Science*(1st ed.) ... (previous) ... (next): $\S 1.2$: Propositional and predicate calculus