II. Правила построения формул ИВ

Формулы ИВ определяются индуктивно, т.е. указываются неделимые атомные формулы, правила, по которым из заданных формул составляются новые, и постулируется, что никаких формул, кроме тех, которые являются таковыми согласно указанным правилам, нет.

Условимся обозначить в метаязыке произвольные формулы ИВ рукописными заглавными буквами из начала латинского алфавита: А,В,С,D,…

1.Каждая отдельно взятая пропозициональная буква является формулой ИВ.

2.а) Если слово А является формулой ИВ, то слово Ø А – тоже формула ИВ.

б) Если слова А и В являются формулами ИВ, то слово (АðВ), где знак ð обозначает в метаязыке произвольную двухместную связку из принятого списка основных связок ИВ, - тоже формула ИВ.

3. Слово из символов ИВ является формулой ИВ тогда, и только тогда, когда оно является таковой согласно ранее сформулированным правилам. При введении новых двухместных связок в сокращениях в метаязыке для соответствующих формул языка-объекта, сокращения записывают в виде, согласующемся с указанными правилами построения формул.

В метаязыке допускают сокращение числа скобок, используемых при записи формул; так, обычно опускают внешние скобки и некоторые другие, на основании соглашения о приоритете логических связок, определяя его местом связок в последовательности

Ø,Ú,Þ,Û:

из двух данных связок в записи с сокращенным числом скобок первой действует связка расположенная ближе к началу списка. При восстановлении скобок, для данного знака ищутся ближайшие подслова являющиеся формулами и образующие вместе со знаком подслово, являющееся формулой с опущенными внешними скобками.

Правила построения формул ИВ сформулированы так, что можно указать алгоритм, позволяющий по каждому знакосочетанию из символов ИВ выяснить, является оно формулой ИВ или нет.