Эквивалентные формулы в ИП. Приведенные и нормальные формы формул в ИП. Теорема о существовании нормальной формулы в ИП.

   )(?->?)&(?->?)=>?~?; Если a~b, то и b~a (симметричность).Если a~b и b~j, то a~j. Теореме эквивалентности. Если в формуле ИП a заменить какую-нибудь ее часть эквивалентной формулой, и если полученная вследствие замены выр-е a’ также явл-ся ф-лой и содержит все своб-е пер-е a, то ?’~?: +(?->?)~((not a)vb);+not (a&b)~((not a) v (not b));+not (avb)~((not a) & (not b));+a(2раза отр)~ a;Формулы не содержащеие знак -> и такие что знак not относится только к э-ым частям наз-ся приведенными. Для каждой a существует эквивалентная ей приведенная ф-ла. Будем наз-ть приведенную ф-лу нормальной если квантор предшествует последовательности символов, образующих формулу. Для каждой a существует эквивалентная ей нормальная ф-ла.