Cesko.wiki Predikátová logika prvního řádu
Author
Albert FloresPredikátová logika prvního řádu je formální systém používaný v matematice, filozofii, lingvistice a informatice. Často se pro její označení používá kratší a méně přesný termín predikátová logika. Predikátová logika prvního řádu se odlišuje od výrokové logiky zavedením kvantifikovaných proměnných.
Teorie o určitém tématu bývá obvykle právě predikátová logika prvního řádu společně se: specifickou univerzální množinou (též. univerzem), ze které jsou brány proměnné, dále pak konečně mnoha funkcemi a predikáty nad touto množinou, a konečně množinou rekurzivních axiomů, jež jsou v rámci teorie pokládány za platné. +more Někdy pojmem teorie formálně rozumíme množinu vět (sentencí) zapsaných v predikátové logice.
Kromě predikátové logiky prvního řádu existují logiky vyšších řádů. Tyto logiky se odlišují tím, že povolují predikáty uvnitř predikátů, kvantifikování predikátu i funkcí (případně predikátů a funkcí zároveň). +more U teorií predikátové logiky prvního řádu jsou predikáty svázány s teorií množin, kdežto v případě logik vyšších řádů bývají predikáty interpretovány jako množiny množin.
Existuje velké množství deduktivních systémů pro predikátovou logiku prvního řádu, které jsou korektní (všechna dokazatelná tvrzení jsou pravdivá) a úplné (všechna pravdivá tvrzení jsou dokazatelná). Velký pokrok byl zaznamenán na poli automatických dokazovačů postavených právě na této logice, a to i přes její semi-rozhodnutelnost v oblasti dokazovačů. +more A v neposlední řadě splňuje několik metalogických vět, např. Löwenheim-Skolemovu větu nebo větu o kompaktnosti.
Predikátová logika prvního řádu je nesmírně důležitá již pro samotné základy matematiky, protože je standardní logikou pro axiomatické systémy. Mnoho běžných axiomatických systémů, jako Peanova aritmetika a axiomatická teorie množin (včetně Zermel-Fraenkelovy teorie množin), lze formalizovat pomocí predikátové logiky. +more Zato žádná teorie prvního řádu nemá sílu plně a kategoricky popsat struktury s nekonečnou doménou, např. celá čísla nebo reálná čísla. K tomu jsou zapotřebí logiky vyšších řádů.
Úvod
Zatímco výroková logika se zabývá jednoduchými a deklarativními výroky, predikátová logika prvního řádu zavádí jako nadstavbu predikáty a kvantifikátory. Predikát se podobá funkci nabývající booleovské hodnoty (pravda - nepravda).
Uvažujme následující věty: “Sókratés je filozof. ” a “Platón je filozof. +more” Ve výrokové logice se bude jednat o dva čistě nezávislé výroky, označeny např. p a q. V predikátové logice s nimi bude zacházeno daleko provázaněji za použití predikátu P(x). Predikát P říká, že objekt, reprezentovaný proměnnou x, je filozof. Tedy, pokud bude x reprezentovat Sókrata, bude P říkat to samé co výrok p. Obdobně tomu bude u Platóna a druhého výroku. Na tomto příkladu je patrný klíčový aspekt predikátové logiky prvního řádu: P jako symbol je syntaktickou entitou, které byl dán sémantický význam deklarováním, že P(x) platí právě tehdy, když x je filozofem. Takovémuto přiřazení sémantického významu říkáme interpretace.
Predikátová logika umožňuje uvažování nad vlastnostmi, jež jsou sdíleny mnoha objekty, díky použití proměnných. Uveďme si příklad, nechť P(x) značí, že x je filozof a nechť S(x) vyjadřuje, že x je učenec. +more Pak formule :\text{P}(x)\to \text{S}(x) \, říká, že pokud x je filozof pak x je učenec. Symbol \to se používá pro označení implikace (podmínkové věty). Hypotéza leží nalevo od šipky, závěr na druhé straně. Pravdivost této formule závisí na tom, jaký objekt je reprezentován proměnnou x, a na interpretaci predikátů P a S.
Pro vyjádření výrazů ve formě "pro každé x, pokud x je filozofem, pak x je učencem" již nestačí použití proměnných, ale musíme použít kvantifikátor. Opět, nechť P(x) značí, že x je filozof a nechť S(x) znamená, že x je učencem. +more Pak sentence prvního řádu: :\forall x ( \text{P}(x) \to \text{S}(x)) vyjadřuje, že nehledě na to, co x reprezentuje, tak jestliže x je filozofem, pak x je učencem. Zde \forall, neboli univerzální kvantifikátor, vyjadřuje myšlenku, že výraz v závorkách platí pro všechny volby proměnné x.
Pro dokázání nepravdivosti tvrzení "jestliže x je filozof, pak x je učencem" musíme ukázat, že existuje filozof, který není učencem. Toto protitvrzení můžeme vyjádřit za pomoci existenčního kvantifikátoru \exists: :\exists x ( \text{P}(x) \land \lnot \text{S}(x)). +more Zde: * \lnot je operátor negace: \lnot \text{S}(x) je pravda právě tehdy, když \text{S}(x) \, je nepravda - jinými slovy, právě tehdy, když x není učenec. * \land operátor konjunkce: \text{P}(x) \land \lnot \text{S}(x) značí, že x je filozof a zároveň není učenec.
Predikáty P(x) a S(x) z předchozího příkladu mají pouze jeden parametr. Predikátová logika prvního řádu je ovšem schopná zvládnout i predikáty s více než jedním parametrem. +more Například, "existuje osoba, která se nechá pokaždé napálit" můžeme popsat následovně: :\exists x (\mbox{P}(x) \land \forall y (\mbox{T}(y) \rightarrow \mbox{F}(x,y))). Tentokrát P(x) znamená, že x je osoba, Time(y) je interpretován tak, že y je moment v čase, a F(x,y) značí, že (osoba) x může být napálena v (čase) y. Pro jasnost, toto prohlášení říká, že "existuje alespoň jedna osoba, která může být napálena ve všech časových momentech", což je silnější tvrzení než: "pro všechny časové momenty existuje alespoň jedna osoba, jež může být napálena". Druhé tvrzení totiž nespecifikuje, zda je ona napálená osoba jedna a tatáž pro všechny okamžiky.
Rozsahem kvantifikátorů rozumíme množinu objektů, které je mohou uspokojit (v předchozích neformálních příkladech nebyl uváděn). Navíc, kromě specifikace významu predikátových symbolů, musí interpretace určit neprázdnou množinu známou jako univerzální množina nebo univerzum, jakožto rozsah pro kvantifikátory. +more Pak lze o prohlášení ve formě \exists a \text{P}(x) říci, že je pravdivé vzhledem k určité interpretaci, pokud existuje nějaký objekt z univerza v rámci této interpretace, který zaručí, že interpretace přiděluje správný význam predikátu P.
Syntax
Predikátová logika prvního řádu se skládá ze dvou klíčových částí. Syntax určuje, jaké kolekce (posloupnosti) symbolů jsou legální výrazy predikátové logiky, zatímco sémantika hovoří o významu za těmito výrazy.
Abeceda
Na rozdíl od přirozených jazyků, jako Čeština, je jazyk predikátové logiky prvního řádu zcela formální, tedy můžeme zcela mechanicky určit, zda je daný výraz legálně utvořen. Rozlišujeme dva základní druhy výrazů: termy, které intuitivně představují objekty, a formule, jež zahrnují predikáty a mohou být pravdivé nebo nepravdivé. +more Termy a formule predikátové logiky jsou řetězce symbolů, jež společně tvoří abecedu jazyka. Stejně jako u všech formálních jazyků, je povaha těchto symbolů mimo záběr formální logiky. Často jsou brány jednoduše jako písmena a interpunkční znaménka.
Běžně rozlišujeme symboly abecedy na logické symboly, které mají vždy tentýž význam, a mimo-logické symboly, jejichž význam se liší dle interpretace. Např. +more, logický symbol \land vždy reprezentuje "a" ("a zároveň"); nikdy není interpretován jako "nebo" (či jako jiná spojka). Na druhou stranu, mimo-logický predikátový symbol P(x) můžeme interpretovat tak, že x je filozof, x je osoba, nebo jako jiný unární predikát závisející na konkrétní interpretaci.
Logické symboly
Máme několik logických symbolů patřících do abecedy, které se mohou lišit autor od autora, ale obvykle mezi ně patří:
* Kvantifikační symboly \forall a \exists
* Logické spojky: \land pro konjunkci, \lor pro disjunkci, \rightarrow pro implikaci, \harr pro ekvivalenci, \lnot pro negaci. Výjimečně se zařazují další logické spojky. +more Mnozí autoři používají \Rightarrow, nebo Cpq, namísto \rightarrow, a \Harr, či Epq, místo \harr, obzvláště v kontextu, kdy \to je použita k jiným účelům. Dále, \supset může nahradit \rightarrow; místo \harr lze použít \equiv, a tilda (~), Np, nebo Fpq, mohou nahradit \lnot; ||, či Apq zase \lor; a &, nebo Kpq, mohou být použity místo \land, zejména pokud tyto symboly nemohou být použity z různých technických důvodů.
* Různé druhy závorek a jiná interpunkční znaménka. Volba těchto symbolů se liší dle kontextu.
* Nekonečná množina proměnných, často označovaných malými písmeny z konce abecedy x, y, z, etc. . Lze také použít dolní index k rozlišení proměnných: x0, x1, x2, …
* Symbol rovnosti =
Stojí za poznamenání, že ne všechny výše zmíněné symboly jsou nezbytné. Postačují: pouze jeden z kvantifikátorů (obvykle univerzální), negace a konjunkce, proměnné, závorky a symbol rovnosti. +more V neposlední řadě, lze definovat ještě další drobné variace:.
* Mnohdy zavádíme pravdivostní konstanty: T, Vpq, nebo \top, pro "pravdu" (tautologii) a F, Opq, nebo \bot, pro "nepravdu" (kontradikci). Bez takovýchto logických operátorů nulové arity můžeme tyto dvě konstanty vyjádřit pouze za pomoci kvantifikátorů.
* Někdy přidáváme další logické spojky, jako např. Shefferova funkce, Dpq (NAND), nebo exkluzivní disjunkce, Jpq.
Mimo-logické symboly
Mimo-logické symboly představují predikáty (relace), funkce a konstanty představené v rámci univerza. Standardní praxí bylo používat fixní, nekonečnou množinu mimologických symbolů pro všechny účely. +more V současnosti používáme různé mimo-logické symboly podle zamýšlené aplikace. Proto začalo být nutné pojmenovat množinu všech mimo-logických symbolů použitou pro konkrétní aplikaci. Tuto volbu zprostředkovává tzv. signatura.
V tradičním přístupu máme pouze jednu nekonečnou množinu mimo-logických symbolů (jednu signaturu) pro všechny aplikace. V důsledku to znamená, že existuje pouze jeden jazyk predikátové logiky prvního řádu. +more Tento přístup se stále objevuje, zejména ve filosoficky orientovaných knihách. # Pro každé přirozené číslo n ≥ 0 existuje posloupnost n-árních predikátových symbolů. Jelikož predikáty představují relace mezi n elementy, říká se jim také relační symboly. Pro každou aritu n jich máme nekonečnou zásobu: #: Pn0, Pn1, Pn2, Pn3, … # Pro každé přirozené číslo n ≥ 0 existuje nekonečně mnoho n-árních funkčních symbolů: #: f n0, f n1, f n2, f n3, ….
V současné matematické logice se signatura liší dle aplikace. Typické signatury jsou {1, ×} nebo pouze {×} pro grupy, či {0, 1, +, ×,
Pravidla tvorby
Pravidla tvorby definují termy a formule pro predikátovou logiku prvního řádu. Pokud jsou termy a formule reprezentovány řetězci symbolů, mohou být tato pravidla použita k sepsání formální gramatiky pro termy a formule. +more Pravidla jsou obecně bezkontextová gramatika, s výjimkou toho, že množina symbolů může být nekonečná a startovacích symbolů může být mnoho.
Termy
Množina termů je induktivně definována pomocí následujících pravidel: # Proměnné. Jakákoli proměnná je term. +more # Funkce. Jakýkoli výraz f(t1,. ,tn) s n argumenty (kde každý argument ti je term a f je funkční symbol arity n) je term. Speciálně, symboly reprezentující jednotlivé konstanty jsou 0-ární funkční symboly, a jsou tedy termy. # Pouze výrazy vytvořené konečně mnoha aplikacemi pravidel 1 a 2 jsou termy. Např. žádný výraz obsahující predikátový symbol není term.
Formule
Množina formulí (známá také jako dobře utvořené formule) je rekursivně definována následujícími pravidly: # Predikátové symboly. Pokud P je n-ární predikátový symbol t1, . +more, tn jsou termy, pak P(t1,. ,tn) je formule. # Symbol rovnosti. Jestliže je symbol rovnosti součástí logiky a t1 a t2 jsou termy, pak t1 = t2 je formule. # Negace. Pokud φ je formule, pak \negφ je také formule. # Binární spojky. Pokud φ a ψ jsou formule, pak (φ \rightarrow ψ) je také formule. Analogicky definujeme pro ostatní binární spojky. # Kvantifikátory. Pokud φ je formule a x je proměnná, pak \forall x \varphi a \exists x \varphi jsou formule. # Pouze výrazy získané konečně mnoha aplikacemi pravidel 1-5 jsou formule. Formulím sestavených za pomocí prvních dvou pravidel říkáme atomické formule.
Například, :\forall x \forall y (P(f(x)) \rightarrow\neg (P(x) \rightarrow Q(f(y),x,z))) je formule, jestliže f je unární funkční symbol, P je unární predikátový symbol a Q je ternární predikátový symbol. Naopak, \forall x\, x \rightarrow není formule, ačkoli se jedná o řetězec znaků patřících do abecedy.
Rolí závorek v definici je zajistit, aby jakákoli formule mohla být utvořena jedním způsobem, a to dle rekurzivní definice (jinak řečeno, existuje jedinečný derivační strom pro každou formuli). Tato vlastnost se nazývá jedinečná čitelnost (anglicky unique readability) formulí. +more Máme mnoho konvencí pro to, kde a jak používat závorky ve formulích. Například, někteří autoři používají dvojtečky nebo tečky namísto závorek, jindy se mění umístění závorek. Každý autor by měl v rámci své konvence ověřit, že jeho řešení dostává čitelnosti.
Definice formule představená výše nedovoluje definování jestliže-pak-jinak (if-then-else) funkce ite(c,a,b), kde "c" je podmínka vyjádřená jako formule, jež by navracela "a", pokud by c bylo pravdivé a "b", jestliže je nepravdivé. Tento nedostatek je důsledek faktu, že predikáty a funkce mohou přijímat pouze termy jako parametry (’’ite’’ funkce má jako první parametr formuli). +more Některé jazyky stavějící na predikátové logice prvního řádu, např. SMT-LIB 2. 0, toto dovolují.
Konvence
Kvůli pohodlnosti se zavedlo mnoho konvencí zabývajících se prioritou logických operátorů, převážně za účelem vyhnutí se psaní závorek. Tato pravidla se podobají prioritě početních operací v aritmetice. +more Běžnou konvencí je: * \lnot se vyhodnocuje jako první * \land a \lor jsou vyhodnoceny následně * Kvantifikátory následují ve vyhodnocení * \to je vyhodnocena jako poslední. Navíc, lze přidat extra interpunkci, která není definicí vyžadována, aby byla formule čitelnější. Tedy formule :(\lnot \forall x P(x) \to \exists x \lnot P(x)) může být přepsána na :(\lnot [\forall x P(x)]) \to \exists x [\lnot P(x)].
V některých oborech je běžné používat infixovou notaci pro binární relace a funkce namísto prefixové notace (použité v definici výše). Například v aritmetice typicky píšeme "2 + 2 = 4" místo "=(+(2,2),4)". +more Je zvykem považovat formule zapsané v infixové notaci za zkratky pro odpovídající formule v prefixové notaci.
Výše představené definice používají infixovou notaci pro binární spojky, jako je \to. Méně používanou konvencí je tzv. +more Polská notace, ve které píšeme \rightarrow, \wedge, atd. před jejich argumenty namísto mezi. Tato notace nám dovoluje odprostit se od veškeré interpunkce. Polská notace je kompaktní a elegantní, ale zřídka používaná v praxi, protože je obtížná ke čtení. V Polské notaci přepíšeme formuli :\forall x \forall y (P(f(x)) \rightarrow\neg (P(x) \rightarrow Q(f(y),x,z))) na 1="∀x∀y→Pfx¬→ PxQfyxz".
Volné a vázané proměnné
Formule mohou obsahovat buď volné nebo vázané proměnné. Intuitivně, proměnnou nazveme volnou, pokud není kvantifikována: ve \forall y\, P(x,y), je proměnná x volnou, zatímco y je vázaná. +more Volné a vázané proměnné formule jsou definovány následovně: # Atomické formule: Pokud φ je atomická formule, pak x je volná proměnná φ právě tehdy, když se x vyskytuje ve φ. Dále nejsou žádné vázané proměnné v atomických formulích. # Negace: x je volná proměnná ve \negφ právě tehdy, když x je volná ve φ. x je vázaná ve \negφ právě tehdy, když x je vázaná ve φ. # Binární spojky: x je volná proměnná ve (φ \rightarrow ψ) právě tehdy, když x je volná buď ve φ nebo ψ. x je vázaná ve (φ \rightarrow ψ) právě tehdy, když x je vázaná buď ve φ nebo ψ. Stejné pravidlo uplatníme v případě jiných binárních spojek na místě \rightarrow. # Kvantifikátory: x je volná proměnná ve \forally φ právě tehdy, když x je volná ve φ a x je rozdílný symbol od y. Dále, x je vázaná ve \forally φ právě tehdy, když x je y nebo x je vázaná ve φ. Stejné pravidlo platí pro \exists na místě \forall.
Například ve \forallx \forally (P(x)\rightarrow Q(x,f(x),z)), x a y jsou vázané proměnné, z je volná proměnná a w není ani volná ani vázaná, neboť se ve formuli nevyskytuje.
Volnost a vázanost lze také specializovat na specifický výskyt proměnných ve formuli. Například ve P(x) \rightarrow \forall x\, Q(x), je první výskyt x volný, kdežto druhý vázaný. +more Řečeno jinak, x v P(x) je volná proměnná, zatímco x v \forall x\, Q(x) je vázaná.
Formule predikátové logiky prvního řádu bez volných proměnných se nazývá sentence prvního řádu. Sentence jsou tedy formule, které budou mít dobře definované pravdivostní hodnoty v rámci určité interpretace. +more Aby byla nějaká formule, např. P(x), pravdivá, musí záviset na tom, jaký objekt x reprezentuje. Zato sentence \exists x\, \text{P}(x) bude pravdivá nebo nepravdivá v závislosti na dané interpretaci.
Příklady
Abelovy grupy
V matematice obsahuje jazyk uspořádané abelovy grupy jeden konstantní symbol 0, jeden unární funkční symbol −, jeden binární funkční symbol +, a jeden binární relační symbol ≤. Pak: * Výrazy +(x, y) a +(x, +(y, −(z))) jsou termy. +more :Obvykle se zapisují jako ‘’x + y’’ a ‘’x + y − z’’. * Výrazy +(x, y) = 0 a ≤(+(x, +(y, −(z))), +(x, y)) jsou atomické formule. :Obvyklý zápis je ‘’x + y = 0’’ a x + y − z ≤ x + y. * Výraz (\forall x \forall y \, \mathop{\leq}(\mathop{+}(x, y), z) \to \forall x\, \forall y\, \mathop{+}(x, y) = 0) je formule, která se obvykle zapisuje následovně: \forall x \forall y ( x + y \leq z) \to \forall x \forall y (x+y = 0).
Axiomy
Pokud vhodně stanovíme axiomy predikátové logiky, stačí nám zavést následující 4 axiomy: * PRED-1: \forall x Z(x) \Rightarrow Z(y) * PRED-2: Z(y) \Rightarrow \exists x Z(x) * PRED-3: \forall x (W \Rightarrow Z(x)) \rightarrow (W \Rightarrow \forall x Z(x)) * PRED-4: \exists x (Z(x) \Rightarrow W) \Rightarrow (\exists x Z(x) \Rightarrow W)
Odvozovací pravidla
Odvozovací pravidlo může být formulováno takto: : \mathit{Pokud} \vdash Z(x), \mathit{pak} \vdash \forall x Z(x) kde Z(x) značí pravdivou formuli predikátové logiky a ∀xZ(x) je jeho rozšířením vzhledem k proměnné x.
Vztah k výrokové logice
Výrokovou logiku lze chápat jako speciální případ predikátové logiky. Predikát arity nula totiž odpovídá výrokové proměnné. +more Pokud tedy syntax výrokové logiky omezíme jen na takové predikáty, dostaneme logiku ekvivalentní výrokové. Predikátová logika je tedy striktně expresivnější, než výroková.