Subštrukturálna Logika

Obsah:

Subštrukturálna Logika
Subštrukturálna Logika

Video: Subštrukturálna Logika

Video: Subštrukturálna Logika
Video: Марат Газизов. Применения Волн Эллиота и Уровней Фибо на форексе урок 3 2024, Marec
Anonim

Vstupná navigácia

  • Obsah vstupu
  • Bibliografia
  • Akademické nástroje
  • Náhľad priateľov PDF
  • Informácie o autorovi a citácii
  • Späť na začiatok

Subštrukturálna logika

Prvýkrát publikované Ut 4. júla 2000; podstatná revízia st 21. február 2018

Subštrukturálna logika je neklasická logika slabšia ako klasická logika, pozoruhodná absenciou štrukturálnych pravidiel prítomných v klasickej logike. Tieto logiky sú motivované úvahami z filozofie (relevantná logika), lingvistiky (Lambekov počet) a výpočtov (lineárna logika). Techniky zo subštruktúrnej logiky sú okrem toho užitočné pri štúdiu tradičnej logiky, ako je klasická a intuičná logika. Tento článok poskytuje stručný prehľad oblasti subštrukturálnej logiky. Pre podrobnejší úvod, doplnený teorémami, dôkazmi a príkladmi, môže čitateľ nahliadnuť do kníh a článkov v bibliografii.

  • 1. Zostatok
  • 2. Logika v rodine
  • 3. Dôkazové systémy
  • 4. Sémantika
  • Bibliografia
  • Akademické nástroje
  • Ďalšie internetové zdroje
  • Súvisiace záznamy

1. Zostatok

Logika je o logických dôsledkoch. Výsledkom je, že podmienka je v logike ústredným pojmom, pretože má úzke spojenie s logickými dôsledkami. Toto spojenie je úhľadne vyjadrené v reziduálnom stave (známeho tiež ako dedukčná veta):

[p, q / vdash r / text {iba vtedy, ak} p / vdash q / rightarrow r)

Hovorí, že (r) vyplýva z (p) spolu s (q) práve vtedy, keď (q / rightarrow r) vyplýva iba z (p). Platnosť prechodu z (q) na (r) (vzhľadom na (p)) sa zaznamenáva pod podmienkou (q / rightarrow r).

Táto súvislosť medzi podmieneným a dôsledkom sa nazýva rezidencia analogicky s prípadom v matematike. Zvážte súvislosť medzi sčítaním a odčítaním. (a + b = c) iba vtedy, ak (a = c - b). Výsledný (a) (čo je (c - b)) je zvyšok, čo zostane z (c), keď sa (b) odoberie. Ďalším menom pre toto spojenie je odpočetová veta.

Tam však súvislosť medzi dôsledkom a podmienenosťou obsahuje jeden ďalší faktor. Nielenže existuje turniket pre logické následky a podmienený, kódujúci dôsledok vo vnútri jazyka výrokov, existuje aj čiarka, ktorá označuje kombináciu priestorov. Čítali sme „(p, q / vdash r)“, pretože „(r) vyplýva z (p) spolu s (q)“. Kombinovať priestory znamená mať spôsob, ako ich spojiť. Ale ako ich môžeme vziať spolu? Ukazuje sa, že existujú rôzne spôsoby, ako to urobiť, a tak aj rôzne subštrukturálne logiky. Správanie kombinácií predpokladov sa mení v závislosti od správania podmienených. V tomto úvodu budeme uvažovať o niektorých príkladoch.

1.1 Oslabenie

Je to jedna vec pre (p), aby to bola pravda. Je ďalšou podmienkou, že podmienená (q / rightarrow p) je pravdivá. Napriek tomu, ak je '(rightarrow)' materiálne podmienené, (q / rightarrow p) vyplýva z (p). Z mnohých rôznych dôvodov by sme si mohli želať pochopiť, ako by podmienečný režim mohol fungovať, ak by k tomu nedošlo. Toto je spojené s správaním premise, ako to môže ukázať táto demonštrácia.

(cfrac {p / vdash p} { cfrac {p, q / vdash p} {p / vdash q / rightarrow p}})

Z axiomatického (p / vdash p) (všetko vyplýva zo samotného) odvodzujeme, že (p) vyplýva z (p) spolu s (q) a potom rezíduami (p / vdash q / rightarrow p). Ak chceme odmietnuť odvodenie z (p) do (q / rightarrow p), odmietneme reziduáciu alebo odmietneme axiómy identity na začiatku dôkazu, alebo odmietneme prvý krok dôkazu, Je poučné uvažovať o tom, čo je súčasťou tejto poslednej možnosti. Tu treba poprieť, že (p) vyplýva z (p, q). Všeobecne platí, že musíme zamietnuť inferenčné pravidlo, ktoré má túto formu:

(frac {X / vdash A} {X, Y / vdash A})

Toto sa nazýva pravidlo oslabenia. Pravidlo vychádza zo silnejšieho tvrdenia, že (A) vyplýva z (X) na možno slabší, to (A) vyplýva z (X) spolu s (Y).

