Logika funktorów predykatów

W logice matematycznej logika funktorów predykatów ( PFL ) jest jednym z kilku sposobów wyrażania logiki pierwszego rzędu (znanej również jako logika predykatów ) za pomocą środków czysto algebraicznych, tj. bez zmiennych ilościowych . PFL wykorzystuje niewielką liczbę urządzeń algebraicznych zwanych funktorami predykatów (lub modyfikatorami predykatów ), które działają na terminach w celu uzyskania terminów. PFL jest w większości wynalazkiem logika i filozofa Willarda Quine’a .

Motywacja

Źródłem tej sekcji, a także większości tego wpisu, jest Quine (1976). Quine zaproponował PFL jako sposób algebraizacji logiki pierwszego rzędu w sposób analogiczny do tego, jak algebra Boole'a algebraizuje logikę zdań . Zaprojektował PFL tak, aby miał dokładnie taką ekspresyjną moc logiki pierwszego rzędu z tożsamością . Stąd metamatematyka PFL jest dokładnie taka, jak w logice pierwszego rzędu bez interpretowanych liter predykatów: obie logiki są rozsądne , kompletne i nierozstrzygalne . Większość prac Quine’a na temat logiki i matematyki opublikowanych w ciągu ostatnich 30 lat jego życia w jakiś sposób nawiązywała do PFL.

Quine wziął „funktor” z pism swojego przyjaciela Rudolfa Carnapa , który jako pierwszy zastosował go w filozofii i logice matematycznej , i zdefiniował go w następujący sposób:

„Słowo funktor , gramatyczne w imporcie, ale logiczne w środowisku… to znak, który łączy się z jednym lub większą liczbą wyrażeń danego rodzaju gramatycznego, aby wytworzyć wyrażenie danego rodzaju gramatycznego”. (Quine 1982: 129)

Inne niż PFL sposoby algebraizacji logiki pierwszego rzędu obejmują:

• Algebra cylindryczna Alfreda Tarskiego i jego amerykańskich uczniów. Uproszczona algebra cylindryczna zaproponowana przez Bernaysa (1959) skłoniła Quine'a do napisania artykułu zawierającego pierwsze użycie wyrażenia „funktor predykatu”;
• Algebra poliadyczna Paula Halmosa . Ze względu na ekonomiczne prymitywy i aksjomaty ta algebra najbardziej przypomina PFL;
• Algebra relacji algebraizuje fragment logiki pierwszego rzędu składający się ze wzorów nie mających wzoru atomowego mieszczącego się w zakresie więcej niż trzech kwantyfikatorów . Fragment ten jednak wystarczy dla arytmetyki Peano i aksjomatycznej teorii mnogości ZFC ; stąd algebra relacji, w przeciwieństwie do PFL, jest niekompletna . Większość prac nad algebrą relacji od około 1920 roku została wykonana przez Tarskiego i jego amerykańskich uczniów. Siła algebry relacji ujawniła się dopiero w monografii Tarski i Givant (1987), opublikowanej po trzech ważnych artykułach dotyczących PFL, a mianowicie Bacon (1985), Kuhn (1983) i Quine (1976);
• Logika kombinatoryczna opiera się na kombinatorach , funkcjach wyższego rzędu, których dziedziną jest inny kombinator lub funkcja i których zakres jest jeszcze innym kombinatorem. Stąd logika kombinatoryczna wykracza poza logikę pierwszego rzędu, mając ekspresyjną moc teorii mnogości , co czyni logikę kombinacyjną podatną na paradoksy . Z drugiej strony, funktor predykatu po prostu odwzorowuje predykaty (zwane także terminami ) na predykaty.

PFL jest prawdopodobnie najprostszym z tych formalizmów, a jednocześnie tym, o którym napisano najmniej.

Quine przez całe życie fascynował się logiką kombinatoryczną , czego dowodem jest jego wprowadzenie do tłumaczenia w Van Heijenoort (1967) artykułu rosyjskiego logika Mosesa Schönfinkela , założyciela logiki kombinatorycznej. Kiedy Quine na poważnie zaczął pracować nad PFL w 1959 roku, logikę kombinacyjną powszechnie uznawano za porażkę z następujących powodów:

