Prenex-formula
 |
Ennek a szócikknek hiányzik vagy nagyon rövid, illetve nem elég érthető a bevezetője. Kérjük, , ami jól összefoglalja a cikk tartalmát, vagy jelezd észrevételeidet a cikk vitalapján. |
 |
Ez a szócikk nem tünteti fel a független forrásokat, amelyeket felhasználtak a készítése során. Emiatt nem tudjuk közvetlenül ellenőrizni, hogy a szócikkben szereplő állítások helytállóak-e. Segíts megbízható forrásokat találni az állításokhoz! Lásd még: A Wikipédia nem az első közlés helye. |
Egy formula prenex-alakúvá tételéhez először változó-tiszta alakra kell hozni a formulát.
Változótiszta alak
[szerkesztés]Minden kvantor különböző változót köt, és egyik kötött változó sem egyezik meg egyetlen szabad változóval sem. Az a legegyszerűbb megoldás, hogy indexeljük a kötött változókat. Ha változótiszta lett a formula, utána alkalmazni kell a kvantorkiemelési törvényeket.
Egyoldali kvantorkiemelési törvények
[szerkesztés]∀xA(x) ∧ B ∼ ∀x(A(x) ∧ B)
A ∧ ∀xB(x) ∼ ∀x(A ∧ B(x))
∃xA(x) ∨ B ∼ ∃x(A(x) ∨ B)
A ∨ ∃xB(x) ∼ ∃x(A ∨ B(x))
¬∀xA(x) ∼ ∃x¬A(x)
¬∃xA(x) ∼ ∀x¬A(x)
A ⊃ ∃xB(x) ∼ ∃x(A ⊃ B(x))
A ⊃ ∀xB(x) ∼ ∀x(A ⊃ B(x))
∃xA(x) ⊃ B ∼ ∀x(A(x) ⊃ B)
∀xA(x) ⊃ B ∼ ∃x(A(x) ⊃ B)
∀xf(x) = ⌐∃x ⌐f(x)