Підтримка
www.wikidata.uk-ua.nina.az
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 zv yazok logichnih operatoriv Danu mnozhinu mozhna rozbiti na pidmnozhini W W 0 W 1 W j W m displaystyle Omega Omega 0 cup Omega 1 cup ldots cup Omega j cup ldots cup Omega m dd dd U comu rozbitti W j displaystyle Omega j ye mnozhina operatoriv arnosti j displaystyle j takozh poznacheno W 0 0 1 displaystyle Omega 0 0 1 Najchastishe vikoristovuyutsya operatori W 1 displaystyle Omega 1 lnot dd dd W 2 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 p 1 p 2 p j displaystyle p 1 p 2 ldots p j ye formulami ta f W j displaystyle f in Omega j todi f p 1 p 2 p j 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 A 1 A 2 A n A displaystyle A 1 A 2 ldots A n A de dlya kozhnoyi formuli A i displaystyle A i A i displaystyle A i ye aksiomoyu abo A i displaystyle A i nalezhit mnozhini S displaystyle Sigma abo A i 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 A B 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 vivodu Nomer Formula Sposib oderzhannya 1 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 vidpovidno 2 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 A B 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 vivodu Nomer Formula Sposib oderzhannya 1 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 vidpovidno 2 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 p 1 0 0 1 displaystyle begin array c c p amp neg p hline 1 amp 0 0 amp 1 hline end array p q p q 1 1 1 1 0 0 0 1 0 0 0 0 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 p q p q 1 1 1 1 0 1 0 1 1 0 0 0 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 p q p q 1 1 1 1 0 0 0 1 1 0 0 1 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 p q p q 1 1 1 1 0 0 0 1 0 0 0 1 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 p q r p q p q p r p q p r 1 1 1 1 0 1 1 1 1 0 1 0 0 1 1 0 1 1 0 1 1 1 0 0 1 0 0 1 0 1 1 1 0 1 1 0 1 0 1 0 1 1 0 0 1 0 1 1 1 0 0 0 0 1 1 1 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 yaznosti Problema 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
Топ