• Dopóki Dana Scott nie zaczął pisać o modelowej teorii logiki kombinatorycznej pod koniec lat sześćdziesiątych XX wieku, nad tą logiką pracowali prawie tylko Haskell Curry , jego uczniowie i Robert Feys w Belgii;
• Zadowalające aksjomatyczne sformułowania logiki kombinatorycznej pojawiały się powoli. W latach trzydziestych XX wieku stwierdzono, że niektóre sformułowania logiki kombinatorycznej są niespójne . Curry odkrył także paradoks Curry'ego , charakterystyczny dla logiki kombinatorycznej;
• Rachunek lambda , mający tę samą moc wyrazu co logika kombinatoryczna , był postrzegany jako wyższy formalizm.

Formalizacja Kuhna

Składnia , elementy podstawowe i aksjomaty języka PFL opisane w tej sekcji są w dużej mierze autorstwa Stevena Kuhna (1983). Semantyka funktorów została opisana przez Quine'a (1982) . Pozostała część tego wpisu zawiera terminologię zaczerpniętą z Bacona (1985).

Składnia

Termin atomowy to wielka litera łacińska, z wyjątkiem I i S , po której następuje numeryczny indeks górny zwany stopniem lub połączone zmienne małymi literami, zwane zbiorczo listą argumentów . Stopień terminu przekazuje tę samą informację, co liczba zmiennych następujących po literze orzeczenia. Termin atomowy stopnia 0 oznacza zmienną logiczną lub wartość logiczną . Stopień I wynosi niezmiennie 2 i dlatego nie jest wskazany.

Funktory predykatu „kombinatywne” (słowo to Quine’a), wszystkie monadyczne i charakterystyczne dla PFL, to Inv , inv , ∃ , + i p . Termin jest terminem atomowym lub skonstruowanym na podstawie poniższej reguły rekurencyjnej. Jeśli τ jest terminem, to Inv τ, inv τ, ∃ τ, + τ i p τ są terminami. Funktor z indeksem górnym n , n liczbą naturalną > 1, oznacza n kolejne zastosowania (iteracje) tego funktora.

Formuła jest albo terminem, albo jest zdefiniowana przez regułę rekurencyjną: jeśli α i β są formułami, to αβ i ~(α) są również formułami. Stąd „~” jest kolejnym funktorem monadycznym, a konkatenacja jest jedynym diadycznym funktorem predykatu. Quine nazwał te funktory „aletycznymi”. Naturalną interpretacją „~” jest negacja ; konkatenacją jest dowolny łącznik , który w połączeniu z negacją tworzy funkcjonalnie kompletny zestaw spójników. Preferowanym przez Quine'a funkcjonalnie kompletnym zestawem była koniunkcja i negacja . Zatem terminy połączone uważa się za połączone. Oznaczenie + to zapis Bacona (1985); cała inna notacja pochodzi od Quine'a (1976; 1982). Część aletyczna PFL jest identyczna ze schematami terminów boolowskich Quine’a (1982).

Jak dobrze wiadomo, dwa funktory aletyczne można zastąpić pojedynczym funktorem diadycznym o następującej składni i semantyce : jeśli α i β są formułami, to (αβ) jest formułą, której semantyka „nie jest (α i/lub β) (patrz NAND i NOR ).

Aksjomaty i semantyka

Quine nie przedstawił ani aksjomatyzacji, ani procedury dowodowej dla PFL. Następująca aksjomatyzacja PFL, jedna z dwóch zaproponowanych przez Kuhna (1983), jest zwięzła i łatwa do opisania, ale w szerokim zakresie wykorzystuje zmienne wolne , a zatem nie oddaje w pełni ducha PFL. Kuhn podaje inną aksjomatyzację, w której nie stosuje się zmiennych wolnych, ale jest ona trudniejsza do opisania i w szerokim zakresie wykorzystuje określone funktory. Kuhn udowodnił, że obie jego aksjomatyzacje PFL są prawidłowe i kompletne .

