Seven formation rules for Grice's natural deduction system (p. 126 of Davidson/Hintikka)

First formation rule:

----

A formula will be

"a subscripted n-ary predicate-constant followed by n unsubscripted variables". Also: "a subscripted propositional letter".

---

Second formation rule:

phi(alpha/omega) as formula.

If phi[n] is a formula, phi(alpha_n+m/omega) is a formula

---- at this point above Grice starts the use of variables for numerical subscripts.

----

Third formation rule:

A-quantified formula.

If phi[n] is a formula, Awn+m(w/a) is a formula

---

Fourth formation rule:

E-quantified formula:

If phi[n] is a formula, Ewn+mphi(w/a) is a formula.

---

Fifth formation rule

For ~n+m

----

Sixth formation rule

for dyadic truth-functors: connectives:

For phin-m
and
phin-l

formulae for

/\n

\/n

and

)n

----

Seventh formation rule:

-- closure clause: phi is a formula only if it can be shown that phi is formula by application of 1-6.