Теоре́ма про деду́кцію (ле́ма про деду́кцію, теоре́ма деду́кції) — один із фундаментальних результатів у теорії доведення, формалізує спосіб міркування, за якого для встановлення імплікації використовується як необхідна умова виведення. Використовується для встановлення існування висновків і доведень без їх побудови. Вперше явно сформулював і довів Ербран, а без доведення використовував її 1928 року. Незалежно цей принцип сформулював 1930 року Тарський. За повідомленням Тарського, він знав і застосовував цей принцип ще 1921 року.
Формулювання для числення висловлень
- Якщо , то .
- Якщо , то .
Тут — логічні формули (формальної теорії для числення висловлень), означає, що формула виводиться з формули (в теорії ), а означає, що формулу доведено (є теоремою теорії ). Знак означає логічну операцію імплікації.
Формулювання для теорій першого порядку
Нехай — підмножина (можливо порожня) формул деякої теорії першого порядку , і — формули теорії . Тоді, якщо існує таке виведення формули зі множини формул , в якому ні при якому застосуванні [en] до формул, залежних у цьому виведенні від формули , не зв'язується жодна з вільних змінних формули , то .
Див. також
Примітки
- Математическая логика, 1973, с. 54-55.
Література
- Клини С. К. Математическая логика. — М. : Мир, 1973. — 480 с.
Вікіпедія, Українська, Україна, книга, книги, бібліотека, стаття, читати, завантажити, безкоштовно, безкоштовно завантажити, mp3, відео, mp4, 3gp, jpg, jpeg, gif, png, малюнок, музика, пісня, фільм, книга, гра, ігри, мобільний, телефон, android, ios, apple, мобільний телефон, samsung, iphone, xiomi, xiaomi, redmi, honor, oppo, nokia, sonya, mi, ПК, web, Інтернет
Teore ma pro dedu kciyu le ma pro dedu kciyu teore ma dedu kciyi odin iz fundamentalnih rezultativ u teoriyi dovedennya formalizuye sposib mirkuvannya za yakogo dlya vstanovlennya implikaciyi A B displaystyle A Rightarrow B vikoristovuyetsya A displaystyle A yak neobhidna umova vivedennya Vikoristovuyetsya dlya vstanovlennya isnuvannya visnovkiv i doveden bez yih pobudovi Vpershe yavno sformulyuvav i doviv Erbran a bez dovedennya vikoristovuvav yiyi 1928 roku Nezalezhno cej princip sformulyuvav 1930 roku Tarskij Za povidomlennyam Tarskogo vin znav i zastosovuvav cej princip she 1921 roku Formulyuvannya dlya chislennya vislovlenYaksho A B displaystyle A vdash B to A B displaystyle vdash A Rightarrow B Yaksho A1 Am 1 Am B displaystyle A 1 A m 1 A m vdash B to A1 Am 1 Am B displaystyle A 1 A m 1 vdash A m Rightarrow B Tut A B A1 Am 1 Am displaystyle A B A 1 A m 1 A m logichni formuli formalnoyi teoriyi L displaystyle L dlya chislennya vislovlen A B displaystyle A vdash B oznachaye sho formula B displaystyle B vivoditsya z formuli A displaystyle A v teoriyi L displaystyle L a B displaystyle vdash B oznachaye sho formulu B displaystyle B dovedeno ye teoremoyu teoriyi L displaystyle L Znak A B displaystyle A Rightarrow B oznachaye logichnu operaciyu implikaciyi Formulyuvannya dlya teorij pershogo poryadkuNehaj G displaystyle Gamma pidmnozhina mozhlivo porozhnya formul deyakoyi teoriyi pershogo poryadku K displaystyle K A displaystyle A i B displaystyle B formuli teoriyi K displaystyle K Todi yaksho isnuye take vivedennya formuli B displaystyle B zi mnozhini formul G A displaystyle Gamma cup A v yakomu ni pri yakomu zastosuvanni en do formul zalezhnih u comu vivedenni vid formuli A displaystyle A ne zv yazuyetsya zhodna z vilnih zminnih formuli A displaystyle A to G A B displaystyle Gamma vdash A Rightarrow B Div takozhTeorema ErbranaPrimitkiMatematicheskaya logika 1973 s 54 55 LiteraturaKlini S K Matematicheskaya logika M Mir 1973 480 s