-
při ekvivalentních transformacích formulí soustavně uplatňujeme zejména ...
De Morganovy zákony pro záměnu kvantifikátorů a tautologie VL. Připomeňme si, že vzájemně ekvivalentní formule vyplývají jedna z druhé a že řetězec ekvivalentních transformací můžeme pokládat za důkaz koncové formule z kterékoli předcházející formule.
-
Při ekvivalentních transformacích se snažíme o to, aby se symboly negace vyskytovaly nanejvýše před ...
atomickými (pod)formulemi
-
Následující výroky formalizujte prostředky PL a takto získané formule transformujte na formule ekvivalentní, které pak vyjádřete slovně.
Co je skutečné, to je rozumné.
- Formálně ∀x (S(x)→R(x))
- Ekvivalentní formule:
- ↔ ¬∃x ¬(S(x)→R(x)) DM zákon
- ↔ ¬∃x (S(x)∧¬R(x)) tautologie VL
- Slovně „Neexistuje něco skutečné, co není rozumné“. Daný výrok je mimochodem ekvivalentní výroku „Pouze rozumné je skutečné“ s formalizací ∀x (R(x)←S(x)).
-
Vrozené ideje neexistují.
- Formálně ¬∃x (V(x)∧I(x))
- Ekvivalentní formule:
- ↔ ∀x ¬(V(x)∧I(x)) DM zákon
- ↔ ∀x (¬V(x)∨¬I(x)) tautologie VL
- ↔ ∀x (V(x)→¬I(x)) tautologie VL
- Slovně „Nic vrozené není idea“. Ekvivalentní je i „Žádná idea není vrozená“, protože ∀x (V(x)→¬I(x)) ↔ ∀x (I(x)→¬V(x)).
-
Člověk je tvor společenský.
- Formálně ∀x (Č(x)→(T(x)∧S(x)))
- Ekvivalentní formule:
- ↔ ¬∃x ¬(Č(x)→(T(x)∧S(x))) DM zákon
- ↔ ¬∃x (Č(x)∧¬(T(x)∧S(x))) tautologie VL
- ↔ ¬∃x (Č(x)∧(¬T(x)∨¬S(x))) tautologie VL
- Slovně „Neexistuje člověk, který není tvor nebo není společenský“.
-
Nic není v rozumu, co by nebylo ve smyslech.
- Formálně ¬∃x (R(x)∧¬S(x))
- Ekvivalentní formule:
- ↔ ∀x ¬(R(x)∧¬S(x)) DM zákon
- ↔ ∀x (¬R(x)∨¬¬S(x)) tautologie VL
- ↔ ∀x (¬R(x)∨S(x)) tautologie VL
- ↔ ∀x (R(x)→S(x)) tautologie VL
- Slovně „Je-li to v rozumu, bylo to ve smyslech“.
(Jiná vhodná formalizace je ∀x (¬R(x)←¬S(x)), kdy ¬S(x) reprezentuje podmínku a tedy antecedent implikace „co by nebylo ve smyslech“; obrat „Nic není v rozumu“ obsahuje nám jíž známý dvojí gramatický zápor češtiny, jenž reprezentujeme jedním záporem logickým. ∀x (¬R(x)←¬S(x)) je ekvivalentní ∀x (¬S(x)→¬R(x)) a tedy pak ∀x (R(x)→S(x)).)
-
Zvláště v prostředí informatiky jsou často diskutovány prenexní formy formulí a rozmanitá problematika o ně se opírající, zejm. skolemizace, Herbrandova procedura, Robinsonův unifikační algoritmus, rezoluční dokazování ad.
Formule A je v prenexní normální formě (či prenexním tvaru) právě tehdy, když má tvar...
- Q1x1Q2x2...Qnxn B, kde Qk (pro 1 ≤ k ≤ n) označuje ∀ nebo ∃ a proměnné x1, x2,..., xn jsou od sebe různé (tj. žádná se nevyskytuje dvakrát)
- Sekvence „Q1x1Q2x2...Qnxn“ se nazývá prefix a „B“ se nazývá (otevřené) jádro formule A.
- (Formule Q1x1Q2x2...Qnxn B je zvána univerzální či existenční formule v souladu s tím, zda Q1, Q2, ...,Qn jsou jen obecné či jen existenční kvantifikátory.)
-
Věta o prenexní normální formě říká, že ...
ke každé formuli A existuje formule B v prenexní normální formě, přičemž platí, že A↔B.
-
Tzv. Skolemova normální forma je formule ekvivalentní ...
- ekvivalentní formuli v prenexní normální formě, nicméně všechny existenční kvantifikátory a jimi vázané proměnné byly postupem skolemizace nahrazeny Skolemovou funkcí.
- Například formuli ∀x∀y∃z R(x,y,z) odpovídá Skolemova normální forma ∀x∀y R(x,y,f(x,y)).
-
K převodu formulí do jejich prenexní normální formy používáme De Morganovy zákony a další transformační logické zákony (ty používáme jako pravidla, čili zákon A→B je pravidlem A / B). Zejména pro přesun kvantifikátorů ven, tj. dopředu, jsou používány následující čtyři zákony distributivity kvantifikátorů: ...
- (A→∀x B) ↔ ∀x (A→B) →∀
- (A→∃x B) ↔ ∃x (A→B) →∃
- (∀x A→B) ↔ ∃x (A→B) ∀→
- (∃x A→B) ↔ ∀x (A→B) ∃→
- Při přesouvání kvantifikátorů musí být proměnné vhodně přejmenovávány (de facto vyměněny za jinou proměnnou), abychom zabránili tomu, že proměnné začnou být vázány jiným kvantifikátorem.
-
příklad transformací formule do jejího prenexního normálního tvaru: ∀x∃y R(x,y)→∃z∀x R(z,x)
- ∀x∃y R(x,y)→∃z∀x R(z,x)
- ↔ ∀x∃y R(x,y)→∃z∀w R(z,w) ...přejmenování proměnné (w/x)
- ↔ ∃z (∀x∃y R(x,y)→∀w R(z,w)) ...→∃
- ↔ ∃z∀w (∀x∃y R(x,y)→R(z,w)) ...→∀
- ↔ ∃z∀w∃x (∃y R(x,y)→R(z,w)) ...∀→
- ↔ ∃z∀w∃x∀y (R(x,y)→R(z,w)) ∃→
-
příklad transformací formule do jejího prenexního normálního tvaru: ∃x∀y R(x,y)→∀x∃y R(x,y)
- ∃x∀y R(x,y)→∀x∃y R(x,y)
- ↔ ∃x∀y R(x,y)→∀w∃z R(w,z) ...přejmenování proměnných (w/x, z/y)
- ↔ ∀w (∃x∀y R(x,y)→∃z R(w,z)) ...→∀
- ↔ ∀w∃z (∃x∀y R(x,y)→R(w,z))... →∃
- ↔ ∀w∃z∀x (∀y R(x,y)→R(w,z)) ...∃→
- ↔ ∀w∃z∀x∃y (R(x,y)→R(w,z)) ...∀→
- Danou formuli bychom totiž mohli upravovat i v jiném pořadí aplikace pravidel
- ∃x∀y R(x,y)→∀x∃y R(x,y)
- ↔ ∃x∀y R(x,y)→∀w∃z R(w,z) ...přejmenování proměnných (w/x, z/y)
- ↔ ∀x (∀y R(x,y)→∀w∃z R(w,z)) ...∃→
- ↔ ∀x∃y (R(x,y)→∀w∃z R(w,z)) ...∀→
- ↔ ∀x∃y∀w (R(x,y)→∃z R(w,z)) ...→∀
- ↔ ∀x∃y∀w∃z (R(x,y)→R(w,z)) ...→∃
- Oba získané výsledky jsou však ekvivalentní a mohou být dále převedeny na identickou formuli pomocí zákonů pro záměnu pořadí kvantifikátorů.
- Právě dosaženou formuli ∀x∃y∀w∃z (R(x,y)→R(w,z)) bychom tak upravili třeba na
- ↔ ∀x∀w∃y∃z (R(x,y)→R(w,z)) ...záměna pořadí ∃ a ∀
- O něco výše dosaženou formuli ∀w∃z∀x∃y (R(x,y)→R(w,z)) bychom těmito zákony zase upravili postupně následovně:
- ↔ ∀w∀x∃z∃y (R(x,y)→R(w,z)) ...záměna pořadí ∃ a ∀
- ↔ ∀w∀x∃y∃z (R(x,y)→R(w,z)) ...záměna pořadí ∃ a ∃
- ↔ ∀x∀w∃y∃z (R(x,y)→R(w,z)) ...záměna pořadí ∀ a ∀
-
tento příklad má kromě jiného připomenout, že formule, jež nejsou tvaru implikace, lze po vhodných převodech na tvar implikace převést, aby pak mohly být aplikovány výše uváděné zákony pro distribuci kvantifikátorů; ∃x P(x)∨∃x ¬P(x)
- ∃x P(x)∨∃x ¬P(x)
- ↔ ¬∃x P(x)→∃x ¬P(x) ...tautologie VL
- ↔ ¬∃x P(x)→∃y ¬P(y) ...přejmenování proměnné (y/x)
- ↔ ∃y (¬∃x P(x)→¬P(y)) ...→∃
- ↔ ∃y (∀x ¬P(x)→¬P(y)) ...DM
- ↔ ∃y∃x (¬P(x)→¬P(y)) ...∀→
- ↔ ∃x∃y (¬P(x)→¬P(y)) ...záměna pořadí ∃ a ∃
-
Následující formule upravte do prenexní normální formy.
∃x∀y R(x,y)∨∀x∃y R(x,y)
-
Následující formule upravte do prenexní normální formy.
∀x (P(x)→∀y (Q(x,y)→¬∀z R(y,z)))
-
Následující formule upravte do prenexní normální formy. Pro úpravu této formule použijte zákon ∃x (A∧B) ↔ (A∧∃x B).
|
|
