Predikátová logika vyššího řádu

V matematice se predikátová logika (tj. soustava pravidel, jak formalizovat pojmy teorie a důkaz) dělí na logiku prvního řádu a logiku vyšších řádů.

V logice prvního řádu lze kvantifikátory, tj. výrazy „pro každé“ a „existuje nějaké“, používat pouze na samotné objekty, nikoli na jejich množiny. Například:

V teorii, která popisuje částečně uspořádané množiny (a má tedy binární predikátové symboly $=$ a $\preceq$ ), lze vyslovit: Pro každé $x$ existuje $y\not =x$ takové, že $x\preceq y$ (tj. uspořádání je shora neomezené). Ale nelze vyslovit: Každá neprázdná množina $A$ má nejmenší prvek $m$ takový, že pro všechny $x\in A$ platí $m\preceq x$ , což je součást definice dobře uspořádané množiny. Takové tvrzení není formulí predikátové logiky prvního řádu.
V aritmetice nelze vyslovit zákon matematické indukce jako jednu formuli: Pro každou množinu $M$ , která splňuje dvě podmínky (že $0\in M$ a že s každým $a\in M$ platí i $(a+1)\in M$ ), platí, že „ $M$ je totožná s celým univerzem,“ neboli že pro každé $x$ je splněno $x\in M$ . Proto je třeba tento výrok imitovat nekonečným schématem axiomů indukce, ovšem tato imitiace nepokrývá vše, tj. nebrání tomu, aby existovaly i nestandardní modely PA (tj. neizomorfní s přirozenými čísly), v níž taková množina přesto existuje, jen není vymezená žádným axiomem tohoto schématu. Následkem toho Peanova aritmetika není úplná teorie, např. neumí prokázat vlastní bezespornost, jak dokazují Gödelovy věty o neúplnosti.

Predikátová logika druhého řádu umožňuje kvantifikovat i přes množiny, třetího řádu přes množiny množin atd.

Další vlastnost, kterou se logika vyššího řádu liší od logiky prvního řádu, jsou dovolené konstrukce v typové teorii, na které je (případně) založena. Predikát vyššího řádu je takový predikát, který má jeden nebo víc jiných predikátů jako argumenty. Obecně, predikát vyššího řádu, který má řád n, má jeden nebo víc predikátů řádu (n − 1) jako svoje argumenty (pro n > 1). Podobnou vlastnost mají funkce vyšších řádů, běžně využívané ve funkcionálním programování

Logiky vyšších řádů mají větší vyjadřovací sílu, ale kvůli svým vlastnostem, zvláště vzhledem k teorii modelů, mají méně vhodné chování pro mnoho aplikací. Gödel dokázal, že klasická logika vyššího řádu nedovoluje (rekurzivně axiomatizovatelný) korektní a úplný důkazový systém. Ale existuje takový důkazový systém, který je korektní a úplný vzhledem k Henkinovým modelům.

Příklady logik vyšších řádů jsou Churchova jednoduchá teorie typů (angl. 'Simple Theory of Types') a kalkulus konstrukcí (angl. 'calculus of constructions').

Vztah mezi logikou prvního řádu a logikami vyšších řádů

Logika druhého řádu reflektuje problémy axiomatizace ZF (Willard Van Orman Quine ji proto nazýval "teorií množin v rouše beránčím"), neboť v případě kvantifikace přes všechny možné predikáty (počínaje unárními) se pracuje s potenčními množinami, což může vést k překročení hranice mezi spočetnýmni a nespočetnými množinami. Z tohoto důvodu se v praktických aplikacích logik vyšších řádů používá tzv. obecná sémantika, ve které platí, že každá bezesporná teorie má spočetný model. Na druhou stranu Jaakko Hintikka dokázal, že jakákoliv logika řádu n>2 je ekvivalentní logice druhého řádu, rozšířením jazyka logiky druhého řádu tedy nezískáme expresivnější formalismus. Toto tvrzení dokázal Hintikka tím, že ukázal, jak v logice druhého řádu vyjádřit operátor potenční množiny—máme-li unární predikát I pro individua, S pro množiny a binární E pro náležení, následující konjunkce modeluje až na isomorfismus operátor potence:

$(\forall x.Ix+Sx)\land (\forall x\forall y.Exy\supset Ix\land Sy)\land (\forall x\forall y.(Sx\land Sy\land \forall t.Etx\equiv Ety)\supset x=y)\land (\forall X\exists y.Sy\land \forall t.It\supset (Ety\equiv Xt))$

Odkazy

Reference

V tomto článku byl použit překlad textu z článku Higher-order logic na anglické Wikipedii.

Literatura

Andrews, P.B., 2002. An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, 2nd ed. Kluwer Academic Publishers, available from Springer.
Church, Alonzo, 1940, "A Formulation of the Simple Theory of Types," Journal of Symbolic Logic 5: 56-68.
Henkin, Leon, 1950, "Completeness in the Theory of Types," Journal of Symbolic Logic 15: 81-91.
Stewart Shapiro, 1991, "Foundations Without Foundationalism: A Case for Second-Order Logic". Oxford University Press.
Stewart Shapiro, 2001, "Classical Logic II: Higher Order Logic," in Lou Goble, ed., The Blackwell Guide to Philosophical Logic. Blackwell.
Lambek, J. and Scott, P. J., 1986. Introduction to Higher Order Categorical Logic, Cambridge University Press.

Související články

Externí odkazy

(anglicky) Miller, Dale, 1991, "Logic: Higher-order," Encyclopedia of Artificial Intelligence, 2nd ed.