Ta sekcja jest zbudowana wokół prymitywnych funktorów predykatów i kilku zdefiniowanych. Funktory aletyczne można aksjomatyzować za pomocą dowolnego zestawu aksjomatów logiki zdaniowej , których prymitywami są negacja i jeden z ∧ lub ∨. Równoważnie wszystkie tautologie logiki zdaniowej można uznać za aksjomaty.

Semantyka Quine'a (1982) dla każdego funktora predykatu jest podana poniżej w formie abstrakcji (notacja konstruktora zbiorów), po której następuje odpowiedni aksjomat Kuhna (1983) lub definicja Quine'a (1976). Oznaczenie $_$ _ _ -krotki spełniające wzór atomowy ${\ Displaystyle Fx_ {1} \ cdots x_ {n}.}$

• Tożsamość , I , definiuje się jako:

${\ Displaystyle IFx_ {1} x_ {2} \ cdots x_ {n} \ leftrightarrow (Fx_ {1} x_ {1} \ cdots x_ {n} \ leftrightarrow Fx_ {2} x_ {2} \ cdots x_ {n} ){\tekst{.}}}$

Tożsamość jest zwrotna ( Ixx ), symetryczna ( Ixy → Iyx ), przechodnia ( ( Ixy ∧ Iyz ) → Ixz ) i podlega zasadzie podstawienia:

${\ Displaystyle (Fx_ {1} \ cdots x_ {n} \ land Ix_ {1} y) \rightarrow Fyx_ {2} \ cdots x_ {n}.} Dopełnienie, + dodaje zmienną$

• po lewej stronie dowolnej listy argumentów .

${\ Displaystyle \ + F ^ {n} \ {\ overset {\ underset {\ operatorname {def}} }} {=}} \ \ {x_ {0} x_ {1} \ cdots x_ {n}: F ^{n}x_{1}\cdots x_{n}\}.}$

$} \ leftrightarrow Fx_ {2} \ cdots x_ {n}.}$

• n Kadrowanie ∃ usuwa zmienną znajdującą się najbardziej po lewej stronie z dowolnej listy argumentów.

${\ Displaystyle \ istnieje F ^ {n} \ {\ overset {\ underset {\ operatorname {def}} }} {=}} \ \ {x_ {2} \ cdots x_ {n}: \ istnieje x_ {1 } F^{n}x_{1}\cdots x_{n}\}.}$

${\ Displaystyle Fx_ {1} \ cdots x_ {n} \rightarrow \ istnieje Fx_ {2} \ cdots x_ {n}.}$

Przycinanie umożliwia użycie dwóch przydatnych zdefiniowanych funktorów:

• Odbicie , S :

${\ Displaystyle SF ^ {n} \ {\ overset {\ underset {\ operatorname {def}} }} 2}x_{2}\cdots x_{n}\}.}$

${\ Displaystyle SF ^ {n} \ leftrightarrow \ istnieje JEŻELI ^ {n}.}$

S uogólnia pojęcie zwrotności na wszystkie terminy o dowolnym skończonym stopniu większym niż 2. Uwaga: S nie należy mylić z prymitywnym kombinatorem S logiki kombinatorycznej.

• Produkt kartezjański , ${\ displaystyle \ razy}$ ;

${\ Displaystyle F ^ {m} \ razy G ^ {n} \ leftrightarrow F ^ {m} \ istnieje ^ {m} G ^ {n}.}$

Tylko w tym przypadku Quine przyjął notację wrostkową, ponieważ ta notacja wrostkowa iloczynu kartezjańskiego jest bardzo dobrze ugruntowana w matematyce. Iloczyn kartezjański umożliwia przekształcenie koniunkcji w następujący sposób:

${\ Displaystyle F ^ {m} x_ {1} \ cdots x_ {m} G ^ {n} x_ {1} \ cdots x_ {n} \ leftrightarrow (F ^ {m} \ razy G ^ {n}) x_ {1}\cdots x_{m}x_{1}\cdots x_{n}.}$

