ИВ - это новая логическая система, которая адекватна алгебре высказываний, но здесь мы не будем рассматривать закон исключения третьего. Сами законы нас будут интересовать только в смысле выводимости. Т.е. мы будем себе ставить задачу обосновать тот или иной закон, показав, что пользование им не приведет к противоречию.
СИМВОЛЫ ИВ состоят из знаков трех категорий: 1. Большие латинские буквы A, B, C, ..., Y, Z. Эти символы мы будем называть переменными высказываниями. 2. Логические связки: & - знак конъюнкции; \/ - дизъюнкции; -> импликации и (not ) - знак отрицания. 3. Скобки: ( ).
В ИВ определение ФОРМУЛЫ представляет собой следующую рекурсию: 1) Переменное высказывание есть формула. 2) Если a и b - формулы, то слова (a&b), (a\/b), (a->b) и (not b) также формулы. Переменные высказывания называются также ЭЛЕМЕНТАРНЫМИ ФОРМУЛАМИ.
Определение ЧАСТИ ФОРМУЛ представляет собой следующую рекурсию: 1. Частью каждой элементарной формулы является только она сама. 2. Если определены все части формул a и b, то частями формулы (a&b) будут все части формул a и b и сама формула. Аналогично определяются части формул (a\/b), (a->b), (not a).