Cesko.wiki Logika vyššího řádu
Author
Albert FloresV 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. +more 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. +more 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. +more '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. +more 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 . +more 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
Literatura
Andrews, P. B. +more, 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
Gramatika vyššího řádu * Typovaný lambda kalkulus * Intuicionistická teorie typů * Vícedruhová logika * Logika
Externí odkazy
Miller, Dale, 1991, "[url=https://web. archive. +moreorg/web/20060104050925/http://www. lix. polytechnique. fr/Labo/Dale. Miller/papers/AIencyclopedia/]Logic: Higher-order,[/url]" Encyclopedia of Artificial Intelligence, 2nd ed.