Ľudia ponúkli rôzne dôvody na odmietnutie pravidla oslabenia v závislosti od interpretácie kombinácie dôsledkov a predpokladov. Jeden z prvých motivačných príkladov pochádza z obavy o relevantnosť. Ak je logika relevantná (ak chceme povedať, že (p) znamená (q) je pravdivá, znamená to, že aspoň to, že (q) skutočne závisí od (p)), potom čiarka nemusí neuspokojujúce oslabenie. Môžeme skutočne mať (A) z (X), bez (A) z (X, Y), pretože to nemusí byť tak, že (A) závisí od (X) a (Y) dohromady.

V relevantnej logike pravidlo oslabenia zlyhá aj na druhej strane, pretože chceme, aby bol tento argument tiež neplatný:

(cfrac {q / vdash q} { cfrac {p, q / vdash q} {p / vdash q / rightarrow q}})

Opäť platí, že (q) môže vyplývať z (q), ale to neznamená, že to vyplýva z (p) spolu s (q) za predpokladu, že „spolu s“je mienené v primerane silnom rozum. V relevantnej logike teda môže dôjsť k zlyhaniu dedukcie z ľubovoľného predpokladu na logickú pravdu, ako je (q / rightarrow q).

1.2 Commutativity

Ak je spôsob premisnej kombinácie komutatívny (ak niečo, čo vyplýva z (X, Y), tiež vyplýva z (Y, X)), môžeme uvažovať nasledovne s použitím iba axiómu identity a reziduácie:

(cfrac {p / rightarrow q / vdash p / rightarrow q} { cfrac {p / rightarrow q, p / vdash q} { cfrac {p, p / rightarrow q / vdash q} {p / vdash (p / rightarrow q) rightarrow q}}})

Ak neexistuje komutatívnosť premise, tento dôkaz nie je k dispozícii. Toto je ďalší jednoduchý príklad prepojenia medzi správaním kombinácií predpokladov a správaním odpočtov zahrňujúcich podmienené.

Existuje veľa druhov podmienených stavov, pre ktoré tento záver zlyhá. Ak má „(rightarrow)“modálnu silu (ak vyjadruje určitý druh obťažovania, v ktorom (p / rightarrow q) platí, keď sa vyskytnú všetky súvisiace okolnosti, za ktorých (p) platí, (q)) áno), a ak výraz „(vdash)“vyjadruje lokálny dôsledok ((p / vdash q) iba vtedy, ak existuje nejaký model a za každých okolností, za ktorých platí (p)) q)) zlyhá. Môže byť pravda, že Greg je logik ((p)) a je pravda, že Greg je logik znamená, že Greg je filozofom ((p / rightarrow q)) - v súvisiacich situáciách, v ktorých je Greg logikom, je to filozof), ale to neznamená, že Greg je filozof. (Existuje veľa okolností, za ktorých je implikácia ((p / rightarrow q)) pravdivá, ale (q) nie je.) Takže sme za okolností, že (p) je pravda, ale ((p / rightarrow q) rightarrow q) nie je. Argument je neplatný.

Tento príklad je možné tiež chápať z hľadiska správania kombinácií predpokladov. Keď hovoríme, že platí, že platí to, že platí to, že platí to, že platí to, že (X) a (A) platia (B). Ak sme po skutočnom zapletení A (rightarrow) B, potom chceme, aby (B) bolo pravdivé za akýchkoľvek (súvisiacich) okolností, za ktorých je pravda, (A). Takže, (X, A / vdash B) hovorí, že v každej možnosti, v ktorej (A) je pravda, platí aj (B). Tieto možnosti nemusia uspokojovať všetky (X). (V klasických teóriách zahrnutia sú možnosti, v ktorých všetko, čo sa v (X) považuje za potrebné, je pravdivé.)

Ak kombinácia predpokladov nie je komutatívna, potom môže rezidencia ísť dvoma spôsobmi. Okrem podmienky zvyšku, ktorá spôsobuje správanie (rightarrow), môžeme definovať novú šípku (leftarrow) takto:

[p, q / vdash r / text {ak a iba ak} q / vdash r / leftarrow p)

Pre šípku zľava doprava máme modus ponens v tomto smere:

[p / rightarrow q, p / vdash q)

V prípade šípky sprava doľava je možné preukázať modus ponens s priestormi v opačnom poradí:

[p, q / leftarrow p / vdash q)

Toto je charakteristika subštrukturálnej logiky. Keď venujeme pozornosť tomu, čo sa stane, keď nemáme úplný doplnok štrukturálnych pravidiel, otvoria sa nové možnosti. Pod tým, čo bolo predtým, odkrývame dva stavy (v intuičnej alebo klasickej logike).

V ďalšej časti uvidíme ďalší príklad motivujúcej nekomutatívnej premisovej kombinácie a tieto dva rôzne podmienky.

1.3 Združenie

Toto je ďalší spôsob, ako štrukturálne pravidlá ovplyvňujú dôkaz. Asociativita kombinácií predpokladov poskytuje tento dôkaz:

(cfrac {r / rightarrow p, r / vdash p / \ / p / rightarrow q, p / vdash q} { cfrac {p / rightarrow q, (r / rightarrow p, r) vdash q} { cfrac {(p / rightarrow q, r / rightarrow p), r / vdash q} { cfrac {p / rightarrow q, r / rightarrow p / vdash r / rightarrow q} {p / rightarrow q / vdash (r / rightarrow p) rightarrow (r / rightarrow q)}}}})

