Predikátová logika prvního řádu

Prediká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é. 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ň).^[1] 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čů. 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. 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.” 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. Pak formule

${\displaystyle {\text{P}}(x)\to {\text{S}}(x)\,}$

říká, že pokud x je filozof pak x je učenec. Symbol ${\displaystyle \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. Pak sentence prvního řádu:

${\displaystyle \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 ${\displaystyle \forall }$, neboli obecný 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 ${\displaystyle \exists }$:

${\displaystyle \exists x({\text{P}}(x)\land \lnot {\text{S}}(x)).}$

Zde:

• ${\displaystyle \lnot }$ je operátor negace: ${\displaystyle \lnot {\text{S}}(x)}$ je pravda právě tehdy, když ${\displaystyle {\text{S}}(x)\,}$ je nepravda - jinými slovy, právě tehdy, když x není učenec.
• ${\displaystyle \land }$ operátor konjunkce: ${\displaystyle {\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. Například, "existuje osoba, která se nechá pokaždé napálit" můžeme popsat následovně:

${\displaystyle \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. Pak lze o prohlášení ve formě ${\displaystyle \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é. 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ř., logický symbol ${\displaystyle \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 ${\displaystyle \forall }$ a ${\displaystyle \exists }$

• Logické spojky: ${\displaystyle \land }$ pro konjunkci, ${\displaystyle \lor }$ pro disjunkci, ${\displaystyle \rightarrow }$ pro implikaci, ${\displaystyle \leftrightarrow }$ pro ekvivalenci, ${\displaystyle \lnot }$ pro negaci. Výjimečně se zařazují další logické spojky. Mnozí autoři používají ${\displaystyle \Rightarrow }$, nebo Cpq, namísto ${\displaystyle \rightarrow }$, a ${\displaystyle \Leftrightarrow }$, či Epq, místo ${\displaystyle \leftrightarrow }$, obzvláště v kontextu, kdy ${\displaystyle \to }$ je použita k jiným účelům. Dále, ${\displaystyle \supset }$ může nahradit ${\displaystyle \rightarrow }$; místo ${\displaystyle \leftrightarrow }$ lze použít ${\displaystyle \equiv }$, a tilda (~), Np, nebo Fpq, mohou nahradit ${\displaystyle \lnot }$; ||, či Apq zase ${\displaystyle \lor }$; a &, nebo Kpq, mohou být použity místo ${\displaystyle \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: x₀, x₁, x₂, …

• 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 obecný), negace a konjunkce, proměnné, závorky a symbol rovnosti. V neposlední řadě, lze definovat ještě další drobné variace:

• Mnohdy zavádíme pravdivostní konstanty: T, Vpq, nebo ${\displaystyle \top }$, pro "pravdu" (tautologii) a F, Opq, nebo ${\displaystyle \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. 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.^[2]

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. ^[3] Tento přístup se stále objevuje, zejména ve filosoficky orientovaných knihách.

1. 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:

   Pⁿ₀, Pⁿ₁, Pⁿ₂, Pⁿ₃, …

2. Pro každé přirozené číslo n ≥ 0 existuje nekonečně mnoho n-árních funkčních symbolů:

   f ⁿ₀, f ⁿ₁, f ⁿ₂, f ⁿ₃, …

V současné matematické logice se signatura liší dle aplikace. Typické signatury jsou {1, ×} nebo pouze {×} pro grupy, či {0, 1, +, ×, <} pro uspořádaná tělesa. Na počet mimo-logických symbolů nejsou kladena žádná omezení. Signaturou může být prázdná, konečná nebo nekonečná, dokonce nespočetná množina. Nespočetné signatury se objevují např. jako součást moderních důkazů Löwenheim-Skolemovy věty.

V moderním přístupu je každý mimo-logický symbol jedním z následujících typů.

1. Predikátový symbol (relační symbol) s určitou valencí (tj. aritou, počtem argumentů) větší nebo rovnou 0. Obvykle je značíme velkými písmeny P, Q, R,...
   • Relace s valencí 0 mohou značit výrokové proměnné. Například P může reprezentovat libovolný výrok.
   • Například P(x) je predikát s valencí 1. Jednou možnou interpretací je: "x je muž".
   • Q(x,y) je predikát s valencí 2. Možné interpretace zahrnují: "x je větší než y" a "x je otec y".
2. Funkční symbol s určitou valencí větší nebo rovnou 0. Funkční symboly často značíme malými písmeny f, g, h,... .
   • Příklady: f(x) může být interpretováno jako "otec x". V aritmetice může představovat "-x". V teorii množin může reprezentovat "potenční množinu množiny x". V aritmetice g(x,y) může korespondovat s "x+y". V teorii množin zase "sjednocení x a y".
   • Funkční symboly valence 0 se nazývají konstantní symboly a často je píšeme malými písmeny ze začátku abecedy a, b, c,... . Symbol a může představovat Sókrata. V aritmetice si lze představit jako 0. V teorii množin zase jako prázdnou množinu.

Z tradičního přístupu se jde jednoduše přesunout do moderního, pokud specifikujeme signaturu, která se bude skládat z tradičních sekvencí mimologických symbolů.

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. 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:

1. Proměnné. Jakákoli proměnná je term.
2. Funkce. Jakýkoli výraz f(t₁,...,t_n) s n argumenty (kde každý argument t_i 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.
3. 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^[4]) je rekursivně definována následujícími pravidly:

1. Predikátové symboly. Pokud P je n-ární predikátový symbol t₁, ..., t_n jsou termy, pak P(t₁,...,t_n) je formule.
2. Symbol rovnosti. Jestliže je symbol rovnosti součástí logiky a t₁ a t₂ jsou termy, pak t₁ = t₂ je formule.
3. Negace. Pokud φ je formule, pak ${\displaystyle \neg }$φ je také formule.
4. Binární spojky. Pokud φ a ψ jsou formule, pak (φ ${\displaystyle \rightarrow }$ ψ) je také formule. Analogicky definujeme pro ostatní binární spojky.
5. Kvantifikátory. Pokud φ je formule a x je proměnná, pak ${\displaystyle \forall x\varphi }$ a ${\displaystyle \exists x\varphi }$ jsou formule.
6. 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,

${\displaystyle \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, ${\displaystyle \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í. 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). Některé jazyky stavějící na predikátové logice prvního řádu, např. SMT-LIB 2.0, toto dovolují.^[5]

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. Běžnou konvencí je:

• ${\displaystyle \lnot }$ se vyhodnocuje jako první
• ${\displaystyle \land }$ a ${\displaystyle \lor }$ jsou vyhodnoceny následně
• Kvantifikátory následují ve vyhodnocení
• ${\displaystyle \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

${\displaystyle (\lnot \forall xP(x)\to \exists x\lnot P(x))}$

může být přepsána na

${\displaystyle (\lnot [\forall xP(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)". 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 ${\displaystyle \to }$. Méně používanou konvencí je tzv. Polská notace, ve které píšeme ${\displaystyle \rightarrow }$, ${\displaystyle \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

${\displaystyle \forall x\forall y(P(f(x))\rightarrow \neg (P(x)\rightarrow Q(f(y),x,z)))}$

na "∀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 ${\displaystyle \forall y\,P(x,y)}$, je proměnná x volnou, zatímco y je vázaná. Volné a vázané proměnné formule jsou definovány následovně:

1. 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.
2. Negace: x je volná proměnná ve ${\displaystyle \neg }$φ právě tehdy, když x je volná ve φ. x je vázaná ve ${\displaystyle \neg }$φ právě tehdy, když x je vázaná ve φ.
3. Binární spojky: x je volná proměnná ve (φ ${\displaystyle \rightarrow }$ ψ) právě tehdy, když x je volná buď ve φ nebo ψ. x je vázaná ve (φ ${\displaystyle \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ě ${\displaystyle \rightarrow }$.
4. Kvantifikátory: x je volná proměnná ve ${\displaystyle \forall }$y φ právě tehdy, když x je volná ve φ a x je rozdílný symbol od y. Dále, x je vázaná ve ${\displaystyle \forall }$y φ právě tehdy, když x je y nebo x je vázaná ve φ. Stejné pravidlo platí pro ${\displaystyle \exists }$ na místě ${\displaystyle \forall }$.

Například ve ${\displaystyle \forall }$x ${\displaystyle \forall }$y (P(x)${\displaystyle \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 ${\displaystyle P(x)\rightarrow \forall x\,Q(x)}$, je první výskyt x volný, kdežto druhý vázaný. Řečeno jinak, x v ${\displaystyle P(x)}$ je volná proměnná, zatímco ${\displaystyle x}$ v ${\displaystyle \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. Aby byla nějaká formule, např. P(x), pravdivá, musí záviset na tom, jaký objekt x reprezentuje. Zato sentence ${\displaystyle \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.

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 ${\displaystyle (\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ě: ${\displaystyle \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: ${\displaystyle \forall xZ(x)\Rightarrow Z(y)}$
• PRED-2: ${\displaystyle Z(y)\Rightarrow \exists xZ(x)}$
• PRED-3: ${\displaystyle \forall x(W\Rightarrow Z(x))\rightarrow (W\Rightarrow \forall xZ(x))}$
• PRED-4: ${\displaystyle \exists x(Z(x)\Rightarrow W)\Rightarrow (\exists xZ(x)\Rightarrow W)}$

Odvozovací pravidla

Odvozovací pravidlo může být formulováno takto:

${\displaystyle {\mathit {Pokud}}\vdash Z(x),{\mathit {pak}}\vdash \forall xZ(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é. Pokud tedy syntax predikátové logiky omezíme jen na takové predikáty, dostaneme logiku ekvivalentní výrokové. Predikátová logika je tedy striktně expresivnější, než výroková.

Poznámky