Чи́слення висло́влень (логіка висловлень, пропозиційна логіка, англ. propositional calculus) — формальна система в математичній логіці, в якій формули, що відповідають висловленням, можуть утворюватись шляхом з'єднання простих висловлень із допомогою логічних операцій, та система правил виводу, які дозволяють визначати певні формули як «теореми» формальної системи.
Формальне визначення
Численням висловлень є формальна система , де:
- Множина є скінченною множиною символів висловлень (чи елементарних висловлювань, пропозиційних змінних, атомарних формул). Для зображення атомарних формул нижче використовуються малі латинські літери. За потреби можна використовувати і зліченну множину символів.
- Множина — скінченна множина логічних сполучників (логічних операторів). Дану множину можна розбити на підмножини:
- У цьому розбитті є множина операторів арності (також позначено ).
- Найчастіше використовуються оператори:
- Множина є скінченною множиною правил виводу, що дозволяють одержувати одні формули з інших.
- Множина є скінченною множиною, елементи якої називаються аксіомами. В окремих прикладах дана множина може бути пустою.
Мовою числення висловлень є множина формул, що визначаються рекурсивно за допомогою наступних правил:
- всі елементи множини є формулами;
- якщо є формулами та , тоді теж є формулою.
- інших формул, ніж побудовані за правилами 1 і 2 немає.
Виведення формул і теорем
Нехай деяка множина формул , а — деяка задана формула, то кажуть, що формула виводиться з множини формул (позначається ), якщо існує така (скінченна послідовність) формул де для кожної формули :
- є аксіомою, або
- належить множині або
- виводиться з попередніх формул послідовності за допомогою котрогось із правил виводу.
Якщо при цьому множина — пуста (формула виводиться лише за допомогою аксіом і правил виводу), то формула називається теоремою (для цього використовується позначення ).
Приклади аксіоматики
Приклад 1
- Алфавіт (елементи множини ) числення висловлень складається з елементарних висловлень (пропозиційних змінних): (можливо з індексами), логічними операціями є .
- Поняття формули визначається аналогічно алгебрі висловлень.
- всі пропозиційні змінні та елементарні висловлення є формулами;
- якщо A і B — формули, то вирази (слова) також є формулами;
- інших формул, ніж побудовані за правилами 2.1 і 2.2 немає.
Аксіоми
В численні висловлень визначають такі схеми аксіом:
Єдиним правилом виводу є:
У даних схемах аксіом та правила виводу символи можна заміщувати усіма допустимими формулами, після чого і отримуються конкретні аксіоми.
Приклад виведення теореми
Користуючись поданими аксіомами і правилом виведення покажемо, що () є теоремою в даній формальній системі для будь-якої формули .
Приклад виводу | ||
---|---|---|
Номер | Формула | Спосіб одержання |
1 | Аксіома 2 з заміною на відповідно | |
2 | аксіома 1(заміна на ) | |
3 | 1, 2 і modus ponens. | |
4 | аксіома 1(заміна на відповідно) | |
5 | 3, 4 і modus ponens. |
Приклад 2 (аксіоми Лукашевича)
- Алфавіт (елементи множини ) числення висловлень складається з елементарних висловлень (пропозиційних змінних): (можливо з індексами), логічними операціями є .
- Поняття формули визначається аналогічно алгебрі висловлень.
- всі пропозиційні змінні та елементарні висловлення є формулами;
- якщо A і B — формули, то вирази (слова) також є формулами;
- інших формул, ніж побудовані за правилами 2.1 і 2.2 немає.
Наступну просту систему аксіом запропонував польський логік Ян Лукашевич:
Єдиним правилом виводу є:
(Modus ponens).
Як і у попередньому прикладі дані вирази є схемами аксіом.
Приклад виведення теореми
Користуючись аксіомами Лукасевича і правилом виведення покажемо, що () є теоремою в даній формальній системі для будь-якої формули .
Приклад виводу | ||
---|---|---|
Номер | Формула | Спосіб одержання |
1 | Аксіома 2 з заміною на відповідно | |
2 | аксіома 1(заміна на відповідно) | |
3 | 1, 2 і modus ponens. | |
4 | аксіома 1(заміна на ) | |
5 | 3, 4 і modus ponens. |
Семантика
У поданих вище формальних системах і оператори можуть фактично мати довільну природу. Для логіки важливе значення має інтерпретація цих символів.
Інтерпретація визначається заданням істинності тобто наданням кожній атомарній формулі одного із значень 1(«Істина») чи 0(«Хиба»), а також визначенням операторів як булевих функцій від своїх операндів.
Найчастіше вживані оператори задаються за допомогою таблиць істинності:
|
|
|
|
|
Зважаючи на спосіб побудови формул, кожна формула при деякому заданню істинності отримує певне значення 0 або 1. Значення найпростіших формул для різних завдань істинності можна обчислювати за допомогою таблиць істинності. Наприклад:
Якщо для деякого задання істинності формула набуває значення 1, то кажуть, що формула задовольняє задання . Формула, що задовольняє усі можливі задання істинності (як формула з прикладу) називається тавтологією. Якщо — деяка множина формул то кажуть, що дана множина задовольняє задання істинності, якщо це задання задовольняє кожна формула цієї множини. Якщо для деякої формули з того, що множина задовольняє заданню істинності випливає що задовольняє цьому заданню то формула називається логічним наслідком множини (позначається ). У випадку якщо множина є пустою, формула є тавтологією.
Основні проблеми числення висловлень
Для обґрунтування будь-якої аксіоматичної теорії необхідно розглянути наступні 4 проблеми:
- Несуперечливості
- Повноти
- Незалежності
- Розв'язності
Проблема несуперечливості
Означення: Нехай задано деяку формальну аксіоматичну теорію. Говорять, що побудована модель цієї теорії, якщо всім символам алфавіту надано деякого конкретного змісту, який описує певну неформальну теорію і відношення між елементами цієї теорії.
Формальна аксіоматична теорія називається категоричною, якщо будь-які її 2 моделі ізоморфні між собою, тобто між ними можна встановити взаємно-однозначну відповідність.
Формальна аксіоматична теорія називається несуперечливою відносно своєї моделі, якщо будь-яка теорема, що доводиться в формальній теорії є істинним твердженням для моделі.
Формальна аксіоматична теорія числення висловлень називається внутрішньо несуперечливою, якщо в цій теорії не можна довести деяку теорему (формулу) разом з її запереченням.
Формальна аксіоматична теорія називається синтаксично несуперечливою якщо в ній існує хоча б якась формула, яка не є теоремою.
Теорема: Формальна аксіоматична теорія числення висловлень є несуперечливою відносно своєї моделі алгебри висловлень.
Наслідок:
- Числення висловлень – внутрішньо-несуперечлива теорія.
- Числення висловлень – синтаксично-несуперечлива теорія.
Теорема: Формальна аксіоматична теорія числення висловлень є категоричною.
Проблема повноти
Формальна аксіоматична теорія числення висловлень називається повною у вузькому розумінні, якщо приєднання до системи аксіом цієї теорії хоча б однієї формули, яка не є теоремою веде до того, що теорія стає внутрішньо-суперечливою.
Формальна аксіоматична теорія числення висловлень є повною у широкому розумінні або повною відносно своєї моделі, якщо будь-яка формула істинна в моделі є теоремою в цій теорії, або якщо будь-яку тотожно істинну формулу можна довести.
Наслідок: Числення висловлень є повним. Справедливість цього твердження безпосередньо випливає з теореми. У математичній логіці існує й інше поняття повноти системи аксіом, що ґрунтується на неможливості доповнення системи аксіом будь-якою формулою, яку не можна вивести з даних аксіом.
Теорема: Формальна аксіоматична теорія числення висловлень є повною відносно своєї моделі алгебри висловлень.
Теорема: Числення висловлень – це формальна аксіоматична теорія, повна у вузькому розумінні.
Проблема незалежності
Означення: Нехай задано деяку формальну аксіоматичну теорію, говорять, що деяка аксіома цієї теорії є незалежною, якщо її не можна довести методами самої теорії, як теорему. Система аксіом формальної аксіоматичної теорії називається незалежною системою аксіом, якщо всі аксіоми є незалежними.
Теорема: Система аксіом числення висловлень є незалежною.
Доведення: Для доведення незалежності деякої аксіоми числення висловлень використовують наступний підхід: будують таку модель формальної аксіоматичної теорії, в якій справджуються всі аксіоми окрім даної. Якщо доводиться, що така модель ізоморфна стандартній моделі формальної аксіоматичної теорії, то робиться висновок, що аксіома не є незалежною, якщо ж такого ізоморфізму немає – незалежна.
Приклад: Як модель формальної аксіоматичної теорії візьмемо
a∧b ≡ b, все інше не змінюємо, покажемо, що ІІ2 і ІІ3 справджуються, а ІІ1 ні.
ІІ2 a∧b → b
|- b → b
ІІ3 (a → b) → (( a→ c ) → ( a → b∧c ))
|- ( a→ b ) → (( a → c ) → ( a → c))
ІІ1 a∧b → a
b → a
Доведено
Наслідок: Система аксіом числення висловлень є незалежною.
Проблема розв’язності
Полягає в тому щоб довести існування алгоритму, який для будь-якої формули числення висловлень визначає чи можна її довести чи ні.
Теорема: Проблема розв`язності числення висловлень є розв'язною.
Теорема 1: Будь-яка тотожно істинна формула алгебри висловлень є теоремою числення висловлень.
Доведення: Нехай A - довільна формула числення числення висловлень. Побудуємо для неї таблицю істинності і розглянемо її останній стовпчик. Якщо він містить лише одиниці, то A - тотожно істинна формула і за теоремою 1 є теоремою числення висловлень. В іншому випадку (останній стовпчик таблиці істинності містить хоча б один нуль), A - не тавтологія і значить, A не є теоремою.
Див. також
Джерела
- Гильберт Д., Аккерман В. Основы теоретической логики. М., 1947
- Клини С. К. Введение в метаматематику. М., 1957
- Мендельсон Э. Введение в математическую логику. М., 1976
- Enderton, H. B., A Mathematical Introduction to Logic. Harcourt/Academic Press 2002.
- A. G. Hamilton Logic for Mathematicians, Cambridge University Press, Cambridge UK 1978 .
Література
- Прийма С.М. Математична логіка і теорія алгоритмів: Навчальний посібник – Мелітополь: ТОВ „Видавничий будинок ММД”, 2008. - 134 с.
- Гасяк О.С. Формальна логіка : короткий словник-довідник. – Чернівці : Чернівецький нац. ун-т, 2014. – 200 с.
- Логічні числення // Філософський енциклопедичний словник / В. І. Шинкарук (гол. редкол.) та ін. — Київ : Інститут філософії імені Григорія Сковороди НАН України : Абрис, 2002. — 742 с. — 1000 екз. — ББК (87я2). — .
- Числення висловлювань // ФЕС, с.714
- Матвієнко М.П., Шаповалов С.П. Математична логіка та теорія алгоритмів. Навчальний посібник. – К.: Видавництво Ліра-К, 2015. – 212 с.
Посилання
- УРЕ
Вікіпедія, Українська, Україна, книга, книги, бібліотека, стаття, читати, завантажити, безкоштовно, безкоштовно завантажити, mp3, відео, mp4, 3gp, jpg, jpeg, gif, png, малюнок, музика, пісня, фільм, книга, гра, ігри, мобільний, телефон, android, ios, apple, мобільний телефон, samsung, iphone, xiomi, xiaomi, redmi, honor, oppo, nokia, sonya, mi, ПК, web, Інтернет
Chi slennya vislo vlen logika vislovlen propozicijna logika angl propositional calculus formalna sistema v matematichnij logici v yakij formuli sho vidpovidayut vislovlennyam mozhut utvoryuvatis shlyahom z yednannya prostih vislovlen iz dopomogoyu logichnih operacij ta sistema pravil vivodu yaki dozvolyayut viznachati pevni formuli yak teoremi formalnoyi sistemi Formalne viznachennyaChislennyam vislovlen ye formalna sistema L L A W Z I displaystyle mathcal L mathcal L left mathrm A Omega mathrm Z mathrm I right de Mnozhina A displaystyle mathrm A ye skinchennoyu mnozhinoyu simvoliv vislovlen chi elementarnih vislovlyuvan propozicijnih zminnih atomarnih formul Dlya zobrazhennya atomarnih formul nizhche vikoristovuyutsya mali latinski literi Za potrebi mozhna vikoristovuvati i zlichennu mnozhinu simvoliv Mnozhina W displaystyle Omega skinchenna mnozhina logichnih spoluchnikiv logichnih operatoriv Danu mnozhinu mozhna rozbiti na pidmnozhini W W0 W1 Wj Wm displaystyle Omega Omega 0 cup Omega 1 cup ldots cup Omega j cup ldots cup Omega m dd dd U comu rozbitti Wj displaystyle Omega j ye mnozhina operatoriv arnosti j displaystyle j takozh poznacheno W0 0 1 displaystyle Omega 0 0 1 Najchastishe vikoristovuyutsya operatori W1 displaystyle Omega 1 lnot dd dd W2 displaystyle Omega 2 subseteq land lor rightarrow leftrightarrow dd dd Mnozhina Z displaystyle mathrm Z ye skinchennoyu mnozhinoyu pravil vivodu sho dozvolyayut oderzhuvati odni formuli z inshih Mnozhina I displaystyle mathrm I ye skinchennoyu mnozhinoyu elementi yakoyi nazivayutsya aksiomami V okremih prikladah dana mnozhina mozhe buti pustoyu Movoyu chislennya vislovlen ye mnozhina formul sho viznachayutsya rekursivno za dopomogoyu nastupnih pravil vsi elementi mnozhini A displaystyle mathrm A ye formulami yaksho p1 p2 pj displaystyle p 1 p 2 ldots p j ye formulami ta f Wj displaystyle f in Omega j todi f p1 p2 pj displaystyle left f p 1 p 2 ldots p j right tezh ye formuloyu inshih formul nizh pobudovani za pravilami 1 i 2 nemaye Vivedennya formul i teorem Nehaj S displaystyle Sigma deyaka mnozhina formul L displaystyle mathcal L a A displaystyle A deyaka zadana formula to kazhut sho formula A displaystyle A vivoditsya z mnozhini formul S displaystyle Sigma poznachayetsya S A displaystyle Sigma vdash A yaksho isnuye taka skinchenna poslidovnist formul A1 A2 An A displaystyle A 1 A 2 ldots A n A de dlya kozhnoyi formuli Ai displaystyle A i Ai displaystyle A i ye aksiomoyu abo Ai displaystyle A i nalezhit mnozhini S displaystyle Sigma abo Ai displaystyle A i vivoditsya z poperednih formul poslidovnosti za dopomogoyu kotrogos iz pravil vivodu Yaksho pri comu mnozhina S displaystyle Sigma pusta formula A displaystyle A vivoditsya lishe za dopomogoyu aksiom i pravil vivodu to formula A displaystyle A nazivayetsya teoremoyu dlya cogo vikoristovuyetsya poznachennya A displaystyle vdash A Prikladi aksiomatikiPriklad 1 Alfavit elementi mnozhini A displaystyle mathrm A chislennya vislovlen skladayetsya z elementarnih vislovlen propozicijnih zminnih a b c d x y z displaystyle a b c d dots x y z mozhlivo z indeksami logichnimi operaciyami ye displaystyle lor land lnot rightarrow Ponyattya formuli viznachayetsya analogichno algebri vislovlen vsi propozicijni zminni ta elementarni vislovlennya ye formulami yaksho A i B formuli to virazi slova A B A B A A B displaystyle A lor B A land B lnot A A rightarrow B takozh ye formulami inshih formul nizh pobudovani za pravilami 2 1 i 2 2 nemaye Aksiomi V chislenni vislovlen viznachayut taki shemi aksiom A B A displaystyle A rightarrow B rightarrow A A B A B C A C displaystyle A rightarrow B rightarrow A rightarrow B rightarrow C rightarrow A rightarrow C A B A displaystyle A land B rightarrow A A B B displaystyle A land B rightarrow B A B A C A B C displaystyle A rightarrow B rightarrow A rightarrow C rightarrow A rightarrow B land C A A B displaystyle A rightarrow A lor B B A B displaystyle B rightarrow A lor B A C B C A B C displaystyle A rightarrow C rightarrow B rightarrow C rightarrow A lor B rightarrow C A B B A displaystyle A rightarrow lnot B rightarrow B rightarrow lnot A A A displaystyle lnot lnot A rightarrow A Yedinim pravilom vivodu ye A B AB displaystyle frac A rightarrow B A B Modus ponens U danih shemah aksiom ta pravila vivodu simvoli A B C displaystyle A B C mozhna zamishuvati usima dopustimimi formulami pislya chogo i otrimuyutsya konkretni aksiomi Priklad vivedennya teoremi Koristuyuchis podanimi aksiomami i pravilom vivedennya pokazhemo sho D D displaystyle D rightarrow D ye teoremoyu v danij formalnij sistemi dlya bud yakoyi formuli D displaystyle D Priklad vivoduNomer Formula Sposib oderzhannya1 D D D D D D D D D displaystyle D rightarrow D rightarrow D rightarrow D rightarrow D rightarrow D rightarrow D rightarrow D rightarrow D Aksioma 2 z zaminoyu A B C displaystyle A B C na D D D D displaystyle D D rightarrow D D vidpovidno2 D D D displaystyle D rightarrow D rightarrow D aksioma 1 zamina A B displaystyle A B na D displaystyle D 3 D D D D D D displaystyle D rightarrow D rightarrow D rightarrow D rightarrow D rightarrow D 1 2 i modus ponens 4 D D D D displaystyle D rightarrow D rightarrow D rightarrow D aksioma 1 zamina A B displaystyle A B na D D D displaystyle D D rightarrow D vidpovidno 5 D D displaystyle D rightarrow D 3 4 i modus ponens Priklad 2 aksiomi Lukashevicha Alfavit elementi mnozhini A displaystyle mathrm A chislennya vislovlen skladayetsya z elementarnih vislovlen propozicijnih zminnih a b c d x y z displaystyle a b c d dots x y z mozhlivo z indeksami logichnimi operaciyami ye displaystyle lnot rightarrow Ponyattya formuli viznachayetsya analogichno algebri vislovlen vsi propozicijni zminni ta elementarni vislovlennya ye formulami yaksho A i B formuli to virazi slova A A B displaystyle lnot A A rightarrow B takozh ye formulami inshih formul nizh pobudovani za pravilami 2 1 i 2 2 nemaye Nastupnu prostu sistemu aksiom zaproponuvav polskij logik Yan Lukashevich A B A displaystyle A to B to A A B C A B A C displaystyle A to B to C to A to B to A to C A B B A displaystyle neg A to neg B to B to A Yedinim pravilom vivodu ye A B AB displaystyle frac A rightarrow B A B Modus ponens Yak i u poperednomu prikladi dani virazi ye shemami aksiom Priklad vivedennya teoremi Koristuyuchis aksiomami Lukasevicha i pravilom vivedennya pokazhemo sho D D displaystyle D rightarrow D ye teoremoyu v danij formalnij sistemi dlya bud yakoyi formuli D displaystyle D Priklad vivoduNomer Formula Sposib oderzhannya1 D D D D D D D D D displaystyle D rightarrow D rightarrow D rightarrow D rightarrow D rightarrow D rightarrow D rightarrow D rightarrow D Aksioma 2 z zaminoyu A B C displaystyle A B C na D D D D displaystyle D D rightarrow D D vidpovidno2 D D D D displaystyle D rightarrow D rightarrow D rightarrow D aksioma 1 zamina A B displaystyle A B na D D D displaystyle D D rightarrow D vidpovidno 3 D D D D D displaystyle D rightarrow D rightarrow D rightarrow D rightarrow D 1 2 i modus ponens 4 D D D displaystyle D rightarrow D rightarrow D aksioma 1 zamina A B displaystyle A B na D displaystyle D 5 D D displaystyle D rightarrow D 3 4 i modus ponens SemantikaU podanih vishe formalnih sistemah i operatori mozhut faktichno mati dovilnu prirodu Dlya logiki vazhlive znachennya maye interpretaciya cih simvoliv Interpretaciya viznachayetsya zadannyam istinnosti tobto nadannyam kozhnij atomarnij formuli odnogo iz znachen 1 Istina chi 0 Hiba a takozh viznachennyam operatoriv yak bulevih funkcij vid svoyih operandiv Najchastishe vzhivani operatori zadayutsya za dopomogoyu tablic istinnosti p p1001 displaystyle begin array c c p amp neg p hline 1 amp 0 0 amp 1 hline end array pqp q111100010000 displaystyle begin array c c c p amp q amp p land q hline 1 amp 1 amp 1 1 amp 0 amp 0 0 amp 1 amp 0 0 amp 0 amp 0 hline end array pqp q111101011000 displaystyle begin array c c c p amp q amp p lor q hline 1 amp 1 amp 1 1 amp 0 amp 1 0 amp 1 amp 1 0 amp 0 amp 0 hline end array pqp q111100011001 displaystyle begin array c c c p amp q amp p to q hline 1 amp 1 amp 1 1 amp 0 amp 0 0 amp 1 amp 1 0 amp 0 amp 1 hline end array pqp q111100010001 displaystyle begin array c c c p amp q amp p land q hline 1 amp 1 amp 1 1 amp 0 amp 0 0 amp 1 amp 0 0 amp 0 amp 1 hline end array Zvazhayuchi na sposib pobudovi formul kozhna formula pri deyakomu zadannyu istinnosti otrimuye pevne znachennya 0 abo 1 Znachennya najprostishih formul dlya riznih zavdan istinnosti mozhna obchislyuvati za dopomogoyu tablic istinnosti Napriklad pqr p q p q p r p q p r 11110111101001101101110010010111011010101100101110000111 displaystyle begin array c c c c c c c p amp q amp r amp p lor q amp neg p lor q amp p to r amp neg p lor q to p to r hline 1 amp 1 amp 1 amp 1 amp 0 amp 1 amp 1 1 amp 1 amp 0 amp 1 amp 0 amp 0 amp 1 1 amp 0 amp 1 amp 1 amp 0 amp 1 amp 1 1 amp 0 amp 0 amp 1 amp 0 amp 0 amp 1 0 amp 1 amp 1 amp 1 amp 0 amp 1 amp 1 0 amp 1 amp 0 amp 1 amp 0 amp 1 amp 1 0 amp 0 amp 1 amp 0 amp 1 amp 1 amp 1 0 amp 0 amp 0 amp 0 amp 1 amp 1 amp 1 hline end array Yaksho dlya deyakogo zadannya istinnosti I displaystyle I formula A displaystyle A nabuvaye znachennya 1 to kazhut sho formula A displaystyle A zadovolnyaye zadannya I displaystyle I Formula sho zadovolnyaye usi mozhlivi zadannya istinnosti yak formula p q p r displaystyle neg p lor q to p to r z prikladu nazivayetsya tavtologiyeyu Yaksho S displaystyle Sigma deyaka mnozhina formul to kazhut sho dana mnozhina zadovolnyaye zadannya istinnosti yaksho ce zadannya zadovolnyaye kozhna formula ciyeyi mnozhini Yaksho dlya deyakoyi formuli A displaystyle A z togo sho mnozhina S displaystyle Sigma zadovolnyaye zadannyu istinnosti viplivaye sho A displaystyle A zadovolnyaye comu zadannyu to formula A displaystyle A nazivayetsya logichnim naslidkom mnozhini S displaystyle Sigma poznachayetsya S A displaystyle Sigma vDash A U vipadku yaksho mnozhina S displaystyle Sigma ye pustoyu formula ye tavtologiyeyu Osnovni problemi chislennya vislovlenDokladnishe Osnovni problemi chislennya vislovlen Dlya obgruntuvannya bud yakoyi aksiomatichnoyi teoriyi neobhidno rozglyanuti nastupni 4 problemi Nesuperechlivosti Povnoti Nezalezhnosti Rozv yaznostiProblema nesuperechlivosti Oznachennya Nehaj zadano deyaku formalnu aksiomatichnu teoriyu Govoryat sho pobudovana model ciyeyi teoriyi yaksho vsim simvolam alfavitu nadano deyakogo konkretnogo zmistu yakij opisuye pevnu neformalnu teoriyu i vidnoshennya mizh elementami ciyeyi teoriyi Formalna aksiomatichna teoriya nazivayetsya kategorichnoyu yaksho bud yaki yiyi 2 modeli izomorfni mizh soboyu tobto mizh nimi mozhna vstanoviti vzayemno odnoznachnu vidpovidnist Formalna aksiomatichna teoriya nazivayetsya nesuperechlivoyu vidnosno svoyeyi modeli yaksho bud yaka teorema sho dovoditsya v formalnij teoriyi ye istinnim tverdzhennyam dlya modeli Formalna aksiomatichna teoriya chislennya vislovlen nazivayetsya vnutrishno nesuperechlivoyu yaksho v cij teoriyi ne mozhna dovesti deyaku teoremu formulu razom z yiyi zaperechennyam Formalna aksiomatichna teoriya nazivayetsya sintaksichno nesuperechlivoyu yaksho v nij isnuye hocha b yakas formula yaka ne ye teoremoyu Teorema Formalna aksiomatichna teoriya chislennya vislovlen ye nesuperechlivoyu vidnosno svoyeyi modeli algebri vislovlen Naslidok Chislennya vislovlen vnutrishno nesuperechliva teoriya Chislennya vislovlen sintaksichno nesuperechliva teoriya Teorema Formalna aksiomatichna teoriya chislennya vislovlen ye kategorichnoyu Problema povnoti Formalna aksiomatichna teoriya chislennya vislovlen nazivayetsya povnoyu u vuzkomu rozuminni yaksho priyednannya do sistemi aksiom ciyeyi teoriyi hocha b odniyeyi formuli yaka ne ye teoremoyu vede do togo sho teoriya staye vnutrishno superechlivoyu Formalna aksiomatichna teoriya chislennya vislovlen ye povnoyu u shirokomu rozuminni abo povnoyu vidnosno svoyeyi modeli yaksho bud yaka formula istinna v modeli ye teoremoyu v cij teoriyi abo yaksho bud yaku totozhno istinnu formulu mozhna dovesti Naslidok Chislennya vislovlen ye povnim Spravedlivist cogo tverdzhennya bezposeredno viplivaye z teoremi U matematichnij logici isnuye j inshe ponyattya povnoti sistemi aksiom sho gruntuyetsya na nemozhlivosti dopovnennya sistemi aksiom bud yakoyu formuloyu yaku ne mozhna vivesti z danih aksiom Teorema Formalna aksiomatichna teoriya chislennya vislovlen ye povnoyu vidnosno svoyeyi modeli algebri vislovlen Teorema Chislennya vislovlen ce formalna aksiomatichna teoriya povna u vuzkomu rozuminni Problema nezalezhnosti Div takozh Nezalezhnist sistemi aksiom Oznachennya Nehaj zadano deyaku formalnu aksiomatichnu teoriyu govoryat sho deyaka aksioma ciyeyi teoriyi ye nezalezhnoyu yaksho yiyi ne mozhna dovesti metodami samoyi teoriyi yak teoremu Sistema aksiom formalnoyi aksiomatichnoyi teoriyi nazivayetsya nezalezhnoyu sistemoyu aksiom yaksho vsi aksiomi ye nezalezhnimi Teorema Sistema aksiom chislennya vislovlen ye nezalezhnoyu Dovedennya Dlya dovedennya nezalezhnosti deyakoyi aksiomi chislennya vislovlen vikoristovuyut nastupnij pidhid buduyut taku model formalnoyi aksiomatichnoyi teoriyi v yakij spravdzhuyutsya vsi aksiomi okrim danoyi Yaksho dovoditsya sho taka model izomorfna standartnij modeli formalnoyi aksiomatichnoyi teoriyi to robitsya visnovok sho aksioma ne ye nezalezhnoyu yaksho zh takogo izomorfizmu nemaye nezalezhna Priklad Yak model formalnoyi aksiomatichnoyi teoriyi vizmemo a b b vse inshe ne zminyuyemo pokazhemo sho II2 i II3 spravdzhuyutsya a II1ni II2 a b b b b II3 a b a c a b c a b a c a c II1a b a b a Dovedeno Naslidok Sistema aksiom chislennya vislovlen ye nezalezhnoyu Problema rozv yaznosti Polyagaye v tomu shob dovesti isnuvannya algoritmu yakij dlya bud yakoyi formuli chislennya vislovlen viznachaye chi mozhna yiyi dovesti chi ni Teorema Problema rozv yaznosti chislennya vislovlen ye rozv yaznoyu Teorema 1 Bud yaka totozhno istinna formula algebri vislovlen ye teoremoyu chislennya vislovlen Dovedennya Nehaj A dovilna formula chislennya chislennya vislovlen Pobuduyemo dlya neyi tablicyu istinnosti i rozglyanemo yiyi ostannij stovpchik Yaksho vin mistit lishe odinici to A totozhno istinna formula i za teoremoyu 1 ye teoremoyu chislennya vislovlen V inshomu vipadku ostannij stovpchik tablici istinnosti mistit hocha b odin nul A ne tavtologiya i znachit A ne ye teoremoyu Div takozhMatematichna logika Predikatna logika Buleva algebra Logika pershogo poryadku Chislennya sekvencij Kon yunktivna normalna forma Diz yunktivna normalna forma Logichnij spoluchnik Osnovni problemi chislennya vislovlen Simvolichna logikaDzherelaGilbert D Akkerman V Osnovy teoreticheskoj logiki M 1947 Klini S K Vvedenie v metamatematiku M 1957 Mendelson E Vvedenie v matematicheskuyu logiku M 1976 Enderton H B A Mathematical Introduction to Logic Harcourt Academic Press 2002 ISBN 0 12 238452 0 A G Hamilton Logic for Mathematicians Cambridge University Press Cambridge UK 1978 ISBN 0 521 21838 1 LiteraturaPrijma S M Matematichna logika i teoriya algoritmiv Navchalnij posibnik Melitopol TOV Vidavnichij budinok MMD 2008 134 s Gasyak O S Formalna logika korotkij slovnik dovidnik Chernivci Cherniveckij nac un t 2014 200 s Logichni chislennya Filosofskij enciklopedichnij slovnik V I Shinkaruk gol redkol ta in Kiyiv Institut filosofiyi imeni Grigoriya Skovorodi NAN Ukrayini Abris 2002 742 s 1000 ekz BBK 87ya2 ISBN 966 531 128 X Chislennya vislovlyuvan FES s 714 Matviyenko M P Shapovalov S P Matematichna logika ta teoriya algoritmiv Navchalnij posibnik K Vidavnictvo Lira K 2015 212 s PosilannyaURE