Zmień kolejność połączonej listy argumentów, tak aby przesunąć parę zduplikowanych zmiennych maksymalnie w lewo, a następnie wywołaj S , aby wyeliminować duplikacje. Powtarzanie tej czynności tyle razy, ile potrzeba, skutkuje listą argumentów o długości max( m , n ).

Kolejne trzy funktory umożliwiają dowolną zmianę kolejności list argumentów.

• Inwersja główna Inv obraca zmienne na liście argumentów w prawo, tak że ostatnia zmienna staje się pierwszą .

${\ Displaystyle \ operatorname {Inv} F ^ {n} \ {\ overset {\ underset {\ operatorname {def}}} {n}x_{n}x_{1}\cdots x_{n-1}\}.}$

${\ Displaystyle \ operatorname {Inv} Fx_ {1} \ cdots x_ {n} \ leftrightarrow Fx_ {n} x_ {1} \ cdots x_ {n-1}.} Drobna inwersja, inv, zamienia$

• pierwsze dwie zmienne w lista argumentów.

${\ Displaystyle \ operatorname {inv} F ^ {n} \ {\ overset {\ underset {\ operatorname {def}}} {n}x_{2}x_{1}\cdots x_{n}\}.}$

${\ Displaystyle \ operatorname {inv} Fx_ {1} \ cdots x_ {n} \ leftrightarrow Fx_ {2} x_ {1} \ cdots x_ {n}.}$

• Permutacja , p , obraca zmienne od drugiej do ostatniej na liście argumentów w lewo, tak że druga zmienna staje się ostatnią.

${\ Displaystyle \ pF ^ {n} \ {\ overset {\ underset {\ operatorname {def}} }} {1}x_{3}\cdots x_{n}x_{2}\}.}$

${\ Displaystyle pFx_ {1} \ cdots x_ {n} \ leftrightarrow \ operatorname {Inv} \ operatorname {inv} Fx_ {1} x_ {3} \ cdots x_ {n} x_ {2}.}$

Mając listę argumentów składającą się z n zmiennych, p domyślnie traktuje ostatnie n -1 zmiennych jak łańcuch rowerowy, przy czym każda zmienna stanowi ogniwo w łańcuchu. Jedno zastosowanie p przesuwa łańcuch o jedno ogniwo. k kolejnych zastosowań p do F ⁿ przesuwa zmienną k +1 na pozycję drugiego argumentu w F .

Gdy n =2, Inv i inv po prostu zamieniają x ₁ i x ₂ . Gdy n = 1, nie mają one żadnego wpływu. Stąd p nie ma wpływu, gdy n < 3.

Kuhn (1983) uważa inwersję większą i inwersję małą za prymitywne. Zapis p w Kuhnie odpowiada inv ; nie ma analogii do permutacji i dlatego nie ma dla niej aksjomatów. Jeśli, podążając za Quine'em (1976), p przyjmiemy jako prymitywne, Inv i inv można zdefiniować jako nietrywialne kombinacje + , ∃ i iterowanego p .

W poniższej tabeli podsumowano wpływ funktorów na stopień ich argumentów.

Wyrażenie	Stopień
${\ displaystyle p; \ nazwa operatora {inv}; \ nazwa operatora {inv}; \ \ lnot; \ ja}$	bez zmiany
${\ Displaystyle + F ^ {n-1}; \ \ istnieje F ^ {n + 1}; \ SF ^ {n + 1}}$	N
${\ displaystyle \ alfa ^ {m} \ beta ^ {n}; \ F ^ {m} \ razy G ^ {n}}$	maks. ( m , n )

Zasady

Wszystkie przypadki litery orzeczenia można zastąpić inną literą orzeczenia tego samego stopnia, bez wpływu na ważność. Zasady następujące :

• modus ponens ;
• Niech α i β będą $.$ których nie występuje Następnie jeśli ${\ Displaystyle (\ alfa \ land Fx_ {1}... x_ {n}) \rightarrow \ beta}$ jest twierdzeniem PFL, to ${\ Displaystyle (\ alfa \ ziemia \ istnieje Fx_ {2}... x_ {n}) \rightarrow \ beta}$ jest również twierdzeniem PFL.

