Logika wyższego rzędu - Higher-order logic

W matematycznych i logicznych , A logiczny wyższego rzędu jest formą bazowego logiki , który różni się od logicznego pierwszego rzędu dodatkowymi kwantyfikatorów , a czasami silniejsze semantyki . Logiki wyższego rzędu ze swoją standardową semantyką są bardziej wyraziste, ale ich właściwości teoretyczne modelu są gorzej zachowane niż logiki pierwszego rzędu.

Termin „logika wyższego rzędu”, w skrócie HOL , jest powszechnie używany na oznaczenie prostej logiki predykatów wyższego rzędu . Tutaj „prosty” wskazuje, że podstawową teorią typów jest teoria typów prostych , zwana także prostą teorią typów (patrz teoria typów ). Leon Chwistek i Frank P. Ramsey zaproponowali to jako uproszczenie skomplikowanej i niezdarnej rozgałęzionej teorii typów określonej w Principia Mathematica przez Alfreda North Whiteheada i Bertranda Russella . Typy proste są obecnie czasami przeznaczone do wykluczenia typów polimorficznych i zależnych .

Zakres kwantyfikacji

Logika pierwszego rzędu określa ilościowo tylko zmienne, których zakres obejmuje osoby; dodatkowo logika drugiego rzędu również kwantyfikuje zbiory; logika trzeciego rzędu również kwantyfikuje zbiory zbiorów i tak dalej.

Logika wyższego rzędu jest sumą logiki pierwszego, drugiego, trzeciego, ..., n -tego rzędu; tj. logika wyższego rzędu dopuszcza kwantyfikację na zbiorach zagnieżdżonych arbitralnie głęboko.

Semantyka

Istnieją dwie możliwe semantyki dla logiki wyższego rzędu.

W semantyce standardowej lub pełnej kwantyfikatory obiektów wyższego typu obejmują wszystkie możliwe obiekty tego typu. Na przykład kwantyfikator zbiorów indywiduów obejmuje cały zbiór potęg zbioru indywiduów. Tak więc w standardowej semantyce, po określeniu zbioru indywiduów, wystarczy określić wszystkie kwantyfikatory. HOL ze standardową semantyką jest bardziej wyrazisty niż logika pierwszego rzędu. Na przykład HOL dopuszcza kategoryczne aksjomatyzacje liczb naturalnych i liczb rzeczywistych , które są niemożliwe w logice pierwszego rzędu. Jednak w wyniku Kurta Gödla , HOL ze standardową semantyką nie dopuszcza skutecznego , solidnego i kompletnego rachunku dowodowego . Teoretyczne właściwości modelu HOL ze standardową semantyką są również bardziej złożone niż właściwości logiki pierwszego rzędu. Na przykład, liczba Löwenheim z logiką drugiego rzędu jest już większa niż pierwsza liczba mierzalna , jeżeli taki istnieje Cardinal. Natomiast liczba Löwenheima logiki pierwszego rzędu wynosi order ₀ , najmniejszy nieskończony kardynał.

W semantyce Henkina oddzielna domena jest zawarta w każdej interpretacji dla każdego typu wyższego rzędu. Tak więc, na przykład, kwantyfikatory nad zestawy jednostek może wahać się tylko podzbiór PowerSet zbioru jednostek. HOL z tą semantyką jest odpowiednikiem logiki pierwszego rzędu z wieloma sortowaniami , a nie jest silniejsza niż logika pierwszego rzędu. W szczególności, HOL z semantyką Henkina ma wszystkie teorie modelowe właściwości logiki pierwszego rzędu i ma kompletny, solidny, skuteczny system dowodzenia odziedziczony z logiki pierwszego rzędu.

Przykłady i właściwości

Wyższe logiki Zamówienie obejmuje odgałęzienia Church „s prostej teorii typów i różnych form intuicjonistycznej teorii typów . Gérard Huet wykazał, że jednorodność jest nierozstrzygalna w teorii typów logiki trzeciego rzędu, to znaczy, że nie może istnieć żaden algorytm decydujący o tym, czy arbitralne równanie między terminami trzeciego rzędu (nie mówiąc już o arbitralnych wyższego rzędu) ma rozwiązanie .

Aż do pewnego pojęcia izomorfizmu, operacja poweret jest definiowalna w logice drugiego rzędu. Korzystając z tej obserwacji, Jaakko Hintikka ustalił w 1955 r., Że logika drugiego rzędu może symulować logikę wyższego rzędu w tym sensie, że dla każdej formuły logiki wyższego rzędu można znaleźć równoważny wzór w logice drugiego rzędu.

W pewnym kontekście zakłada się, że termin „logika wyższego rzędu” odnosi się do klasycznej logiki wyższego rzędu. Jednak zbadano również modalną logikę wyższego rzędu. Według kilku logików dowód ontologiczny Gödla najlepiej jest badać (z technicznego punktu widzenia) w takim kontekście.

Zobacz też

• Logika pierwszego rzędu
• Logika drugiego rzędu
• Teoria typów
• Gramatyka wyższego rzędu
• Programowanie logiczne wyższego rzędu
• HOL (asystent dowód)
• Wielokrotnie posortowana logika
• Wpisany rachunek lambda
• Logika modalna

Uwagi

Bibliografia

• 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, „Fundamenty bez fundamentalizmu: przypadek logiki drugiego rzędu”. Oxford University Press., ISBN   0-19-825029-0
• Stewart Shapiro , 2001, „Classical Logic II: Higher Order Logic”, w: Lou Goble, red., The Blackwell Guide to Philosophical Logic . Blackwell, ISBN   0-631-20693-0
• Lambek, J. and Scott, PJ, 1986. Wprowadzenie do logiki kategorialnej wyższego rzędu , Cambridge University Press, ISBN   0-521-35653-9
• Jacobs, Bart (1999). Logika kategorialna i teoria typów . Studies in Logic and the Foundations of Mathematics 141. North Holland, Elsevier. ISBN   0-444-50170-3 .
• Benzmüller, Christoph; Miller, Dale (2014). „Automatyzacja logiki wyższego rzędu”. W Gabbay, Dov M .; Siekmann, Jörg H .; Woods, John (red.). Podręcznik historii logiki, tom 9: Logika obliczeniowa . Elsevier. ISBN   978-0-08-093067-1 .

Linki zewnętrzne

• Andrews, Peter B, Church's Type Theory w Stanford Encyclopedia of Philosophy .
• Miller, Dale, 1991, „ Logic: Higher-order ”, Encyklopedia sztucznej inteligencji , wyd.
• Herbert B. Enderton, Logika drugiego rzędu i wyższego rzędu w Stanford Encyclopedia of Philosophy , opublikowana 20 grudnia 2007; rewizja merytoryczna 04.03.2009.