Modalny towarzysz

W logice modalny towarzysz superintuicjonistycznej ( pośredniej) logiki L jest normalną logiką modalną , która interpretuje L za pomocą pewnego kanonicznego tłumaczenia, opisanego poniżej. Towarzysze modalne mają różne właściwości oryginalnej logiki pośredniej , co umożliwia badanie logiki pośredniej za pomocą narzędzi opracowanych dla logiki modalnej.

Tłumaczenie Gödla – McKinseya – Tarskiego

Niech A będzie zdaniową formułą intuicjonistyczną . Formuła modalna T ( A ) jest zdefiniowana przez indukcję ze względu na złożoność A :

${\ Displaystyle T (p) = \ Box p,}$ dla dowolnej zmiennej zdaniowej ${\ Displaystyle p}$ ,

${\ Displaystyle T (\ bot) = \ bot ,}$

${\ Displaystyle T (A \ ziemia B) = T (A) \ ziemia T (B),}$

${\ Displaystyle T (A \ lor B) = T (A) \ lor T (B)}$

${\ Displaystyle T (A \ do B) = \ Box (T (A) \ do T (B)).}$

Ponieważ negacja jest w logice intuicjonistycznej zdefiniowana przez , mamy również ${\ Displaystyle A \ do \ bot}$

${\ Displaystyle T (\ neg A) = \ Box \ neg T (A).}$

T nazywa się tłumaczeniem Gödla lub tłumaczeniem Gödel – McKinsey – Tarski . Tłumaczenie jest czasami przedstawiane w nieco inny sposób: na przykład przed każdą podformułą $można$ wstawić Wszystkie takie warianty są równoważne w sposób dający się udowodnić w S4 .

Modalni towarzysze

Dla dowolnej normalnej logiki modalnej M , która rozciąga się na S4 , definiujemy jej si-fragment ρM jako

${\ Displaystyle \ rho M = \ {A \ mid M \ vdash T (A) \}.}$

Si-fragment dowolnego normalnego rozszerzenia S4 jest logiką superintuicjonistyczną. Logika modalna M jest modalnym towarzyszem logiki superintuicjonistycznej L , jeśli ${\ Displaystyle L = \ rho M}$ .

Każda logika superintuicjonistyczna ma towarzyszy modalnych. Najmniejszym modalnym towarzyszem L jest

${\ Displaystyle \ tau L = \ mathbf {S4} \ oplus \ {T (A) \ mid L \ vdash A \}}$

gdzie $oznacza$ normalne zamknięcie Można pokazać, że każda logika superintuicjonistyczna ma również największego towarzysza modalnego , który jest oznaczony przez σL . Logika modalna M jest towarzyszem L wtedy i tylko wtedy, gdy ${\ Displaystyle \ tau L \ subseteq M \ subseteq \ sigma L}$ .

Na przykład sam S4 jest najmniejszym modalnym towarzyszem logiki intuicjonistycznej ( IPC ). Największym modalnym towarzyszem IPC jest logika Grzegorczyka Grz , aksjomatyzowana aksjomatem

${\ Displaystyle \ Box (\ Box (A \ do \ Box A) \ do A) \ do A}$

nad K. _ Najmniejszym modalnym towarzyszem logiki klasycznej ( CPC ) jest S5 Lewisa , podczas gdy jego największym towarzyszem modalnym jest logika

${\ Displaystyle \ mathbf {Triv} = \ mathbf {K} \ oplus (A \ strzałka w lewo \ Pole A).}$

Więcej przykładów:

Ł	τL	σL	inni towarzysze L
IPC	S4	Grz	S4.1 , Dum , ...
KC	S4.2	Grz.2	S4.1.2 , ...
LC	S4.3	grz.3	S4.1.3 , S4.3Dum , ...
CPC	S5	Triv	patrz poniżej

Izomorfizm Bloka-Esakii

Zbiór rozszerzeń logiki superintuicjonistycznej L uporządkowany przez inkluzje tworzy kompletną siatkę , oznaczoną Ext L. Podobnie zbiór normalnych rozszerzeń logiki modalnej M jest kompletną kratą NExt M . Operatory towarzyszące ρM , τL i σL można uznać za odwzorowania między sieciami Ext IPC i NExt S4 :

${\ Displaystyle \ rho \ dwukropek \ operatorname {NExt} \, \ mathbf {S4} \ do \ operatorname {Ext} \, \ mathbf {IPC}, }$

${\ Displaystyle \ tau, \ sigma \ dwukropek \ operatorname {Ext} \, \ mathbf {IPC} \ do \ operatorname {NExt} \, \ mathbf {S4}.}$

Łatwo zauważyć, $na$ są i jest Ext IPC L. Maksimova i V. Rybakov wykazali, że ρ , τ i σ są w rzeczywistości odpowiednio kompletnymi homomorfizmami sieci , łącząco-zupełne i spełniające-zupełne. Kamieniem węgielnym teorii towarzyszy modalnych jest twierdzenie Bloka-Esakii , udowodnione niezależnie przez Wima Bloka i Leo Esakię. W Stanach

Odwzorowania ρ i σ są odwrotnymi izomorfizmami sieciowymi Ext wzajemnie IPC i NExt Grz .

Odpowiednio, σ i ograniczenie ρ do NExt Grz nazywane są izomorfizmem Blok-Esakia . Ważnym następstwem twierdzenia Bloka-Esakii jest prosty opis składniowy największych towarzyszy modalnych: dla każdej logiki superintuicjonistycznej L ,

