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 Henkinovský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').

[editovat] Odkazy

[editovat] Reference

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

[editovat] Související články

• Gramatika vyššího řádu
• Typovaný lambda kalkulus
• Intuicionistická teorie typů
• Vícedruhová logika
• Logika

[editovat] Externí odkazy

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

Tento matematický článek je příliš stručný nebo neobsahuje důležité informace. Pomozte Wikipedii tím, že jej vhodně rozšíříte.

Tento článek je zčásti nebo zcela založen na překladu článku Higher-order logic na anglické Wikipedii.