neděle 28. února 2016
21:51
Formální systém predikátové logiky (axiomy a odvozovací pravidla, dokazatelnost, model a důsledek teorie, věty o úplnosti a kompaktnosti, prenexní tvar formulí).
[link]
Formální (axiomatický) systém predikátové logiky je tvořen: 
jazykem predikátové logiky (zde redukovaný pouze logické spojky negace ¬, implikace → a obecný kvantifikátor ∀)
axiomy
odvozovacími pravidly
Axiomy predikátové logiky
Axiomy lze definovat pouze za použití spojek ¬ a → a kvantifikátoru ∀. Přepis existenčního kvantifikátoru na univerzální ∃𝑥𝜑 je logicky ekvivalentní formule ¬(∀𝒙(¬𝝋))
Není pravda, že by pro všechna 𝑥 neplatila formule 𝜑
Axiomy výrokové logiky (predikátová logika je rozšířením výrokové logiky, přejímá i její axiomy)
𝜑→𝜓→𝜑
Zda můžu prostřední implikaci otočit? - tipuji, že ANO
𝝋
𝝍
Res
1
1
1
1
0
1
0
1
1
0
0
1
Axiom kvantifikátoru
Axiom substituce
Říkáme, že term t je substituovatelný za proměnnou x do formule φ, jestliže x není volná v žádné podformuli tvaru ∀𝑦𝜓, kde proměnná y má výskyt v termu t.
Například následující substituce neplatí:∀𝑥¬∀𝑦𝑥=𝑦→(¬∀𝑦(𝑦=𝑦))
Tedy, pokud náš term t obsahuje proměnnou y, která je v místě substituce vázaná, musí tam být i x vázaná.
Substituovatelná proměnná x je taková, že žádný její volný výskyt neleží v oboru kvantifikátoru proměnné y, která je obsažená v substituovaném termu. Např. term S(y) není substituovatelný za term x ve formuli 𝑥→∃𝑦(𝑥=𝑆(𝑦))
Axiomy rovnosti (je-li L jazyk s rovností)
𝒙=𝒙 je axiom (x je proměnná) (reflexivita)
Pozn.: Symetrie a tranzitivita jde z těchto axiomů odvodit.
Odvozovací pravidla
Pravidlo zobecnění: Pro libovolnou proměnnou 𝒙 z 𝝋 lze odvodit ∀𝒙𝝋
𝑃𝑜𝑘𝑢𝑑⊢𝑍𝑥, 𝑝𝑎𝑘⊢∀𝑥𝑍(𝑥), kde Z(x) značí pravdivou formuli predikátové logiky a ∀xZ(x) je jeho rozšířením vzhledem k proměnné x.
Pravidlo odloučení (Modus Ponens): Z formulí 𝝋,𝝋→𝝍 (předpoklady) lze odvodit 𝝍 (závěr).
Důkaz - libovolná posloupnost formulí jazyka L, každá formule je buď axiom nebo ji lze odvodit z některých předchozích formulí.
Formule 𝝋 je dokazatelná z předpokladů T, jestliže existuje důkaz z předpokladů T. Píšeme 𝑇⊢𝜑.
Teorie - Je-li L jazyk prvního řádu a T množina formulí jazyka L, říkáme, že T je teorie prvního řádu s jazykem L. Formulím z T říkáme speciální axiomy teorie T.
Model -  Je-li M realizace jazyka L taková, že v ní je splněn každý speciální axiom T, říkáme, že M je modelem teorie T, a píšeme M |= T.
Gödelova věta o úplnosti predikátové logiky
Větou o úplnosti se obvykle nazývá následující ekvivalence. Implikace zleva doprava se někdy nazývá věta o korektnosti.
Formule 𝜑 je dokazatelná v teorii T, právě když 𝜑 platí v každém modelu T.
Prenexní tvar formulí
Definice
Formule A je v prenexní formě, jestliže má tvar 𝑸𝟏𝒙𝟏…𝑸𝒏𝒙𝒏𝑩 a je splněno
𝑄𝑖 je buď ∀ nebo ∃
B je otevřená vormule (neobsahuje kvantifikátor)
Každou formuli predikátové logiky 1. řádu lze převést na formuli v tzv. prenexním normálním tvaru, která je původní formuli ekvivalentní. Formule v tomto tvaru začíná kvantifikátory (obecné a existenční), které kvantifikují za nimi následující jádro. Jádro je otevřená formule, tj. formule, která neobsahuje kvantifikované proměnné. Pro převod formule do prenexního tvaru existuje několik málo pravidel, které formuli rekurzivně převádějí.
From <[link]> 
Postup
Jádro lze dále převést do konjunktivního, resp. disjunktivního normálního tvaru (CNF, resp. DNF). Formule v CNF (DNF) je stručně řečeno konjunkce disjunkcí (¬𝐀∧(𝐁∨𝐂)) (disjunkce konjunkcí). Opět s pomocí několika jednoduchých pravidel lze ve třech krocích každou otevřenou formuli do normálního tvaru převést.
Řešený příklad
Skolemizace, Skolemova normální forma
[link]
Skolemizace je převod formulí na formule bez existenčních kvantifikátorů v jazyce, který je rozšířen o tzv. Skolemovy funkce; zachovává splnitelnost.
Skolemova normální forma je prenexová normální forma pouze s univerzálními kvantifikátory.
Ideí je transformace formule (∀𝑥1)…(∀𝑥𝑛)(∃𝑦)(𝑃𝑥1,…,𝑥𝑛,𝑦) na formuli ∀𝒙𝟏…∀𝒙𝒏𝑷𝒙𝟏,…,𝒇𝒙𝟏,…,𝒙𝒏
podmínku na existenci 𝑦 můžeme chápat jako podmínku na existenci zobrazení 𝑓 (tzv. výběrové funkce), která pro konkrétní hodnoty 𝑥1,…,𝑥𝑛 konstruuje požadované 𝑦=𝑓(𝑥1,…,𝑥𝑛).
Například mějme čísla s + : ∀𝒙∃𝒚 :𝒙+𝒚=𝟎 převedeme na ∀𝒙 :𝒙+𝒇(𝒙)=𝟎, kde interpretace funkce f je, že vrátí opačné číslo k číslu x (unární operátor mínus).
-----------------------------------------------------------------
Věty, lemma, definice
Věta o korektnosti: Libovolná formule jazyka 𝐿 dokazatelná v predikátové logice 1. řádu je logicky platnou formulí, tj. je splněna v každé realizaci jazyka 𝐿.
Pravidlo ∀: Je-li ⊢𝜑→𝜓 a proměnná 𝑥 nemá volný výskyt ve 𝜑, pak ⊢𝜑→(∀𝑥𝜓).
Pravidlo ∃: Je-li ⊢𝜑→𝜓 a proměnná 𝑥 nemá volný výskyt ve 𝜓, pak ⊢(∃𝑥𝜑)→𝜓.
Uzávěr formule: Jsou-li x1,...,xn všechny volné proměnné ve formuli 𝜑, pak formuli ∀𝑥1…∀𝑥𝑛𝜑 nazveme uzávěrem formule 𝜑.
Věta o uzávěru: Je-li T množina formulí, je-li 𝜑′ uzávěr formule 𝜑, pak 𝑇⊢𝜑 právě když 𝑇⊢𝜑′.
Distribuce kvantifikátorů: Je-li ⊢𝜑→𝜓, potom ⊢∀𝑥𝜑→(∀𝑥𝜓), ⊢∃𝑥𝜑→∃𝑥𝜓.
Věta o dedukci: Nechť 𝑇 je množina formulí jazyka 𝐿, nechť 𝜑 je uzavřená formule, 𝜓 je libovolná formule jazyka 𝐿. Potom 𝑇⊢𝜑→𝜓 právě tehdy, když 𝑇,𝜑⊢𝜓.
Notes
2. Otazka (predmet) (okruh): MAT - 7. Formální systém predikátové logiky (axiomy a odvozovací pravidla, dokazatelnost )
Kdo me primarne zkousel: Šlapal Josef, prof. RNDr., CSc.
Co jsem k tomu rekl(a)/na co se ptali/co mne vytkli:
Chtěl jsem začít s popisem základních pojmů. To mě ale zastavil a že chce konkrétně ti axiomy. Tak jsem si vzpomněl akorát na ty tři z výrokové logiky a na Pravidlo odloučení. Pak mi řekl, že tam je ještě axiom kvantifikátorů a substituce. Na to jsem si ale nemohl vzpomenout, tak jsem něco napsal na tabuli, ale bylo to úplně špatně. Pak se ptal co je to důkaz to jsem mu začal vlastními slovy popisovat a zastavil mě s tím, že to chce stručně a jasně. Nakonec zhodnotil, že jsem se na predikátovou logiku moc nepodíval a že mu to stačí. Dohromady jsem teda nedal víc než ty tři axiomy a stejně mi dali za E 
From <[link]> 
2. Formální systém predikátové logiky (axiomy a odvozovací pravidla, dokazatelnost, věty o úplnosti)
Kdo me primarne zkousel:
Šlapal
Co jsem k tomu rekl(a)/na co se ptali/co mne vytkli:
Šlapal mi ihned řekl, ať začnu Výrokovou logikou.
Napsal jsem tedy: tři axiomy a odvozovací pravidlo MP.
Pak jsem do začal rozšiřovat o axiomy predikátové log. a odvozovací pravidla. Zmínil jsem, že P.L. přidává 2 další axiomy a jedno odvozovací pravidlo. Načeš se Šlapal zamračil a já rychle dodal, že pokud to není jazyk s rovností.
Popsal jsem nové axiomy. Pak se mě ptal na "substituovatelný term". Chtěl to říci přesně (Používat spojení jako obor kvantifikátoru)
Já jsem to spíše popisoval jako v lambda kalkulu. Pak se mne zeptal co je to důkaz. Teď ovšem přišel kámen úrazu. Zeptal se mě na Větu o úplnosti. Dostal jsem okno. Úplný Windows. Snažil se mě na to navést, mě ale začal vypínat mozek. Nakonec se do toho přidal ještě Čéška a zeptal se mne na aximon (-B -> -A) -> (A->B). Zda můžu prostřední implikaci otočit. Teď jsem se to snažil odvodit. No nakonec jsme to dali nějak dohromady. Nakonec B
From <[link]> 
1. Otazka (předmět) (okruh): MAT - Formální systém výrokové logiky (podtrženo výrokové)
Kdo me primarne zkousel: prof. Češka
Co jsem k tomu rekl(a)/na co se ptali/co mne vytkli: U této otázky jsme se trochu hledali - docela mě to i zaskočilo, protože takhle se ten okruh nejmenoval 
 Moc ho nezajímal jazyk ani sémantika, ale postupně jsme se dopracovali k tomu, že chtěl axiomy, odvozovací pravidla (hlavně MP). Potom jsme řešili rozdíly oproti predikátové - pořád jsem mluvil o jazyku, modelech, ale to nechtěl. Po chvíli jsem se dopracoval k (beze)spornosti, tautologiím, ke Gödelovi. Celkově jsem spíš odpovídal na otázky a chtěl úplně jiný pohled, než jsme řešili v MATu. Musím však říct, že mu moc nevadilo, že jsem nevěděl co myslí. 
From <[link]> 
1. Otazka (okruh): Formální systém predikátové logiky (axiomy a odvozovací pravidla, dokazatelnost, model a důsledek
teorie, věty o úplnosti a kompaktnosti, prenexní tvar formulí).
Kto ma primarne skusal: doc. Horák (FI MUNI)
Co som k tomu povedel/na co sa ma ptali:
Otázky jsem dostal na papírcích a hned mi oznámili, jaké části se přesně věnovat. U této otázky jsem se měl věnovat čistě formulím v prenexním tvaru. Něco jsem řekl a pak jsem ho nechal ať se ptá... V podstatě jsem věděl skoro všechno. Chtěl po mě převést jednu formuli do prenexního tvaru, to bylo celkem v klidu. Celkem jsem pletl názvosloví, místo termů jsem říkal proměnné apod. Ale asi pochopil, že vím jak se tomu říká a jen v té rychlosti říkám blbosti. 
 Chtěl něco o rezoluci, něco jsem řekl, nakolik dobře už nevím... Dále se mně zeptal co je Skolemova normální forma, bohužel jsem si nevzpomněl... Výsledek - B.
From <[link]> 