Tento dôkaz používa pravidlo strihu v najvyššom kroku. Myšlienka je, že závery možno kombinovať. Ak (X / vdash A) a (Y (A) vdash B) (kde (Y (A)) je štruktúra priestorov, ktorá môže zahŕňať (A) raz alebo viackrát), (Y (X) vdash B) je tiež štruktúra (kde (Y (X)) je štruktúra priestorov, kde tieto prípady (A) boli nahradené (X)). V tomto dôkaze nahradíme (p) v (p / rightarrow q, p / vdash q) za (r / rightarrow p, r) na základe platnosti (r / rightarrow p, r / vdash p).

1.4 Kontrakcia

Posledným dôležitým príkladom je pravidlo kontrakcie, ktoré určuje, ako môžu byť priestory znovu použité. Kontrakcia je rozhodujúca pre odvodenie (p / rightarrow q) od (p / rightarrow (p / rightarrow q))

(cfrac { matrix { cfrac {p / rightarrow (p / rightarrow q) vdash p / rightarrow (p / rightarrow q)} {p / rightarrow (p / rightarrow q), p / vdash p / rightarrow q } & / cfrac {p / rightarrow q / vdash p / rightarrow q} {p / rightarrow q, p / vdash q}}} { cfrac {(p / rightarrow (p / rightarrow q), p), p / vdash q} { cfrac {p / rightarrow (p / rightarrow q), p / vdash q} {p / rightarrow (p / rightarrow q) vdash p / rightarrow q}}})

Tieto rôzne príklady vám dávajú chuť na to, čo sa dá urobiť pomocou štrukturálnych pravidiel. Štrukturálne pravidlá ovplyvňujú nielen podmienené, ale majú tiež účinky na iné spojivá, ako sú spojovacie a disjunkčné (ako uvidíme ďalej) a negácie (Dunn 1993; Restall 2000).

1.5 Štruktúra napravo od turniketu

Od zavedenia Gentzenovho sekvenčného počtu (Gentzen 1935) sme vedeli, že rozdiel medzi klasickou logikou a intuicionálnou logikou možno chápať aj ako rozdiel štruktúrnych pravidiel. Namiesto toho, aby sme uvažovali o postupnosti formy (X / vdash A), v ktorej máme zbierku predkov a jediný dôsledok, je pre klasickú logiku užitočné zvážiť postupnosti formy

[X / vdash Y)

kde (X) a (Y) sú zbierky výpisov. Zamýšľaná interpretácia je, že zo všetkých (X) vyplýva, že niektoré z (Y). Inými slovami, nemôžeme získať všetky (X) a žiadne (Y).

Ak umožnímeme sekvenciu s viacerými dôsledkami a prevedieme pravidlá do tohto rozšíreného kontextu, dokážeme odvodiť klasické tautológie. Napríklad odvodenie

(cfrac {p / vdash p} { cfrac {p / vdash q, p} { vdash p / rightarrow q, p}})

ukazuje, že musí mať buď / (p / rightarrow q) alebo (p). Toto je klasicky platné (ak (p) zlyhá, (p) je nepravdivé a podmienky s falošnými predchodcami sú pravdivé), ale v intuicionálnej logike sú neplatné. Rozdiel medzi klasickou a intuicionálnou logikou sa teda dá formálne chápať ako rozdiel medzi druhmi povolených štrukturálnych pravidiel a druhmi štruktúr vhodných na použitie pri analýze logických dôsledkov.

2. Logika v rodine

V rodine subštrukturálnych logík existuje veľa rôznych formálnych systémov. Tieto logiky môžu byť motivované rôznymi spôsobmi.

2.1 Relevantná logika

Mnoho ľudí sa chcelo vyjadriť k logickej platnosti, ktorá venuje určitú pozornosť podmienkam relevantnosti. Ak platí (X, A / vdash B), potom (X) musí nejako súvisieť s (A). Kombinácia areálu je obmedzená nasledujúcim spôsobom. Možno máme (X / vdash A) bez toho, aby sme mali (X, Y / vdash A). Nový materiál (Y) nemusí byť pre odpočet relevantný. V 50-tych rokoch Moh (1950), Church (1951) a Ackermann (1956) uviedli, čo môže byť „relevantná“logika. Myšlienky boli vyvinuté prúdom pracovníkov sústredených okolo Andersona a Belnapa, ich študentov Dunn a Meyer a mnohých ďalších. Kánonickými referenciami pre túto oblasť sú Anderson, Belnap a Dunnova dvojzväzková Entailment (1975 a 1992). Ďalšie úvody nájdete v Read's Relevant Logic, Dunn and Restall's Relevance Logic (2002),a Maresova relevantná logika: filozofická interpretácia (2004).

2.2 Vedomie zdrojov

