Predikátová logika prvního řádu
From Wikipedia, the free encyclopedia
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ů.