- •Элементы математической логики Лекция 6. Исчисление высказываний (ив)
- •6.1 Аксиомы
- •6.2. Формальное доказательство и формальный вывод
- •А1, а2,...., Аn ├ в.
- •6.3 Свойства отношения выводимости
- •Некоторые вспомогательные правила вывода
- •6.5 Полнота, непротиворечивость и независимость аксиом исчисления высказываний
- •6.6 Использование правил введения и удаления и мт1
- •Другие аксиоматизации исчисления высказываний
6.6 Использование правил введения и удаления и мт1
при установлении доказательств и выводов в теории L (на «5» баллов)
Правила введения и удаления логических операций и МТ1 позволяют упрощать построение доказательств и выводов по сравнению с непосредственным построением этих доказательств и выводов.
Пример. Докажем один из законов поглощения (формула (37) из 50-ти общезначимых формул)
|– ААВА
и связанные с этим законом правила вывода:
А |– ААВ
ААВ |– А.
Схема хода решения:
Доказательство в таблице.
1 |
А |– А |
МТ1а |
2 |
АВ |– А |
УК1 |
3 |
ААВ |– А |
УД(1,2) |
4 |
|– ААВА |
ВИ(3) |
5 |
А |– ААВ |
ВД1 |
6 |
|– АААВ |
ВИ(5) |
7 |
|– ААВА |
ВЭ(4,6) |
Другие аксиоматизации исчисления высказываний
Теория L не является единственной аксиоматической теорией исчисления высказываний. Известны многие другие аксиоматические теории, предложенные различными авторами:
а) теория Гильберта, б) Россера, в) Клини и другие (смотри Новиков Ф.А. Дискретная математика для программистов, стр.118). Они отличаются друг от друга, в основном, системой аксиом.
Теория L1. Основные связки: V, .
Метаопределение: А В= А V В.
Схемы аксиом:
А1: А V А А
А2: А А V В
А3: А V В В V А
А4: (В С) (А V В А V С)
Правило вывода: МР.
Теория L2. Основные связки: Λ, .
Метаопределение: А В = (А Λ В).
Схемы аксиом:
А1: А (А Λ А)
А2: (А Λ В) А
А3: (А В) ( (В Λ С) (С Λ А))
Правило вывода: МР.
Теория L3 Основные связки: Λ, ., V
Схемы аксиом (аксиомы разбиты на четыре группы):
1.1. А(ВА)
1.2. (А (ВС)) ((АВ) (АС))
2.1. АВА
2.2. АВВ
2.3. (АВ) ((АС) (АВС))
3.1. ААВ
3.2. ВАВ
3.3. (АС) ((ВС) (АВС))
4.1. (АВ) ( ВА)
4.2. АА
4.3. АА
Правило вывода: МР.