BackusNaur Form
Here is the formal syntax definition for wellformed formulas (WFF’s) of the sentential and monadic predicate calculi using Extended BackusNaur Form (EBNF) \cite EBNF notation for contextfree grammars. In each production rule, symbols enclosed in apostrophes are literal strings and vertical bars separate alternative sequences. Ellipses are used to denote sets of all possible alphabetic characters in a given case. Parentheses are used for grouping sequences.
EBNF
wff ::= term ‘.';
term ::= sentence  predicate  generalization  negation  connective  description  identity;
sentence ::= uppercase;
predicate ::= uppercase lowercase;
generalization ::= quantifier lowercase term;
negation ::= ‘¬’ term;
connective ::= ‘(’ term operator term ‘)';
description ::= ‘ι’ lowercase term;
identity ::= lowercase ‘=’ lowercase;
operator ::= and  or  if  iff
quantifier ::= universal  existential;
and ::= ‘∧';
or ::= ‘∨';
if ::= ‘→';
iff ::= ‘↔';
universal ::= ‘∀';
existential ::= ‘∃';
uppercase ::= ‘A’ … ‘Z’;
lowercase ::= ‘a’ … ‘z’;
The preceding defines the “official” syntax that is amenable, for example, to automatic parsing as by a computer algorithm. The examples throughout this document use a more relaxed syntax, of the sort that human beings are likely to write on whiteboards and the like. For example, the following are perfectly understandable by human readers but do not conform to the preceding production rules due to missing parentheses and periods:

P

P ∨ Q

∀xy(Fx → Gy)
Here are the corresponding “proper” wff’s:

P.

(P ∨ Q).

∀x(∀y(Fx → Gy)).