Logiko de supera ordo

En matematiko kaj logiko, logiko de supera ordo estas formo de predikatkalkulo distingata de la predikata logiko de la unua ordo pere de aldonaj kvantigiloj kaj, fojfoje, per pli forta semantiko. Logiko de supera ordo kun sia norma semantiko estas pli esprimkapabla, sed ĝiaj model-teoriaj ecoj estas pli kompleksaj ol tiuj de la unuaorda logiko.

La anglalingva termino por logiko de supera ordo nome "higher-order logic", mallongigita kiel HOL, estas ofte uzata por referenci simplan predikatkalkulon de supera ordo. Tie "simpla" indikas, ke subkuŝa teorio de tipoj estas la teorio de simplaj tipoj, nomata ankaŭ simpla teorio de tipoj. Leon Chwistek kaj Frank P. Ramsey proponis tion kiel simpligon de la komplika kaj aspra branĉigita teorio de tipoj specifita en la Principia Mathematica de Alfred North Whitehead kaj Bertrand Russell. Nuntempe simplaj tipoj estas rimedo por ekskludi plurformajn kaj dependajn tipojn.

Bibliografio

• Andrews, Peter B. (2002). An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, 2a eld, Kluwer Academic Publishers, ISBN 1-4020-0763-9
• Stewart Shapiro, 1991, "Foundations Without Foundationalism: A Case for Second-Order Logic". Oxford University Press., ISBN 0-19-825029-0
• Stewart Shapiro, 2001, "Classical Logic II: Higher Order Logic," en Lou Goble, eld., The Blackwell Guide to Philosophical Logic. Blackwell, ISBN 0-631-20693-0
• Lambek, J. kaj Scott, P. J., 1986. Introduction to Higher Order Categorical Logic, Cambridge University Press, ISBN 0-521-35653-9
• Jacobs, Bart (1999). Categorical Logic and Type Theory. Studies in Logic and the Foundations of Mathematics 141. North Holland, Elsevier. ISBN 0-444-50170-3.
• Benzmüller, Christoph; Miller, Dale (2014). "Automation of Higher-Order Logic". In Gabbay, Dov M.; Siekmann, Jörg H.; Woods, John (eld.). Handbook of the History of Logic, Volume 9: Computational Logic. Elsevier. ISBN 978-0-08-093067-1.