Kilka przydatnych wyników

Zamiast aksjomatyzować PFL, Quine (1976) zaproponował następujące przypuszczenia jako kandydujące aksjomaty.

${\ displaystyle \ istnieje ja}$

n −1 kolejnych iteracji p przywraca status quo ante :

${\ Displaystyle F ^ {n} \ leftrightarrow p ^ {n-1} F ^ {n}}$

+ i ∃ unicestwiają się nawzajem:

${\ Displaystyle {\ początek {przypadków} F ^ {n} \rightarrow +\istnieje F^{n} \\F^{n} \leftrightarrow \istnieje +F^{n}\end{cases}}}$

Negacja rozkłada się na + , ∃ i p :

${\ displaystyle {\ początek {przypadków} + \ lnot F ^ {n} \ leftrightarrow \ lnot + F^{n}\\\lnot \exists F^{n}\rightarrow \exists \lnot F^{n}\\p\lnot F^{n}\leftrightarrow \lnot pF^{n}\end{cases }}}$

+ i p rozkładają się na koniunkcję:

${\ Displaystyle {\ początek {przypadków} + (F ^ {n} G ^{m})\leftrightarrow (+F^{n}+G^{m})\\p(F^{n}G^{m})\leftrightarrow (pF^{n}pG^{m}) \end{przypadki}}}$

Tożsamość ma interesujące implikacje:

${\ Displaystyle IF ^ {n} \rightarrow p ^ {n-2} \ istnieje p + F ^ {n}}$

Quine wysunął również hipotezę: jeśli α jest twierdzeniem PFL, to twierdzeniem jest również pα , + α i ${\ displaystyle \ nie \ istnieje \ lnot \ alfa}$ .

Praca Bacona

Bacon (1985) przyjmuje warunek , negację , tożsamość , dopełnienie oraz inwersję większą i mniejszą jako prymitywną, a kadrowanie zgodnie z definicją. Stosując terminologię i notację różniącą się nieco od powyższej, Bacon (1985) przedstawia dwa sformułowania PFL:

• Naturalny preparat dedukcyjny w stylu Fredericka Fitcha. Bacon szczegółowo udowadnia, że ​​ta formuła jest solidna i kompletna .
• Sformułowanie aksjomatyczne, które Bacon twierdzi, ale którego nie udowadnia, jest równoważne z poprzednim. Niektóre z tych aksjomatów to po prostu przypuszczenia Quine'a powtórzone w notacji Bacona.

Bekon także:

• Omawia związek języka PFL z logiką terminów Sommersa (1982) i argumentuje, że przekształcenie języka PFL przy użyciu składni zaproponowanej w dodatku Lockwooda do Sommers powinno ułatwić „czytanie, używanie i nauczanie” języka PFL;
• Dotyka teoretycznej struktury grupowej Inv i inv ;
• Wspomina, że ​​logika zdaniowa , monadyczna logika predykatów , logika modalna S5 i logika boolowska (nie)permutowanych relacji są fragmentami PFL.

Od logiki pierwszego rzędu do PFL

Poniższy algorytm jest adaptacją Quine'a (1976: 300-2). Biorąc pod uwagę zamkniętą formułę logiki pierwszego rzędu , wykonaj najpierw następujące czynności:

• Dołącz numeryczny indeks dolny do każdej litery orzeczenia, podając jej stopień;
• Przetłumacz wszystkie kwantyfikatory uniwersalne na kwantyfikatory egzystencjalne i negację;
• Przekształć wszystkie formuły atomowe w postaci x = y jako Ixy .

Teraz zastosuj następujący algorytm do poprzedniego wyniku:

