Højere ordens logik

Højere-ordens logik i matematik og logik er en form for prædikatlogik, der adskiller sig fra førsteordenslogik i yderligere prædikater over prædikater, kvantificerere over dem og følgelig rigere semantik . Højere ordens logikker med deres standardsemantik er mere udtryksfulde, men deres modelteoretiske egenskaber er meget sværere at studere og anvende sammenlignet med førsteordenslogik.

Førsteordens logik kvantificerer kun variable; andenordens logik tillader også kvantificering af prædikater og funktionssymboler (oversæt); tredjeordens logik bruger og kvantificerer prædikater over prædikater (sæt af sæt) og så videre. For eksempel en anden ordens sætning

udtrykker princippet om matematisk induktion . Højere-ordens logik inkluderer alle lavere-ordens logikker; med andre ord tillader logik af højere orden udsagn med prædikater (oversæt) med lavere rededybde.

Eksempler og egenskaber

Højere ordens logik omfatter udløbere af Kirkens simple typeteori [1] og forskellige former for intuitionistisk typeteori. Gerard Huet viste, at foreningsproblemet er algoritmisk uløseligt i den intuitionistiske variation af tredjeordens logik [2] [3] [4] , det vil sige, at der ikke er nogen algoritme, der vil afgøre, om en vilkårlig ligning har en løsning frem for tredjeordens logik vilkår (og endnu mere ved vilkår vilkårlig rækkefølge over den tredje).

Under hensyntagen til begrebet isomorfisme er den boolske operation defineret i andenordens logik. Ved hjælp af denne observation fastslog Hintikka i 1955, at højereordens logik kan repræsenteres af andenordenslogik i den forstand, at man for hver formel af højereordenslogik kan finde en tilsvarende lige gyldig andenordenslogikformel [5] .

I nogle sammenhænge antages begrebet højere ordens logik at henvise til klassisk højere ordens logik. Imidlertid er højere-ordens modal logik også blevet undersøgt. Ifølge nogle logikere studeres Gödels ontologiske bevis (ud fra et teknisk synspunkt) i denne sammenhæng ] .

Se også

• Første ordens logik
• Anden ordens logik
• Højere grammatik
• Intuitionistisk typeteori
• Multi-sorteret logik
• Indtastet lambdaregning
• modal logik

Noter

1. ↑ Church, Alonzo , En formulering af den simple teori om typer Arkiveret 15. november 2018 på Wayback Machine , The Journal of Symbolic Logic 5(2):56–68 (1940)
2. ↑ Huet, Gérard P.  Unification of Unification in Third Order Logic  // Information og kontrol : journal. - 1973. - Bd. 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 senere // Proceedings, 15th International Conference TPHOL  (engelsk) / Carreño, V.; Muñoz, C.; Tahar, S. - Springer, 2002. - Vol. 2410. - S. 3-12. — (LNCS).
5. ↑ Stanford Encyclopedia of Philosophy artikel om Higher Order Logic . Hentet 9. august 2016. Arkiveret fra originalen 17. juni 2016. (ubestemt)
6. ↑ Passende, MelvinTyper, Tableauer og Gödels Gud. - Springer Science & Business Media , 2002. - S. 139. - ISBN 978-1-4020-0604-3 . . — “Godels argument er modalt og i det mindste anden orden, da der i hans definition af Gud er en eksplicit kvantificering over egenskaber. [...] [AG96] viste, at man kunne se en del af argumentet ikke som andenordens, men som tredjeordens."

Litteratur

• Andrews, Peter B. (2002). An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof , 2. udgave, 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. og Scott, PJ, 1986. Introduction to Higher Order Categorical Logic , Cambridge University Press, ISBN 0-521-35653-9
• Jacobs, Bart. Kategorisk logik og typeteori . - Nordholland, Elsevier, 1999. - (Studies 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, bind 9: Computational Logic  (engelsk) / Gabbay, Dov M.; Siekmann, George H.; Woods, John. - Elsevier , 2014. - ISBN 978-0-08-093067-1 .

Links

• Andrews, Peter B, Church's Type Theory i Stanford Encyclopedia of Philosophy .
• Miller, Dale, 1991, " Logic: Higher-order " , Encyclopedia of Artificial Intelligence , 2. udg.
• Herbert B. Enderton, Second-order and Higher-order Logic in Stanford Encyclopedia of Philosophy , udgivet 20. december 2007; væsentligt revideret 4. marts 2009.