Högre ordningslogik

Högre ordningens logik i matematik och logik är en form av predikatlogik som skiljer sig från första ordningens logik i ytterligare predikat över predikat, kvantifierare över dem och, följaktligen, rikare semantik . Högre ordningens logik med sin standardsemantik är mer uttrycksfull, men deras modellteoretiska egenskaper är mycket svårare att studera och tillämpa jämfört med första ordningens logik.

Första ordningens logik kvantifierar endast variabler; andra ordningens logik tillåter också kvantifiering av predikat och funktionssymboler (över uppsättningar); tredje ordningens logik använder och kvantifierar predikat över predikat (uppsättningar av mängder) och så vidare. Till exempel en andra ordningens mening

uttrycker principen om matematisk induktion . Högre ordningslogik inkluderar all lägre ordningslogik; med andra ord tillåter logik av högre ordning satser med predikat (överuppsättningar) med lägre häckningsdjup.

Exempel och egenskaper

Logik av högre ordning inkluderar utlöpare av kyrkans enkla typteori [1] och olika former av intuitionistisk typteori. Gerard Huet visade att föreningsproblemet är algoritmiskt olösligt i den intuitionistiska variationen av tredje ordningens logik [2] [3] [4] , det vill säga det finns ingen algoritm som skulle avgöra om en godtycklig ekvation har en lösning över tredje ordningens termer (och ännu mer genom termer godtycklig ordning över den tredje).

Med hänsyn till begreppet isomorfism, definieras den booleska operationen i andra ordningens logik. Med hjälp av denna observation slog Hintikka 1955 fast att högre ordningens logik kan representeras av andra ordningens logik i den meningen att man för varje formel av högre ordningens logik kan hitta en motsvarande lika giltig andra ordningens logikformel [5] .

I vissa sammanhang antas begreppet logik av högre ordning syfta på klassisk logik av högre ordning. Men modal logik av högre ordning har också studerats. Enligt vissa logiker studeras Gödels ontologiska bevis (ur teknisk synvinkel) i detta sammanhang ] .

Se även

• Första beställningslogik
• Andra ordningens logik
• Högre grammatik
• Intuitionistisk typteori
• Flersorterad logik
• Skrivet lambdakalkyl
• modal logik

Anteckningar

1. ↑ Church, Alonzo , A formulering av den enkla teorin om typer Arkiverad 15 november 2018 på Wayback Machine , The Journal of Symbolic Logic 5(2):56–68 (1940)
2. ↑ Huet, Gérard P.  Unifieringens obeslutbarhet i tredje ordningens logik  // Information och kontroll : journal. - 1973. - Vol. 22 , nr. 3 . - s. 257-267 . - doi : 10.1016/s0019-9958(73)90301-x .
3. ↑ Huet, Gerard (sep 1976). Resolution d'Equations dans des Langages d'Ordre 1,2,...ω (Ph.D.). Université de Paris VII.
4. ↑ Huet, Gerard. Higher Order Unification 30 år senare // Proceedings, 15th International Conference TPHOL  (engelska) / Carreño, V.; Muñoz, C.; Tahar, S. - Springer, 2002. - Vol. 2410. - S. 3-12. — (LNCS).
5. ↑ Stanford Encyclopedia of Philosophy artikel om högre ordningslogik . Hämtad 9 augusti 2016. Arkiverad från originalet 17 juni 2016. (obestämd)
6. ↑ Passande, MelvinTyper, tablåer och Gödels Gud. - Springer Science & Business Media , 2002. - P. 139. - ISBN 978-1-4020-0604-3 . . — “Godels argument är modalt och åtminstone av andra ordningen, eftersom det i hans definition av Gud finns en explicit kvantifiering över egenskaper. [...] [AG96] visade att man kunde se en del av argumentet inte som andra ordningens utan som tredje ordningens."

Litteratur

• Andrews, Peter B. (2002). An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof , 2nd ed, 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," i Lou Goble, red., The Blackwell Guide to Philosophical Logic . Blackwell, ISBN 0-631-20693-0
• Lambek, J. och Scott, PJ, 1986. Introduction to Higher Order Categorical Logic , Cambridge University Press, ISBN 0-521-35653-9
• Jacobs, Bart. Kategorisk logik och typteori . - North Holland, Elsevier, 1999. - (Studier in Logic and the Foundations of Mathematics 141). - ISBN 0-444-50170-3 .
• Benzmuller, Christoph; Miller, Dale. Automation of Higher-Order Logic // Handbook of the History of Logic, Volym 9: Computational Logic  (engelska) / Gabbay, Dov M.; Siekmann, George H.; Woods, John. - Elsevier , 2014. - ISBN 978-0-08-093067-1 .

Länkar

• Andrews, Peter B, Church's Type Theory i Stanford Encyclopedia of Philosophy .
• Miller, Dale, 1991, " Logic: Higher-order " , Encyclopedia of Artificial Intelligence , 2nd ed.
• Herbert B. Enderton, andra ordningens och högre ordningens logik i Stanford Encyclopedia of Philosophy , publicerad 20 december 2007; väsentligt reviderad 4 mars 2009.