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

V matematice se logika vyššího řádu odlišuje od predikátové logiky prvního řádu několika způsoby.

Jeden z nich je typ proměnných, přes které se kvantifikuje; v logice prvního řádu se kvantifikuje pouze pro proměnné pro individua a nelze kvantifikovat (volně řečeno) přes proměnné pro predikátové symboly. To lze v logice druhého řádu a dalších systémech.

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.