Toto nie je jediný spôsob, ako obmedziť kombináciu predpokladov. Girard (1987) predstavil lineárnu logiku ako model pre procesy a využitie zdrojov. Myšlienka odpočtu spočíva v tom, že sa musia použiť zdroje (takže premisová kombinácia spĺňa kritérium relevantnosti) a neobmedzuje sa donekonečna. Priestory nemožno (re) použiť. Mohol by som teda mať (X, X / vdash A), ktorý hovorí, že na získanie (A) môžem použiť (X) dvakrát. Možno by som nemal (X / vdash A), čo hovorí, že môžem použiť (X) raz na získanie (A). Užitočný úvod do lineárnej logiky je uvedený v prednáške Troelstra o lineárnej logike (1992). Existujú aj iné formálne logiky, v ktorých pravidlo kontrakcie (od (X, X / vdash A) do (X / vdash A)) chýba. Najznámejšie z nich sú Łukasiewiczova cenná logika. Bez tohto pravidla existuje trvalý záujem o logiku kvôli Curryho paradoxu (Curry 1977, Geach 1995; pozri tiež Restall 1994 in Other Internet Resources).

3. Objednávka

Nezávisle na jednej z týchto tradícií Joachim Lambek uvažoval o matematických modeloch jazyka a syntaxe (Lambek 1958, 1961). Myšlienka je taká, že kombinácia predpokladov zodpovedá zloženiu reťazcov alebo iných jazykových jednotiek. Obsah (X, X) sa tu líši od obsahu (X), ale (X, Y) sa navyše líši od Y, X. Počíta sa nielen počet použitých priestorov, ale aj ich poradie. Dobré úvody do Lambekovho počtu (nazývaného aj kategorizovaná gramatika) možno nájsť v knihách Moortgata (1988) a Morrilla (1994).

3. Dôkazové systémy

Už sme videli zlomok jedného spôsobu prezentácie subštrukturálnej logiky, pokiaľ ide o dôkazy. Použili sme podmienku reziduácie, ktorá sa dá chápať tak, že zahŕňa dve pravidlá pre podmienečné, jedno na zavedenie podmieneného stavu

(cfrac {X, A / vdash B} {X / vdash A / rightarrow B})

a ďalšie na jeho odstránenie.

(cfrac {X / vdash A / rightarrow B / \ / Y / vdash A} {X, Y / vdash B})

Pravidlá, ako sú tieto, sú základným kameňom prirodzeného systému odpočtov a tieto systémy sú k dispozícii pre širokú škálu subštruktúrnej logiky. Teóriu dôkazov však možno urobiť aj inými spôsobmi. Gentzenove systémy nefungujú zavádzaním a odstraňovaním spojív, ale ich zavádzaním vľavo aj vpravo od turniketu logických dôsledkov. Zachováme úvodné pravidlo vyššie a vylučovacie pravidlo nahradíme jedným, ktoré vľavo uvedie podmienku.

(cfrac {X / vdash A / \ / Y (B) vdash C} {Y (A / rightarrow B, X) vdash C})

Toto pravidlo je zložitejšie, ale má rovnaký účinok ako pravidlo eliminácie šípok: Hovorí, že ak (A) stačí (X) a (B) (v niektorých súvislostiach) (Y)) na preukázanie (C), potom môžete rovnako dobre použiť (A / rightarrow B) spolu s (X) (v tom istom kontexte (Y)) na preukázanie (C)), pretože (A / rightarrow B) spolu s (X) vám dáva (B).

Gentzenove systémy so svojimi úvodnými pravidlami vľavo a vpravo majú veľmi špeciálne vlastnosti, ktoré sú užitočné pri štúdiu logiky. Pretože spojivá sú vždy zavedené v korekcii (prečítané zhora nadol), dôkazy nikdy nestratia štruktúru. Ak sa konektivita neobjaví na konci dôkazu, vôbec sa neobjaví v doklade, pretože spojky nemožno vylúčiť.

V určitých subštrukturálnych logikách, ako je lineárna logika a Lambekov počet, a vo fragmente relevantnej logiky (mathbf {R}) bez prerušenia, sa dá Gentzenov systém ukázať, že logika je rozhodnuteľná, možno nájsť algoritmus na určenie, či je argument (X / vdash A) platný. Toto sa vykonáva hľadaním dôkazov o (X / vdash A) v Gentzenovom systéme. Pretože priestory tohto záveru nesmú obsahovať žiadny jazyk, ktorý nie je v tomto závere, a nemajú väčšiu zložitosť (v týchto systémoch), existuje iba obmedzený počet možných priestorov. Algoritmus môže skontrolovať, či tieto spĺňajú pravidlá systému, a pokračovať v hľadaní priestorov pre tieto, alebo pri ukončení axióma prestať. Týmto spôsobom je zabezpečená rozhodovateľnosť niektorých subštrukturálnych logík.

V tomto zmysle však nie sú rozhodujúce všetky subštrukturálne logiky. Najdôležitejšie je, že relevantná logika (mathbf {R}) nie je rozhodnuteľná. Čiastočne je to preto, že jej teória dôkazov je zložitejšia ako teória inej subštrukturálnej logiky. (mathbf {R}) sa líši od lineárnej logiky a Lambekovho počtu priamym zaobchádzaním s konjunkciou a disjunkciou. Spojenie a rozpojenie spĺňajú najmä pravidlo distribúcie:

[p / amp (q / vee r) vdash (p / amp q) vee (p / amp r))

