Спирина, М.С. Дискретная математика

1. a |— a v b ,т.е. к заключению можно добавить другое высказы­ вание с помощью дизъюнкции. 2. а, b |— а л Ь. 3. а л Ь\—а. 4. а с, b -> с |— (a v b) -» с — распределительный закон относительно дизъюнкции посылок. 5. а -> />, а -» 6 1— а. 6. (—a v а — закон исключенного третьего. Для доказательства других тавтологий нужно использовать ана­ литические правила выводов через логические следствия. Напри­ мер, достаточно часто применяется теорема дедукции Ф, А |— В о <=> Ф (— А -» В, где Ф — список формул, А и В — отдельные формулы. Известный из школьного курса геометрии метод дока­ зательства от противного можно сформулировать как правило ис­ числения высказываний (Г, А |— В и Г, А |— В) => (Г -» А) — правило введения отрицания. Эти теоремы могут быть доказаны методом математической индукции (см. подразд. 5.7). Построенная теория Т не является единственно возможной аксиоматизацией исчисления высказываний. Существуют и дру­ гие аксиоматизации исчисления высказываний (табл. 5.3). Т а б л и ц а 5.3 Аксиоматизации исчисления высказываний Гильберт, Аккерман (1938) Клини (1952) Россер (1953) А Основные: v, дополнительные: d e f — (А -> В = A v В) —1, А , V , — » Основные: л; дополнительные: de f - (4 -» В = А а В) Р A v А -> А А — > A v В A v В —>B v A (В-> C ) ^ > ( A v В-> - >А v С) А - > ( В - * А ) (А -> (В С) ) -» ( (А -> - з В) -> (А -> С)) А а В — » А А л В — > В А — > (В — > A v В) А -> ( A v В) B - > ( A v B ) ( Л - > С ) - > ( (В -> С) -> -> ((A v В) С )) ( / ) - > # ) - > ({А -> В) -> - * А) = d e f — А = ч(А) -> А А —> А л А А л В -> А (А -> В) -> ( В а А С) —>С А А R modus ponens modus ponens modus ponens 223