${\ Displaystyle \ sigma L = \ tau L \ oplus \ mathbf {Grz}.}$

Opis semantyczny

Tłumaczenie Gödla ma odpowiednik oparty na teorii ram. Niech ${\ Displaystyle \ mathbf {F} = \ langle F, R, V \ rangle}$ będzie ogólną ramą modalną przechodnią i zwrotną . Preorder R indukuje relację równoważności

${\ Displaystyle x \ sim y \ iff x \, R \, y \ ziemia y \, R \, x}$

na F , który identyfikuje punkty należące do tego samego klastra. Niech $, R \ rangle / {\ sim}}$ , \ równoważnik \ rangle = \ langle F , ρF jest zbiorem klas równoważności $umieścić$ i

${\ Displaystyle \ rho V = \ {A / {\ sim} \ mid A \ in V, A = \ Box A \}.}$

Wtedy $, \ równoważnik, \ rho V \ rangle} jest intuicjonistyczną ramą ogólną$ F , zwaną szkieletem F . Istotą konstrukcji szkieletu jest to, że zachowuje ważność translacji modulo Gödla: dla dowolnej intuicjonistycznej formuły A ,

A jest ważne w ρ F wtedy i tylko wtedy, gdy T ( A ) jest ważne w F .

Dlatego si-fragment logiki modalnej M można zdefiniować semantycznie: jeśli M jest zupełny w odniesieniu do klasy C przechodnich zwrotnych ram ogólnych, to ρM jest zupełny w odniesieniu do klasy ${\ Displaystyle \ {\ rho \ mathbf {F}; \ \ mathbf {F} \ w C \}}$ .

Najwięksi modalni towarzysze mają również opis semantyczny. Dla dowolnej intuicjonistycznej ramy ogólnej $przecięcie$ V boolowskimi ( dopełnienie ). Można wykazać, że σ V jest domknięty pod ${\ displaystyle \ Box}$ , a zatem ${\ Displaystyle \ sigma \ mathbf {F} = \ langle F, \ równoważnik, \ sigma V \ rangle}$ jest ogólną ramką modalną. Szkielet σ F jest izomorficzny z F . Jeśli L jest logiką superintuicjonistyczną zupełną względem klasy C układów ogólnych, to jej największy towarzysz modalny σL jest zupełny względem ${\ Displaystyle \ {\ sigma \ mathbf {F}; \ \ mathbf {F} \ w C \}}$ .

Szkielet ramy Kripkego sam jest ramą Kripkego. Z drugiej strony, σ F nigdy nie jest układem Kripkego, jeśli F jest układem Kripkego o nieskończonej głębokości.

Twierdzenia o zachowaniu

Wartość towarzyszy modalnych i twierdzenia Bloka-Esakii jako narzędzia do badania logik pośrednich wynika z faktu, że wiele interesujących właściwości logiki jest zachowanych przez niektóre lub wszystkie odwzorowania ρ , σ i τ . Na przykład,

• rozstrzygalność jest zachowana przez ρ , τ i σ ,
• skończona właściwość modelu jest zachowana przez ρ , τ i σ ,
• tabularność jest zachowana przez ρ i σ ,
• Kompletność Kripkego jest zachowana przez ρ i τ ,
• pierwszego rzędu na ramkach Kripkego jest zachowana przez ρ i τ .

Inne właściwości

Każda logika pośrednia $L$ ma nieskończoną liczbę towarzyszy, a ponadto zbiór modalnych towarzyszy malejący Na przykład ${\ Displaystyle \ rho ^ {- 1} (\ mathbf {CPC} )}$ składa się z S5 i logiki $n$ każdej dodatniej liczby całkowitej $,$ gdzie klastrem n - . Zbiór modalnych towarzyszy dowolnego L jest albo przeliczalny , albo ma liczność kontinuum . Rybakov wykazał, że sieć Ext L może być osadzona w . ${\ Displaystyle \ rho ^ {- 1} (L)}$ ; w szczególności logika ma kontinuum towarzyszy modalnych, jeśli ma kontinuum rozszerzeń (dotyczy to na przykład wszystkich logik pośrednich poniżej KC ). Nie wiadomo, czy odwrotność jest również prawdziwa.

Tłumaczenie Gödla można zastosować zarówno do reguł , jak i formuł: tłumaczenie reguły

${\ Displaystyle R = {\ Frac {A_ {1}, \ kropki, A_ {n}} {B}}}$

jest regułą

${\ Displaystyle T (R) = {\ Frac {T (A_ {1}), \ kropki, T (A_ {n})} {T (B)}}.}$

Reguła R jest dopuszczalna w logice L , jeśli zbiór twierdzeń L jest domknięty pod R . Łatwo zauważyć, że R jest dopuszczalne w superintuicjonistycznej logice L , ilekroć T ( R ) jest dopuszczalne w modalnym towarzyszu L. Odwrotność nie jest generalnie prawdziwa, ale dotyczy największego modalnego towarzysza L .

• Alexander Chagrov i Michael Zakharyaschev, Logika modalna , tom. 35 Oxford Logic Guides, Oxford University Press, 1997.
• Vladimir V. Rybakov, Dopuszczalność reguł wnioskowania logicznego , tom. 136 Studiów nad logiką i podstawami matematyki, Elsevier, 1997.