В настоящей книге определено несколько языков, включая языки пропозициональной логики (с. 1), логики первого порядка (с. 1) и подмножество английского языка (с. 1). Формальный язык определяется как множество строк, в котором каждая строка представляет собой последовательность символов. Все языки, которые были необходимы нам в этой книге, состоят из бесконечного множества строк, поэтому нужен краткий способ, позволяющий охарактеризовать это множество. Для этого служит грамматика. Авторы приняли в качестве способа оформления грамматик формальную систему, называемую формой Бэкуса—Наура (Backus—Naur form — BNF). Грамматика BNF состоит из четырех компонентов, перечисленных ниже.

•    Множество терминальных символов. Это — символы или слова, из которых состоят строки языка. В качестве таких символов могут использоваться буквы (А, В, С, ...) или слова (a, aardvark, abacus, ...).

•    Множество нетерминальных символов, которые обозначают компоненты предложений языка. Например, нетерминальный символ NounPhrase (именное словосочетание) в английском языке обозначает бесконечное множество строк, которое включает "you" и "the big slobbery dog".

•    Начальный символ, который представляет собой нетерминальный символ, обозначающий законченные строки языка. В описанной выше грамматике английского языка таковым является символ Sentence; в грамматике арифметических выражений может быть задан символ Ехрг.

• Множество правил подстановки в форме, где LHS — нетерминальный символ; RHS— последовательность, в которую входят от нуля и больше символов (терминальных или нетерминальных).

Правило подстановки в приведенной ниже форме означает, что при наличии двух строк, обозначенных как NounPhrase (именное словосочетание) и VerbPhrase (глагольное словосочетание), их можно соединить друг с другом и обозначить результат как Sentence:

Несколько правил с одинаковой левой частью могут быть заданы как одно правило с той же левой частью и со всеми правыми частями этих правил, разделенными символом |. Ниже приведена грамматика BNF для простых арифметических выражений.

Более подробные сведения о языках и грамматиках приведены в главе 22. Следует отметить, что в других книгах в системе обозначений BNF могут использоваться немного другие правила, например, нетерминальные символы обозначаются как (Digi t) вместо Digi t, терминальные символы — ' word', а не word, а в правилах используются символ : : = вместо.