§ 3. Упрощения в записях формул

Введем некоторые соглашения о более экономном употреблении скобок в записях формул. Эти соглашения облегчат нам чтение сложных выражений.

Во-первых, будем опускать в формуле внешнюю пару скобок. (В случае одной переменной этой внешней пары скобок нет по определению.)

Во-вторых, если формула содержит вхождения только одной бинарной связки &, ∨, ⇒ или ≡, то для каждого вхождения этой связки опускаются внешние скобки у той из двух формул (соединяемых этим вхождением) которая стоит слева.

Пример. x∨y∨z∨x пишется вместо (((x∨y)∨z)∨x), а y⇒y⇒x⇒(z⇒x) пишется вместо (((y⇒y)⇒x)⇒(z⇒x)).

В-третьих, договоримся считать связки упорядоченными следующим образом: ¬ , &, ∨, ⇒, ≡ и будем опускать во всякой формуле все те пары скобок, без которых возможно восстановление этой формы на основе следующего правила.

Каждое вхождение знака ¬ относится к наименьшей формуле, следующей за ним; после расстановки всех скобок, относящихся ко всем вхождениям знака ¬, каждое вхождение знака & связывает наименьшие формулы, окружающие это вхождение; затем (т.е. после расстановки всех скобок, относящихся ко всем вхождениям знаков ¬ и &) каждое вхождение знака ∨ связывает наименьшие формулы, окружающие это вхождение, и аналогично для ⇒ и ≡. При применении этого правила к одной и той же связке продвигаемся слева направо.

Пример. В упрощенной записи формулы x≡¬x&y⇒z∨¬t скобки восстанавливаются следующими шагами:

x≡(¬ x)&y⇒z∨(¬ t),
x≡((¬ x)&y)⇒z∨(¬ t),
x≡((¬ x)&y)⇒(z∨(¬ t)),
x≡(((¬ x)&y)⇒(z∨(¬ t))),
(x≡(((¬ x)&y)⇒(z∨(¬ t)))).

Однако не всякая формула может быть записана без скобок. Например, нельзя опустить оставшиеся скобки в следующих случаях: x&(y⇒z), x⇒(y⇒z), ¬ (x∨y).

Для операций +, | и ↓ не указаны порядки их выполнения, поэтому последовательность их выполнения устанавливается с помощью скобок.