Backus-Naur Form

Backus-Naur Form

Here is the formal syntax definition for well-formed formulas (WFF’s) of the sentential and monadic predicate calculi using Extended Backus-Naur Form (EBNF) \cite EBNF notation for context-free 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 ::= upper-case;

predicate ::= upper-case lower-case;

generalization ::= quantifier lower-case term;

negation ::= ‘¬’ term;

connective ::= ‘(’ term operator term ‘)';

description ::= ‘ι’ lower-case term;

identity ::= lower-case ‘=’ lower-case;

operator ::= and | or | if | iff

quantifier ::= universal | existential;

and ::= ‘∧';

or ::= ‘∨';

if ::= ‘→';

iff ::= ‘↔';

universal ::= ‘∀';

existential ::= ‘∃';

upper-case ::= ‘A’ … ‘Z’;

lower-case ::= ‘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

  • PQ

  • xy(FxGy)

Here are the corresponding “proper” wff’s:

  • P.

  • (PQ).

  • x(∀y(FxGy)).