Питання для самоконтролю
1. Що вивчає математична логіка? Вкажіть основні розділи математичної логіки. Що таке числення?
2. Що вивчає логіка висловлювань? Чим характеризується класична логіка висловлювань? Вкажіть різновиди класичної логіки висловлювань. Чим вони відрізняються один від одного?
3. Які основні задачі розв’язуються в логіці висловлювань? Чим відрізняються змістовий і формальний підходи при доведенні тотожної істинності висловлювань?
4. Що називають висловлюванням у логіці висловлювань? Яке висловлювання називають простим? Яке висловлювання називають складним? Які зв’я́зки використовують при побудові складних висловлювань із простих? Наведіть приклади простих і складних висловлювань.
5. Що є логічними змінними і які логічні операції використовують у логіці висловлювань? Чи повинна бути система логічних операцій, які використовують у логіці висловлювань, повною (надлишково повною)? Що таке формула? Вкажіть пріоритети логічних операцій логіки висловлювань. За допомогою якої операції можна подати поняття достатньої й необхідної умов? Наведіть приклади висловлювань і відповідних їм формул.
6. Дайте визначення логіки висловлювань як алгебри. Як можна встановити зв’язок між логікою висловлювань і алгеброю логіки? Чи можна в логіці висловлювань використовувати результати алгебри логіки?
7. Для чого використовують систему обчислень в логіці висловлювань? Який вигляд має таблиця істинності в алгебрі висловлювань? Яку формулу називають тавтологією? Наведіть приклади тавтологій. Як, використовуючи систему обчислень, можна довести, що формула є тавтологією?
8. Для чого використовують еквівалентні перетворення формул в алгебрі висловлювань? Які формули називають еквівалентними? Яку формулу називають еквівалентністю? Які закони еквівалентності використовують при перетвореннях формул? Поясніть суть закону виключення третього. Сформулюйте правило підстановки і поясніть його суть. Сформулюйте правило транзитивності і подайте його формулою.
9. Для чого використовують системи формального виведення в чи́сленні висловлювань? Що таке аксіоми числення висловлювань? Наведіть приклади аксіом. Наведіть приклади правил виведення і поясніть їхній зміст. Сформулюйте правило висновку (modus popens), поясніть його суть. Чи в усіх різновидах класичного числення висловлювань використовують ті самі правила виведення? Яку формулу називають безпосередньо вивідною? Що таке доведення формули? Чи можна довести формулу із множини умовно істинних формул? Яку формулу називають довідною? Що таке теорема числення висловлювань? Яку систему аксіом називають несуперечною? Яке числення висловлювань називають несуперечним, а яке суперечним? Як довести несуперечність числення висловлювань? Яку систему аксіом називають повною в широкому розумінні? Сформулюйте теорему про повноту. Що таке повнота у вузькому розумінні? Яку систему аксіом називають незалежною? Сформулюйте теорему дедукції і наслідки з неї. Вкажіть загальні схеми доведення теорем у чи́сленні висловлювань.
10. Схарактеризуйте систему природного виведення. Чи використовують аксіоми в системі природного виведення? Що записують в схемі формального доведення теореми? Вкажіть правила виведення системи природного виведення і поясніть їхню суть. Наведіть приклади застосування правил виведення. Сформулюйте теорему дедукції системи природного виведення. У чому полягає метод доведення теорем “від протилежного”? Сформулюйте теорему про пряму підстановку. Як можна встановити зв’язок між системою обчислень, еквівалентними перетвореннями і системою природного виведення?
11. Наведіть приклади аксіоматичних систем в чи́сленні висловлювань. Чим вони відрізняються одна від одної? У чому полягає еквівалентність деяких із них? Чи правильне твердження: формула, яка є аксіомою в одному різновиді класичного числення висловлювань, може бути доведена як теорема в іншому різновиді?
1 Числення (дедуктивна система) — це система, яка задає множину, зазначаючи первісні елементи (аксіоми) й правила виведення, кожне з яких описує спосіб побудови нових елементів із первісних і зі збудованих раніше.
2 Герхард Карл Еріх Генцен (Gerhard Karl Erich Gentzen; 1909–1945) — німецький математик і логік; у 1934 році розробив систему натурального числення.
3
У
деяких різновидах логіки висловлювань
може бути більше операцій, ніж ми
розглядаємо. Наприклад, ще використовуються
“виключне або” (
),
штрих Шеффера (
),
стрілка Пірса (
).
4 У більшості аксіоматизацій правило підстановки не включають в перелік правил виведення, а вважають його правилом побудови аксіом.
5 На основі системи природного виведення побудовано системи комп’ютерної верифікації програм.
6 Давид Гільберт (David Hilbert; 1862–1943) — німецький математик; зробив значний внесок у розвиток багатьох галузей математики.
7 Зауважимо, що в доведенні теореми дедукції (наприклад, в [8, 10]) використовуються лише схеми аксіом А1 і А2.
8 Петро Сергійович Новиков (Пётр Сергеевич Новиков; 1901–1975) — російський радянський математик.
9 Стівен Коул Кліні (Клейні, Stephen Cole Kleene;1909–1994) — американський логік і математик, праці якого заклали основи теоретичної інформатики.
10 Джон Барклі Россер старший (John Barkley Rosser Sr.; 1907–1989) — американський логік.
11 Вільгельм Фрідріх Аккерман (Wilhelm Friedrich Ackermann; 1896–1962) — німецький математик і логік.
12 Кар’ю Артур Мередіт (Carew Arthur Meredith; 1904–1976) — ірландський логік.
13 Жан П’єр Джордж Нікод (Ніко; Jean George Pierre Nicod; 1893–1924) — французький філософ і логік; дану аксіоматизацію опублікував у 1917 році.