Prirodzený dôkaz distribúcie v akomkoľvek dôkazovom systéme používa oslabenie aj kontrakciu, takže nie je k dispozícii v príslušnej logike (mathbf {R}), ktorá neobsahuje oslabenie. Výsledkom je, že teórie dôkazov pre (mathbf {R}) obsahujú distribúciu ako primitívne pravidlo, alebo obsahujú druhú formu premise (tzv. Extenzívnu kombináciu, na rozdiel od intenzívnej premise, ktorú sme videli), ktorá uspokojuje oslabenie a kontrakcie.

V posledných rokoch sa vykonalo veľa práce na teórii dôkazov klasickej logiky, inšpirovanej a informovanej výskumom subštrukturálnej logiky. Klasická logika má plný doplnok štrukturálnych pravidiel a historicky predchádzala novším systémom subštrukturálnej logiky. Pokiaľ však ide o pokus porozumieť hlbokej štruktúre klasických dôkazových systémov (a najmä keď dve derivácie, ktoré sa líšia nejakým povrchným syntaktickým spôsobom, sú skutočne odlišné spôsoby, ako reprezentovať jeden základný „dôkaz“), je poučné uvažovať o klasická logika vytvorená základnou subštrukturálnou logikou, v ktorej sa ako dodatky ukladajú zvláštne štrukturálne pravidlá. Najmäje zrejmé, že to, čo odlišuje klasický dôkaz od svojich súrodencov, je prítomnosť štrukturálnych pravidiel kontrakcie a oslabenia v ich úplnej všeobecnosti (pozri napríklad Bellin a kol. 2006 a tam citovanú literatúru).

4. Teória modelu

Zatiaľ čo príslušná logika (mathbf {R}) má kontrolný systém zložitejší ako subštruktúrna logika, ako je lineárna logika, ktorej chýba distribúcia (extenzívnej) konjunkcie cez disjunkciu, jej teória modelov je celkom jednoduchšia. Routley-Meyerov model pre príslušnú logiku (mathbf {R}) sa skladá zo súboru bodov (P) s trojmiestnym vzťahom (R) na (P). Podmienečné (A / rightarrow B) sa hodnotí vo svete nasledovne:

(A / rightarrow B) je pravda v (x) iba vtedy, ak pre každé (y) a (z) kde (Rxyz), ak (A) je v (y, B) je pravda na (z).

Argument je platný v modeli práve vtedy, keď v ktoromkoľvek okamihu, keď sú priestory pravdivé, platí aj záver. Argument (A / vdash B / rightarrow B) je neplatný, pretože môžeme mať bod (x), v ktorom (A) je pravda, ale v ktorom (B / rightarrow B) nie je. Môže sa stať, že (B / rightarrow B) nebude pravdivý v (x) jednoducho tým, že (Rxyz) kde (B) je pravdivý v (y), ale nie v (z).

Vzťah troch miest (R) pozorne sleduje správanie sa spôsobu premisnej kombinácie v teórii dôkazov pre subštrukturálnu logiku. Pre rôzne logiky môžu byť na (R) umiestnené rôzne podmienky. Napríklad, ak je premisová kombinácia komutatívna, umiestnime podmienku symetrie na (R) takto: (Rxyz) iba vtedy, ak (Ryxz). Ternárna vzťahová sémantika nám dáva skvelé prostriedky na modelovanie správania sa subštruktúrnej logiky. (Rozsah korešpondencie medzi teóriou dôkazov a algebrou substrukturálnej logiky a sémantikou je uvedený v Dunnovej práci na Gaggleovej teórii (1991) a je zhrnutý v Restallovom úvode do subštrukturálnej logiky (2000).)

Okrem toho, ak spojenie a disjunkcia vyhovujú distribučnej axióme spomenutej v predchádzajúcej časti, môžu sa modelovať tiež priamo: spojenie je pravdivé v bode práve vtedy, keď sú obe spojky v tomto bode pravdivé, a disjunkcia je pravdivá v čase, keď tam je aspoň jeden disjunkt. V prípade logiky, ako je lineárna logika, bez distribučnej axiómy, musí byť sémantika zložitejšia s inou klauzúrou pre disjunkciu, ktorá by zneplatnila odvodenie distribúcie.

Jedna vec je použiť sémantiku ako formálne zariadenie na modelovanie logiky. Ďalšou možnosťou je použitie sémantiky ako interpretačného zariadenia na aplikovanie logiky. Literatúra o subštrukturálnej logike nám poskytuje množstvo rôznych spôsobov, ako je možné použiť ternárnu relačnú sémantiku na opísanie logickej štruktúry niektorých javov, v ktorých sa tradičné štrukturálne pravidlá neuplatňujú.

Pre logiku, ako je Lambekovský počet, je interpretácia sémantiky jednoduchá. Body môžeme považovať za jazykové položky a ternárny vzťah je vzťahom zreťazenia ((Rxyz) iba vtedy, ak (x) zreťazený s (y) vedie k (z)), V týchto modeloch zlyhávajú štrukturálne pravidlá kontrakcie, oslabenia a permutácie, ale kombinácia predpokladov je asociatívna.

Súčasná literatúra o lingvistickej klasifikácii rozširuje základný Lambekov kalkul o bohatšie formy kombinácií, v ktorých je možné modelovať syntaktickejšie rysy (pozri Moortgat 1995).