1. Przetłumacz macierze najgłębiej zagnieżdżonych kwantyfikatorów na rozłączną postać normalną , składającą się z alternatyw koniunkcji terminów , w razie potrzeby zanegowając terminy atomowe. Powstała podformuła zawiera jedynie negację, koniunkcję, alternatywę i kwantyfikację egzystencjalną.
2. Rozprowadź kwantyfikatory egzystencjalne po alternatywach macierzy, korzystając z reguły przejścia (Quine 1982: 119):

   ${\ Displaystyle \ istnieje x [\ alfa (x) \ lor \ gamma (x)] \ leftrightarrow (\ istnieje x \ alfa (x) \ lor \ istnieje x \ gamma (x)).}$

3. Zastąp koniunkcję iloczynem kartezjańskim , powołując się na fakt:
   ${\ Displaystyle (F ^ {m} \ kraina G ^ {n}) \ leftrightarrow (F ^ {m} \ razy G ^ {n}) \ leftrightarrow (F ^ {m} \ istnieje ^ {m} G ^ { n});m<n.}$
4. Połącz listy argumentów wszystkich terminów atomowych i przenieś połączoną listę na skrajną prawą stronę podformuły.
5. Użyj Inv i inv , aby przenieść wszystkie wystąpienia zmiennej ilościowej (nazwij ją y ) na lewo od listy argumentów.
6. Wywołaj S tyle razy, ile jest to konieczne, aby wyeliminować wszystkie oprócz ostatniego wystąpienia y . Wyeliminuj y , poprzedzając podformułę jednym wystąpieniem ∃ .
7. Powtarzaj (1)-(6), aż wszystkie zmienne ilościowe zostaną wyeliminowane. Wyeliminuj wszelkie alternatywy mieszczące
   ${\ Displaystyle (\ alfa \ lor \ beta \ lor ...) \ leftrightarrow \ lnot (\ lnot \ alfa \ ziemia \ lnot \ beta \ ziemia ...).}$
   w zakresie kwantyfikatora, odwołując się do równoważności

Odwrotne tłumaczenie z PFL na logikę pierwszego rzędu omawia Quine (1976: 302-4).

Kanonicznym fundamentem matematyki jest aksjomatyczna teoria mnogości , z logiką tła składającą się z logiki pierwszego rzędu z tożsamością , ze wszechświatem dyskursu składającym się wyłącznie ze zbiorów. Istnieje pojedyncza litera predykatu stopnia 2, interpretowana jako przynależność do zbioru. Tłumaczenie PFL kanonicznej aksjomatycznej teorii mnogości ZFC nie jest trudne, ponieważ żaden aksjomat ZFC nie wymaga więcej niż 6 zmiennych ilościowych.

Zobacz też

• Logika algebraiczna

Przypisy

• Bacon, John, 1985, „Kompletność logiki predykatu-funktora”, Journal of Symbolic Logic 50 : 903–26.
• Paul Bernays , 1959, „Uber eine naturliche Erweiterung des Relationenkalkuls” w: Heyting, A., red., Konstruktywizm w matematyce . Holandia Północna: 1–14.
• Kuhn, Steven T. , 1983, „ Aksjomatyzacja logiki funktorów predykatów ”, Notre Dame Journal of Formal Logic 24 : 233–41.
• Willard Quine , 1976, „Logika algebraiczna i funktory predykatów” w: Ways of Paradox and Other Essays , wyd. powiększone. Uniwersytet Harvarda Prasa: 283–307.
• Willard Quine, 1982. Metody logiki , wyd. 4. Uniwersytet Harvarda Naciskać. Rozdz. 45.
• Sommers, Fred, 1982. Logika języka naturalnego . Uniwersytet Oksfordzki Naciskać.
• Alfred Tarski i Givant, Steven, 1987. Formalizacja teorii mnogości bez zmiennych . AMS .
• Jean Van Heijenoort , 1967. Od Fregego do Gödla: książka źródłowa o logice matematycznej . Uniwersytet Harvarda Naciskać.

Linki zewnętrzne

• Wprowadzenie do logiki predykatów-funktorów (pobranie jednym kliknięciem, plik PS) autorstwa Matsa Dahllöfa (Wydział Lingwistyki Uniwersytetu w Uppsali)