Главная страница Случайная страница
Разделы сайта
АвтомобилиАстрономияБиологияГеографияДом и садДругие языкиДругоеИнформатикаИсторияКультураЛитератураЛогикаМатематикаМедицинаМеталлургияМеханикаОбразованиеОхрана трудаПедагогикаПолитикаПравоПсихологияРелигияРиторикаСоциологияСпортСтроительствоТехнологияТуризмФизикаФилософияФинансыХимияЧерчениеЭкологияЭкономикаЭлектроника
Если используется только правило (ВИ), то доказательство будет прямым, а если используется (ВО),, то доказательство будет косвенным.
|
|
Доказательство в S3 начинают с допущений, а затем по правилам вывода получают из них соответствующие следствия, после чего с помощью правил (ВИ) и (ВО) элиминируют (удаляют) допущения. Так что в S3 исходным является понятие вывода из допущений, а понятие безусловного вывода (доказательства) – производным.
Определение понятия выводимости из допущений. «Формула В выводима из допущений G, А, символически G, А |- В, если и только если:
1) существует правило вывода, в котором G и А являются посылками, а В заключением этого правила, либо
2) существует некоторая последовательность применений правил вывода R1, …Rn, в которой посылками каждого применяемого правила являются либо формулы из G, А, либо следствия предыдущих (в данной последовательности) применений правил, причем следствием последнего применения правила является формула В. При этом разрешается использовать свойства знака |- ».
Гипотезу называют устраненной в ходе дедукции, если в процессе дедукции к этой гипотезе (или к ее следствию) применялось правило (ВИ) или (ВО).
Доказательством формулы А называется дедукция из такого конечного множества гипотез, в ходе которой каждая гипотеза устраняется.
Осуществим доказательство некоторых теоерем пропозиционального исчисления с помощью натурального вывода.
Чтобы построить доказательство теоермы в S3, необходимо выполнить следующие действия:
Выписать все возможные допущения, исходя из структуры данной формулы;
2) применить к выписанным допущениям соответствующие правила вывода из 14 правил, входящих в дедуктивный аппарат S3;
Применить одно из правил (ВИ) или (ВО) для элиминации допущений.
Пользуясь этими установками, перейдем к доказательству конкретных теорем.
Теорема 1. (А É В) É ((В É С) É (А É С))
Доказательство.
1. А É В - допущение 1
2. В É С - допущение 2
3. A - допущение 3
4. В - УІ к 1, 3
5. С - УІ к 2, 4
6. А É С - ВИ к 3, 5
7. (B É C) É (A É С) - ВИ к 2, 6
8. (А É В) É ((В É С) É (А É С)) - ВИ к 1, 7
Теорема 2. (А É В) É ((С É А) É (С É В))
Доказательство.
1. А É В - допущение 1
2. С É А - допущение 2
3. C - допущение 3
4. А - УІ к 2, 3
5. В - УI к 1, 4
6. С É В - ВИ к 3, 5
7. (C É A) É (С É B) - ВИ к 2, 6
8. (А É В) É ((С É А) É (С É В)) - ВИ к 1, 7
Теорема 3. (А É В) É ((С & А) É (С & В))
Доказательство.
1. А É В - допущение 1
2. C & A - допущение 2
3. С - УК к 2
4. А - УК к 2
5. В - УИ к 1, 4
6. С & В - ВК к 3, 5
7. (C & A) É (С & B) - ВИ к 2, 6
8. (А É В) É ((С & А) É (С & В)) - ВИ к 1, 7
Теорема 4. (А É В) É ((А & С) É (В & С))
|
|