Ďalšou aplikáciou týchto modelov je liečenie sémantiky funkčných aplikácií. Môžeme uvažovať o bodoch v štruktúre modelu ako o funkciách, ako aj o dátach, a myslíme si, že (Rxyz) iba vtedy, ak (x) (považovaný za funkciu) aplikovaný na (y) (považovaný za údaje)) je (z). Tradičné účty funkcií nepodporujú toto dvojaké použitie, pretože funkcie sa považujú za „vyššie“ako ich vstupy alebo výstupy (na tradičnom súbore teoretických modelov funkcií je funkcia (je) množina jej vstupov - výstupné páry, a tak sa nikdy nemôže brať ako vstup, pretože množiny sa nemôžu samy osebe stať členmi). Napríklad systémy funkcií, ktoré sú modelované netypovaným (lambda) - počtom, umožňujú samoaplikáciu. Vzhľadom na toto čítanie bodov v modeli,bod je typu (A / rightarrow B) len vtedy, keď vždy berie vstupy typu (A), berie výstupy typu (B). Inferenčné pravidlá tohto systému sú potom princípy, ktorými sa riadia typy funkcií: postupnosť

[(A / rightarrow B) amp (A / rightarrow C) vdash A / rightarrow (B / amp C))

hovorí, že vždy, keď funkcia trvá (A) s na (B) s a (A) s na (C) s, potom berie (A) s na veci, ktoré sú (B) a (C).

Tento príklad nám dáva model, v ktorom je príslušná subštrukturálna logika mimoriadne slabá. V tomto modeli nie sú splnené žiadne z obvyklých štrukturálnych pravidiel (dokonca ani asociativita). Tento príklad ternárneho relačného modelu je uvedený v (Restall 2000, kapitola 11).

Pokiaľ ide o príslušnú logiku (mathbf {R}) a jej interpretáciu kondicionálov v prirodzenom jazyku, musí sa urobiť viac práce pri identifikácii toho, aké vlastnosti reality tvoria formálne sémantické modely. Je to otázka určitej kontroverzie, pretože ternárny vzťah nie je oboznámený iba s tými, ktorých expozícia je primárne zameraná na modálnu logiku s jednoduchším vzťahom binárnej prístupnosti medzi možnými svetmi, ale aj kvôli novosti zaobchádzania s negáciami v modeloch pre relevantná logika. Nie je na našom mieste diskutovať o tejto diskusii podrobnejšie tu. Niektoré z tejto práce sú uvedené v článku o relevantnej logike v tejto encyklopédii a v tomto svetle je príslušnou logikou Maresova relevantná logika filozofická filozofia. tlmočenie (2004).

5. Kvantifikátory

Zaobchádzanie s kvantifikátormi v modeloch pre subštrukturálnu logiku sa ukázalo byť dosť ťažké, ale na začiatku 2000-tych rokov sa dosiahol pokrok. Problémy sa objavili v nesúlade medzi teóriou dôkazov a teóriou modelov pre kvantifikátory. Vhodné axiómy alebo pravidlá pre kvantifikátory sú pomerne jednoduché. Axiom eliminátora univerzálneho kvantifikátora (forall xA / rightarrow A [t / x]) uvádza, že inštancia vyplýva (v relevantnom zmysle) z jej univerzálnej zovšeobecnenia. Úvodné pravidlo (cfrac { vdash A / rightarrow B} { vdash A / rightarrow / forall xB}) (kde platí výhrada, že (x) nie je zadarmo v (A))) nám hovorí že ak dokážeme dokázať inštanciu zovšeobecnenia (forall xB), ako logiku, z nejakého predpokladu, ktorý v tejto inštancii nijako zvlášť netvrdí,z tohto predpokladu tiež môžeme dokázať zovšeobecnenie. Zdá sa, že táto axióma a pravidlo dobre zapadajú do akejkoľvek interpretácie kvantifikátorov prvého poriadku v rozsahu subštrukturálnej logiky, od najslabších systémov až po silné systémy ako (mathbf {R}).

Zatiaľ čo teória dôkazov pre kvantifikátory sa javí dobre chovaná, zovšeobecnenie na modelovanie teórie pre subštrukturálnu logiku sa ukázalo ako ťažké. Richard Routley (1980) ukázal, že pridanie pravidiel pre kvantifikátory do veľmi slabého systému subštrukturálnej logiky (mathbf {B}) je v súlade s ternárnou relačnou sémantikou, kde sú kvantifikátory interpretované tak, že zasahujú celú doménu objektov, konštantná vo všetkých bodoch modelu. Táto skutočnosť neplatí pre silnejšiu logiku, najmä pre príslušnú logiku (mathbf {R}). Kit Fine (1989) ukázal, že existuje komplexný vzorec, ktorý platí vo všetkých rámcových modeloch konštantnej domény pre (mathbf {R}), ale ktorý nie je odvoditeľný z axiómov. Podrobnosti argumentu Fine nie sú pre naše účely dôležité,ale základná príčina nesúladu je relatívne jednoduchá na vysvetlenie. V sémantike konštantnej domény má univerzálna zovšeobecnenie (forall x Fx) presne rovnaké podmienky pravdy - v každom bode modelu - ako rodina inštancií (Fx_1), (Fx_2), (Fx_3, / ldots), (Fx_ / lambda, / ldots), kde sú objekty domén spočítané hodnotami výrazov (x_i). Kvantifikovaný výraz (forall x Fx) je sémanticky nerozoznateľný od (možno nekonečnej) spojnice (Fx_1 / land Fx_2 / land Fx_3 / land / cdots). Žiadna kombinácia prípadov (aj nekonečná) však nemohla byť relevantne ekvivalentná univerzálne kvantifikovanému tvrdeniu (forall x Fx),pretože tieto prípady by mohli byť pravdivé za určitých okolností (alebo by sa to dalo dosiahnuť skutočnosťou), bez toho, aby sa zároveň zovšeobecnila generalizácia - keby existovalo viac vecí ako tých. Zdá sa teda, že modely s konštantnou doménou nie sú vhodné pre projekt relevantnej teórie kvantifikácie.

Nedávna práca Goldblatta a Maresa (2006) ukázala, že existuje alternatíva a ukázalo sa, že je elegantná a pomerne priama. Kľúčovou myšlienkou je modifikovať ternárnu relačnú sémantiku len tak, aby sa nemusel každý súbor bodov považovať za „návrh“. To znamená, že nie každý súbor bodov je možnou sémantickou hodnotou vety. Zatiaľ čo existuje množina svetov určená nekonečným spojením príkladov (forall xFx): (Fx_1 / land Fx_2 / land Fx_3 / land / cdots), táto presná sada svetov sa nemusí počítať ako návrh. (Možno neexistuje spôsob, ako tieto konkrétne predmety vyčleniť takým spôsobom, ktorý by ich spojil do jedného rozsudku.) Môžeme povedať, že zovšeobecnenie (forall xFx), a to je tvrdenie, ktoré zahŕňa každý prípad (to je axióma eliminácie univerzálneho kvantifikátora), a ak tvrdenie zahŕňa každý prípad, znamená to zovšeobecnenie (že je úvodné pravidlo), takže tvrdenie vyjadrené (forall xFx) je sémanticky najslabšie tvrdenie, ktoré zahŕňa každý prípad Fa. Toto je presne modelová podmienka pre univerzálny kvantifikátor v modeloch Goldblatta a Maresa a presne sa zhoduje s axiómami. Toto je presne modelová podmienka pre univerzálny kvantifikátor v modeloch Goldblatta a Maresa a presne sa zhoduje s axiómami. Toto je presne modelová podmienka pre univerzálny kvantifikátor v modeloch Goldblatta a Maresa a presne sa zhoduje s axiómami.

Bibliografia

Komplexnú bibliografiu o relevantnej logike zostavil Robert Wolff a možno ju nájsť v Andersonovi, Belnapovi a Dunnovi 1992. Bibliografia v Restall 2000 (pozri Ďalšie internetové zdroje) nie je taká komplexná ako Wolffova, ale obsahuje materiál až po súčasnosť.

Knihy o subštrukturálnej logike a úvodoch do terénu

  • Anderson, AR, a Belnap, ND, 1975, Entailment: The Logic of Relevance and Necessity, Princeton, Princeton University Press, Zväzok I.
  • Anderson, AR, Belnap, ND Jr., a Dunn, JM, 1992, Entailment, Zväzok II, Princeton, Princeton University Press

    [Táto kniha a predchádzajúca publikujú zhrnutie práce v relevantnej logike tradície Anderson-Belnap. Niektoré kapitoly v týchto knihách majú iných autorov, ako napríklad Robert K. Meyer a Alasdair Urquhart.]

  • Dunn, JM a Restall, G., 2000, „Relevance Logic“v F. Guenthner a D. Gabbay (eds.), Handbook of Philosophical Logic, druhé vydanie; Zväzok 6, Kluwer, str. 1-136.

    [Zhrnutie práce v relevantnej logike v tradícii Andersona-Belnapa.]

  • Galatos, N., P. Jipsen, T. Kowalski a H. Ono, 2007, Zbytkové mriežky: Algebraický pohľad na subštrukturálnu logiku (Štúdie v logike: zväzok 151), Amsterdam: Elsevier, 2007.
  • Mares, Edwin D., 2004, Relevantná logika: filozofická interpretácia Cambridge University Press.

    [Úvod do relevantnej logiky, navrhujúci teoretické informácie o porozumení ternárnej relačnej sémantiky.]

  • Moortgat, Michael, 1988, Kategorické vyšetrenia: Logické aspekty Lambek Calculus Foris, Dordrecht.

    [Ďalší úvod do Lambekovho počtu.]

  • Morrill, Glyn, 1994, Typ Logická gramatika: Kategorická logika znakov Kluwer, Dordrecht

    [Úvod do Lambekovho počtu.]

  • Paoli, Francesco, 2002, Substructural Logics: Primer Kluwer, Dordrecht

    [Všeobecný úvod do subštrukturálnej logiky.]

  • Čítané, S., 1988, Relevantná logika, Oxford: Blackwell.

    [Úvod do relevantnej logiky motivovanej úvahami v teórii významu. Vyvíja teóriu dôkazov typu Lemmon pre príslušnú logiku (mathbf {R}).]

  • Restall, Greg, 2000, Úvod do subštrukturálnej logiky, Routledge. (online précis)

    [Všeobecný úvod do oblasti subštrukturálnej logiky.]

  • Routley, R., Meyer, RK, Plumwood, V., a Brady, R., 1983, Relevant Logics and jejich Rivals, zväzok I, Atascardero, CA: Ridgeview.

    [Ďalší výrazný opis relevantnej logiky, tentoraz z austrálskeho filozofického hľadiska.]

  • Schroeder-Heister, Peter a Došen, Kosta, (eds), 1993, Substructural Logics, Oxford University Press.

    [Upravená zbierka esejí o rôznych témach v subštrukturálnej logike, od rôznych tradícií v tejto oblasti.]

  • Troestra, Anne, 1992, Lectures on Lineear Logic, CSLI Publications

    [Stručný a ľahko čitateľný úvod do Girardovej lineárnej logiky.]

Ďalšie uvedené práce

  • Ackermann, Wilhelm, 1956, „Begründung Einer Strengen Implikation“, Journal of Symbolic Logic, 21: 113–128.
  • Avron, Arnon, 1988, „Sémantika a dôkazná teória lineárnej logiky“, Teoretická informatika, 57 (2–3): 161–184.
  • Gianluigi Bellin, Martin Hyland, Edmund Robinson a Christian Urban, 2006, „Kategorická dôkazná teória klasického navrhovaného počtu“, teoretická informatika, 364: 146–165.
  • Church, Alonzo, 1951, „Slabá teória implikácie“, v Kontrolliertes Denken: Untersuchungen zum Logikkalkül und zur Logik der Einzelwissenschaften, A. Menne, A. Wilhelmy a H. Angsil (ed.), Kommissions-Verlag Karl Alber, 22 -37.
  • Curry, Haskell B., 1977, základy matematickej logiky, New York: Dover (pôvodne publikovaný v roku 1963).
  • Dunn, JM, 1991, „Gaggleova teória: abstrakcia galoisových spojení a rezíduí s aplikáciami na negácie a rôzne logické operácie,“v Logics in AI, Proceedings European Workshop JELIA 1990 (Poznámky k prednáške v odbore informatiky, zväzok 476), Berlín: Springer-Verlag.
  • Dunn, JM, 1993, „Star and Perp“, Philosophical Perspectives, 7: 331–357.
  • Fine, K., 1989, „Inkompletity for Quantified Relevance Logics“, J. Norman a R. Sylvan (eds.), Pokyny v relevantnej logike, Dordrecht: Kluwer, s. 205–225.
  • Geach, PT, 1955, „On Insolubilia“, analýza, 15: 71–72.
  • Gentzen, Gerhard, 1935, „Untersuchungen über das logische Schließen“, Mathematische Zeitschrift, 39: 176–210 a 405–431. [Anglický preklad sa nachádza v Gentzen 1969.]
  • Gentzen, Gerhard, 1969, The Collected Papers of Gerhard Gentzen, ME Szabo (ed.), Amsterdam: North Holland, 1969.
  • Goldblatt, R. a E. Mares, 2006, „Alternatívna sémantika pre kvantifikovanú relevantnú logiku“, Journal of Symbolic Logic, 71 (1): 163–187.
  • Girard, Jean-Yves, 1987, „Lineárna logika“, Theoretical Computer Science, 50: 1-101.
  • Lambek, Joachim, 1958, „The Mathematics of Sentence Structure“, American Mathematical Monthly, 65: 154–170.
  • Lambek, Joachim, 1961, „Kalkul syntaktických typov“, v štruktúre jazyka a jeho matematických aspektov (Zborník sympózií v aplikovanej matematike, XII), R. Jakobson (ed.), Providence, RI: American Mathematical Society.
  • Moh Shaw-Kwei, 1950, „Dedukčné vety a dva nové logické systémy“, Methodos, 2: 56–75.
  • Moortgat, Michael, 1995, „Multimodal Linguistic Inference“, Logic Journal of IGPL, 3: 371–401.
  • Ono, Hiroakira, 2003, „Subštrukturálna logika a zvyškové mriežky - úvod“, v V. Hendricks a J. Malinowski (ed.), Trends in Logic: 50 rokov Studia Logica, Dordrecht: Kluwer, 2003, s. 193– 228.
  • Routley, R., 1980. „Problémy a riešenia v sémantike v kvantifikovanej relevantnej logike“, v A. Arruda, R. Chuaqui a NCA Da Costa (ed.), Matematická logika v Latinskej Amerike, Amsterdam: Severný Holland, 1980, strany 305 - 340.

Akademické nástroje

ikona sep muž
ikona sep muž
Ako citovať tento záznam.
ikona sep muž
ikona sep muž
Ukážku verzie tohto príspevku vo formáte PDF si môžete pozrieť na stránke Friends of the SEP Society.
ikona
ikona
Vyhľadajte túto vstupnú tému v projekte Internet Philosophy Ontology Project (InPhO).
ikona phil papiere
ikona phil papiere
Vylepšená bibliografia tohto záznamu vo PhilPapers s odkazmi na jeho databázu.

Ďalšie internetové zdroje

  • Restall, Greg, 1994, Logics without Contraction, Ph. D. Thesis, Queenslandská univerzita.
  • Slaney, John, 1995, MaGIC: Matrix Generator for Implication Connectives, softvérový balík na generovanie konečných modelov pre subštrukturálnu logiku.

Odporúčaná: