"Porazdelitev variabel" kot algoritem relevance
MARKO URŠIČ
Glavni historični motiv za nastanek logike relevance kot nadgradnje modalne logike so bili t. i. paradoksi striktne implikacije. C. I. Lewis (1918 in 1932, skupaj z Langfordom), utemeljitelj modalne logike, je uvedel striktno implikacijo kot "necesitirano" materialno implikacijo med drugim tudi zato, da bi se izognil t. i. paradoksom materialne implikacije, tj. formulam:
(1)	A D (B D A) " Resničen stavek je impliciran od kateregakoli stavka."
(2)	~ A3 (A3B) " Neresničen stavek implicira katerikoli stavek."
V Lewisovih sistemih striktne implikacije (modalne logike) formuli (1) in (2), "prevedeni" v striktno implikacijo 'A —3 B', nista več teorema, tako kot v standardnih ekstenzionalnih (resničnostno-funkcijskih) sistemih. Nastane pa nova težava, ki so jo kritiki Lewisovih sistemov imenovali paradoksi striktne implikacije (npr. že Nelson 1930, Duncan-Jones 1935, Ackermann 1956, predvsem pa Anderson & Bclnap 1975). Formuli:
(ls) □ A —3 (B—3 A) " Nujen stavek je striktno impliciran od kateregakoli stavka."
(2s) - O A —3 (A—3 B)" Nemožen stavek striktno implicira katerikoli stavek."
ostajata teorema Lewisovih modalnih sistemov, čeprav jima per analogiam prav tako lahko očitamo paradoksnost, kot formulama (1) in (2). Za relevantiste, Lewisovc kritike, je še posebej sporna in paradoksna varianta teze (2s), namreč teza ex contradic-tione sequitur quodlibet:
(2's) (A & ~ A) —3 B .
Paradoksna naj bi bila ta teza predvsem zato, ker iz poljubnega protislovja sledi (implicira) poljubni stavek, pri čemer konsekvens ni v nobeni relevantni ("pomenski") zvezi z antecedensom. Lewis in njegovi somišljeniki (npr. Bennett 1954, Prior 1948, Hughes & Cresswell 1968 idr. privrženci modalnih sistemov levisovskega tipa) trdijo, da teza (2' s) izraža enega temeljnih principov formalne logike sploh, ki daje neposredno povezan z načelom neprotislovnosti sistema. Relevantisti to zanikajo in pravijo, da formula:
(2r) (A & ~ A) —» B,
pri čemer znak'—»' pomeni "sledenje" (entailment) ni teorem v sistemih relevantne logike oz. sistemih logike relevance, enako pa velja tudi za paradokse striktne implikacije, če implikacijski veznik '—3' beremo kot sledenje'—*'.
Relevantna implikacija (= sledenje) naj bi torej zagotavljala "pomensko zvezo" med antecedensom in konsekvensom in tako formalno ustrezala intuitivnemu pomenu besede 'implicirati' kot obratu odnosa 'slediti iz ...'. Zgodnji relevantisti (Nelson, Duncan-Jones, Baylis, Parry idr.) so upali, da bo "pomensko zvezo" možno zajeti (capture) v formalno-sistemsko mrežo; ta optimizem seje pozneje kljub nedvomnemu razvoju sistemov (in algoritmov) relevance precej zmanjšal, kajti zveza pomenov se je izkazala za zelo zmuzljiv pojem {elusive notion), tako da glavna protagonista sodobne logike relevance, Belnap v Ameriki in Routley v Avstraliji, svojo programsko nalogo vidita predvsem v precizaciji relevantne implikacijske zveze (sledenja), ki se pogosto prekriva z analizo deduktivnega postopka.
Temeljno relevantistično delo Andersona in Bclnapa Entailment (1975) je glede optimizma "zajetja" relevance nekje na sredi med Nelsonom in sodobnimi relevantisti. Gre seveda za zelo široko in kompleksno problematiko, ki jo v pričujoči razpravi -pravzaprav le segmentu širše študije - omenjam zgolj uvodoma, več o tem gl. Uršič (1990). Na tem mestu bom skušal na nekaterih primerih algoritmov (upoštevanja) relevance, predvsem s t. i. "porazdelitvijo variabel" v stavčni logiki, pokazati, da ideja relevance vendarle je dostopna formalni obravnavi, namreč na podoben in analogen način, kot so npr. modalnosti - še posebej nujnost - dostopne formalni obravnavi. Logike relevance po mojem mnenju nudijo "preciznejša orodja" za analizo jezikovno-logične forme kot standardni sistemi. Z modalnimi sistemi pa se sistemi relevance ne izključujejo, temveč jih "nadgrajujejo".
Najprej si bomo ogledali Ackermannov teorem (1956), s katerim Ackermann skuša iz formalnega sistema izločiti vse tiste formule, ki bi jim per analogiam s paradoksi materialne in striktne implikacije lahko pripisovali paradoksnost. Dokaz bom predstavil v Andersonovi & Belnapovi verziji iz Entailment (1975), in sicer za "minimalni implikacijski račun", ki kot logični veznik vsebuje samo implikacijo, namreč "sledenje"'—*', kot variable pa stavčne variable nad elementarnimi stavki 'p', 'q', 'r',... in variable nad formulami, sestavljenimi z veznikom '—►' iz elementarnih stavkov, pri čemer so slednje tudi formule 'A', 'B', 'C', ... (ne pa nujno obratno, kakor bomo videli spodaj); sistem E—„ sestavljen iz navedenih jezikovnih elementov, Anderson & Belnap definirata z naslednjimi aksiomi:
(E—»1) A—A	(identiteta)
(E-_»2) (A—►B)—»((B—»C)—»(A—»C))	(tranzitivnost)
(E—*3) (A—-B)—*(((A—-B)—-C)—»C)	("restriktivna" asercija)
(E—»4) (A—»(B—-C))—»((A—»B)—»(A—»C))	(sšmo-distribucija)
in s pravilom izpeljave modus ponens (gl. Entailment, str. 24) ter z običajnimi pravili
substitucije, razen A // p. Ackermannov teorem se za sistem skupaj z dokazom glasi takole:
"TEOREM, p—»(B—-C) ni dokazljiv v E_kadar je p /elementarna/ stavčna
variabla (Ackermann 1956).
DOKAZ. Poglejmo si matrico (prirejeno po Ackermannu):
—	0	1	2
0	2	2	2
1	0	2	0
+ 2	0	0	2
Za to matrico teoremi sistema E__» vedno dobijo (označeno) vrednost 2; toda za katerokoli formulo p—» (B—► C), v kateri je p stavčna variabla, lahko variabli p podelimo vrednost 1, kar da formuli p—»(B—»C) vrednost 0 ne glede na vrednosti B in C. Torej ni nobena takšna formula p—»(B—»C) dokazljiva."(Entailment, str. 40).
Navedeni dokaz je eden izmed mnogih izjemno elegantnih dokazov s pomočjo (skonstruiranih) matric, kakršne je prvi začel uporabljati Lukasiewicz (1929) za dokazovanje neodvisnosti aksiomov in so se potem razširili kot metoda za dokazovanje najrazličnejših teoremov v formalnih sistemih. Bistvena zamisel takšnega dokaza je, da s pomočjo skonstruirane matrice z eno ali več "označenimi vrednostmi" (designated value; tukaj jo označujemo s križcem ' +') definiramo neko - običajno povsem abstraktno (ncinterpretirano) - lastnost/', ki jo imajo tiste formule, ki "zadovoljujejo" oz. "izpoljujejo" (satisfy v smislu Tarskega 1933) to matrico, medtem ko je druge, ki lastnosti P nimajo, ne "izpolnjujejo". V našem zgornjem dokazu "izpolnjujejo" matrico vsi štirje
aksiomi sistema namreč (E_► 1) - (E_»4), prav tako jo "izpolnjuje" (s tem da
"ohranja" lastnost P) pravilo modus ponens, zato jo "izpolnjujejo" vsi teoremi sistema E_; med teoremi pa ne najdemo nobene formule vobliki p—»(B—»C), saj takšne formule nimajo lastnosti P, torej ne "izpolnjujejo" matrice. Med slednjimi so tudi t. i. paradoksi implikacije, tako materialne kot striktne, kakor tudi vse formule implikacije, ki so pradoksne v smislu Sugihare (1955).
Anderson & Belnap se v svojem epohalnem delu Entailment - the Logic of Relevance and Necessity (1975) ne zadovoljita zgolj z Ackermannovim kriterijem relevance (oziroma, natančneje, kriterijem zavrnitve nerelevance), saj se jima kaže kot še vedno premalo restriktiven, ker npr. ne izključuje formule (A—►A)—»(B—»B), za katero smatrata, da ni relevantna, torej ne sodi v sistem logike sledenja E—..Zato Anderson & Belnap formulirata dodatne kriterije (ne)relevance in s tem tudi nove tehnike zavrnitve nerelevantnih formul, med katerimi je posebej zanimiv kriterij "porazdelitve variabel", ki ga bom predstavil v pričujočem tekstu.
Kriterij "porazdelitve variabel" (sharing of variables) in z njim povezan algoritem izločanja nerelevantnih formul iz sistema logike sledenja je vsekakor zanimiv formalno-logični postopek za poskus vsaj delnega zajetja "pomenske zveze", čeprav je treba priznati, da algoritmu oz. metodi "porazdelitve" manjka nekaj tiste splošnosti, ki jo pričakujemo od vsakega tovrstnega kriterija. Algoritem namreč določa, katere formule niso relevantne, ne določa pa v splošnem, katere so. Za pozitivno opredelitev relevance morata Anderson & Belnap, kakor tudi drugi relevantisti, poseči v analizo dokaza (npr. naravne dedukcije), kjer pride v poštev metoda indeksiranja ("podpisovanja", subseript-ing) hipotez in vrstic v dokazu; vendar slednje metode ne bom obravnaval v okviru tega fragmenta.
Metoda "porazdelitve variabel" temelji na dveh teoremih, ki ju bomo skupaj z dokazoma navedli spodaj. Uvodoma lahko rečemo, da je v izvajanju Andersona & Belnapa (1975) s formalno-"tehničnega" zornega kota povsem jasno in nedvoumno, kaj izraz sharing of variables ali variable-sharing pomeni. S semantičnega stališča (predvsem s stališča semantike naravnega jezika) so stvari manj jasne. V slovenščini se zatakne že pri prevodu: sharing namreč ne pomeni samo "porazdelitev", temveč tudi "udeleženost", "so-udeleženost", "skupnost" itd. V smislu angl. share se deli kruh in vino pri obhajilu -namreč tako, da so vsi, ki pri tej (poraz)delitvi so-delujejo, deležni vsak po en (akciden-talno gledano) del istega (substancialno gledano) kruha in vina. Analogno naj bi se sharing dogajala tudi v logiki relevance: antecedens in konsekvens (ali "anteccdenčni del" in "konsekvenčni del", kakor bomo videli spodaj) implikacijske formule naj bi si "(po)razdelila" skupno variablo (ali variable). Prevod "porazdelitev" za angl. sharing torej v tem kontekstu ni najboljši, vendar mislim,da v slov. ni ustreznejšega. Nekoliko hujši problem je seveda v tem, da kljub formalni preciznosti in neoporečnosti tehnike variable-sharing s semantičnega stališča ostaja nekako nejasno, kaj se pravzaprav "porazdeli". (To vrzel bi bržkone moral zapolniti 2. del knjige Entailment, ki pa je precej spremenjen glede na prvotno zamisel izšel šele pred nedavnim.) Na prvi pogled se nam pri variable-sharing vsiljuje analogija s "porazdelitvijo" terminus medius v silogizmu, vendar ta analogija drži zgolj na neki najsplošnejši ravni, sicer pa je med variable-sharing in terminus medius bistvena razlika, tako sintaktična kot semantična, saj se prvo nanaša na (elementarne in sestavljene) stavke, drugo pa na pojme oz. termine kot pomenske enote. Razumevanje stavkov kot osnovnih pomenskih enot skoraj gotovo ni Ander-sonova & Belnapova intenca, saj bi takšno razumevanje vodilo v fregejevsko redukcijo pomena stavkov na binarni Bedeutung in nadalje v standardni sodobni logični kanon.
Čeprav lahko torej zavrnemo neposredno analogijo "porazdelitve" variabel s terminus medius, pa gre pri relevantistih s semantičnega stališča vendarle za "skupno pomensko vsebino" (izraz je seveda okoren) med antecedensom in konsekvensom v implikaciji (sledenju). S tem se relevantisti nedvomno uvrščajo v tradicijo Lewisa, Nelsona in drugih "alternativcev" v logiki našega stoletja, o čemer Anderson in Belnap govorita na začetku paragrafa o variable-sharing-.
"... relevanca A v odnosu do B kot nujni pogoj za resničnost A —► B je tukaj mišljena tako, da zahteva neko 'pomensko vsebino' skupno obojemu, A in B. Ta klic k skupni pomenski vsebini prihaja z različnih vetrov. Nelson 1930 pravi, da je implikacija 'nujna zveza med pomeni'; Duncan-Jones 1935 meni, da A implicira B samo takrat, ko B 'vznikne iz pomena' A ; Baylis 1931 trdi, da če A implicira B, potem je 'intenzionalni pomen B identičen z delom intenzionalnega pomena A'; in Blan-shard 1939 pravi, da tisto, 'iz česar izvira zdravorazumski ugovor /proti striktni implikaciji/, je kljubovalen občutek, da ima implikacija nekaj opraviti s pomenom stavkov in da vsakršen način njihove povezave, ki ne upošteva tega pomena in jih združuje njemu navkljub /kar naj bi s stališča relevantistov veljalo tudi za Lewisovo striktno implikacijo in njene "paradokse", op.M.U./, ostaja preveč umeten, da bi izpolnil zahtevo misli'." (Entailment, str. 32-33)
In zdaj že končno preidimo k sami formalni zastavitvi "porazdelitve" variabel. Anderson & Belnap jo izvajata neposredno iz splošne zahteve po "skupni pomenski vsebini":
"Formalni pogoj za 'skupno pomensko vsebino' ('common meaning content') se ponuja skoraj na dlani, brž ko ugotovimo, da se skupnost pomena v stavčni logiki
dosega s skupnostjo (commonality) stavčnih variabel. Zato predlagamo kot nujni, nikakor pa ne kot zadostni pogoj za relcvanco A v odnosu do B v čistem računu sledenja, da si morata A in B porazdeliti variablo (that A and D must share a variable, tj. da morata imeti skupno vsaj eno variablo, op. M. U.)."(Entailment, str. 33) Ta zahteva je izražena s Teoremomi takole:
"TEOREM. Če je A—► B dokazljiv v E_», potem je med A in B porazdeljena vsaj ena variabla (tj. vsaj eno variablo imata skupno)." (Entailment, ibid.) Znaka 'A' in 'B' sta seveda variabli nad formulami, ki vsebujejo variable za (elementarne) stavke p, q, r, itd. in prav le-te oziroma vsaj ena izmed njih naj bi bila skupna A in B, tj. "porazdeljena" med A in B. Če Teoremi s kontrapozicijo "obrnemo", dobimo neposreden korolarij:
KOROLARIJ. Če med A in B ni porazdeljena nobena variabla (tj. če A in B nimata niti ene variable skupne), potem A—»B ni dokazljiv v E_► .
Iz Teoremai torej dobimo prvi Andersonov & Belnapov kriterij za zavrnitev nerelevantnih implikacijskih formul sistema E_ Še preden pa ta kriterij lahko apliciramo, moramo seveda Teoremi dokazati. Anderson in Belnap ga s pomočjo matrice dokažeta takole:
"DOKAZ. Poglejmo si naslednjo matrico (finitno priredbo matrice, ki jo je formuliral Sugihara 1955; s križcem ' -I-' so označene designated values):
—	-2	-1	+ 1	+ 2	
-2	+ 2	+ 2	+ 2	+ 2	
-1	-2	+ 1	+ 1	+ 2	("pozitivne" vrednosti
+ 1	-2	-1	+ 1	+ 2	"označene" vrednosti)
+ 2	-2	-2	-2	+ 2	op. M.U.
Aksiomi sistema E—dobijo označene vrednosti (designated values) za vse podelitve vrednosti variablam, pa tudi pravilo (—»Izl) ohranja svoj značaj. Toda v primeru, če A in B nimata nobenih skupnih variabel, lahko podelimo vrednost + 2 vsem variablam v A (in dobimo A = + 2) in vrednost + 1 vsem variablam v B (in dobimo B = +1), pri čemer + 2—► + 1 dobi neoznačeno vrednost -2. Torej, če A in B nimata skupne variable, potem je A—»B nedokazljiv." (Entailment, str.33) Dokaz uporablja isto metodo kot dokaz Ackermannovega teorema, ki smo ga navedli in komentirali zgoraj, zato tukaj komentarja o samem dokazu ne bomo ponavljali, čeprav gre za drugačno matrico z dvema označenima vrednostima. Brez težav
je seveda mogoče preveriti, da vsi aksiomi sistema torej (E_l) - (E_► 4) ali
katerikoli drugi ekvivalentni niz aksiomov "zadovoljujejo" navedeno matrico. Lahko pa rečemo še nekaj besed o samem Teoremui. (Indeksikacija je naša, gre seveda za citirani TEOREM iz Entailment, str. 33). Teoremi Andersona & Belnapa se kot kriterij (ne)relevance razlikuje od svojih predhodnikov predvsem po tem, da ne temelji na "analitičnem" pojmu relevance, ki nastopa npr. pri Parry 1933 et al.:
" Če je A—B dokazljiv v PAI, tedaj, vse variable v B nastopajo tudi v A." (Parry 1933, cit. po Entailment 1975, str. 431.)
Očitno je torej sistem PAI, "analitični" implikacijski sistem, restriktivnejši od E, saj postavlja ostrejše zahteve za relevanco oziroma eliminira več "nerelevantnih" formul, med drugimi tudi formuli p—-(p vq) in (p & q)—p, kiju Anderson & Belnap sprejemata kot resnični implikaciji (sledenja). Prva izmed teh dveh formul namreč očitno krši Parryjev teorem, druga pa je s prvo neločljivo povezana z De Morganovim zakonom oziroma s simetrijo konjunkcije in disjunkcije. Andersonov & Belnapov Teoremi ti dve formuli ne izključuje iz sistema E kot nerelevantni, bolje rečeno, nista že na samem začetku (kot pri Parryju) zavrnjeni, saj imata njuna antecedensa in konsekvensa vsaj eno variablo skupno, namreč p, kar seveda še ni zadosten, je pa nujen pogoj za relevanco.
Obstaja pa seveda vrsta stavčnih formul, ki po kriteriju na osnovi Teoremai nimajo "kvalifikacij" za vstop vklub relevantistov. Med njimi je tudi formula (A—»A)—(B—B), katere Ackermannov kriterij, izražen z njegovim Teoremom, ni "ujel v svojo mrežo", čeprav je z intuitivnega stališča očitno nerelevantna; - predvsem pa Teoremi izloči formule, ki pri Lewisu nastopajo kot teoremi striktne implikacije in so pri Lewisovih kritikih (med katerimi sta tudi Anderson & Belnap) dobili naziv "paradoksi striktne implikacije". Arhetipska oblika teh paradoksov je formula:
(•) B—(A—A),
ki je pri Andersonu & Belnapu v sistemu E_. zavrnjena (zato smo jo označili z
zvezdico), ker je možno, da antecedens B in konsekvens (A—►A) nimata nobene skupne variable - namreč takrat, ko v A nastopajo povsem druge (elementarne) variable kot v B, recimo: v A nastopajo p, q, r, v B pa s, t, u. Torej, čeprav je konsekvens formule (*) nujen, saj izraža princip identitete, ta konsekvens ne sledi iz (poljubnega) antecedensa B, ker nista v relevantnem odnosu. Zanimivo pa je, da Teoremi ne zavrne kot ne-relevantno tisto formulo, ki izraža paradoks materialne implikacije (nedvomno očitnejši od paradoksa striktne implikacije), ki pa jo je zavrnil že Ackermannov kriterij in pred njim seveda Lewis in drugi. V formuli
A—(B—A)
namreč antecedens A in konsekvens (B—»A) morata imeti vsaj eno skupno variablo, recimo p v A, oziroma, če poenostavimo (kakor bomo tudi v nadaljevanju): antecedensu in konsekvensu navedene formule A—►(B—»A) je skupna variabla A, torej formula zadovoljuje kriterij relevance, izražen v Teoremui, čeprav je prav ta formula, kot pravita Anderson & Belnap, "arhetip napak relevance" (Entailment, str. 30), zato morata v sistemu E—►polegTeoremai formulirati še en teorem, imenovali ga bomo Teorem2 za zavrnitev nerelevantnih implikacijskih formul. Preden si ogledamo Teorem2, njegov dokaz in selektivno "delovanje", pa moramo definirati dva nova pojma: "antecedenčni del" in "konsekvenčni del" (neke poljubne) implikacijske formule v E—.
Najprej bomo citirali Andersovo in Belnapovo definicijo:
"Antecedenčni del /implikacijske formule/ A in konsekvenčni del /te iste formule/
A definiramo induktivno takole:
(a) A je konsekvenčni del A-ja /tj. samega sebe/;
(b)	če je B—»C konsekvenčni del A-ja, potem je B antecedenčni del A-ja in C je konsekvenčni del a-ja; in
(c)	če je B—»C antecedenčni del A-ja, potem je C antecedenčni del A-ja in B konsekvenčni del A-ja." (Entailment, str. 34)
Na videz malce komplicirana definicija antecedenčnega dela in konsekvenčnega dela (oziroma delov) implikacijske formule se v praksi izkaže kot zelo enostavna in operativna. Antecedenčni del (oz. dele) označimo z 'a', konsekvenčni del (oz. dele) s 'k'. Postopek ločevanja si oglejmo na konkretnem primeru, npr. kar na nerelevantni formuli paradoksa materialne implikacije:
(B^-fA)
k: formula sšma, (B—*A), A a: A, B
V formuli A—»(B—*A) nastopa variabla B samo kot antecedenčni del, medtem ko variabla A nastopa kot oboje, antecedenčni del in konsekvenčni del. Poglejmo si še en primer, tokrat aksiom (E_„3):
.(A—►B)—► (((A—►B) -+Q-+C)
i a k a
-v-k
k
a
<--N
(A—► B) —► C
: k a k
k: formula sama, (((A—► B)—► C)—► C),
A, C, (A—»B), B. a: (A—»B), B, ((A—»B)—»C), C, A.
V tej implikacijski formuli, aksiomu (E_»3) pa vse variable A, B, C nastopajo v obeh vlogah, kot antecedenčni deli in kot konsekvenčni deli. Ločevanje antecedenčnih in konsekvenčnih delov implikacijskih formul pa je še neprimerno enostavnejše v Lukasiewiczevem zapisu, kar je pokazal John Bacon, eden izmed Andersonovih & Belnapovih sodelavcev (gl.Entailment, str. 93). Za primerjavo zapišimo zgornjo formulo še enkrat v našem "običajnem" zapisu in pod vsakim njenim delom dodajmo oznako za 'k' oziroma 'a':
(A—* B) —► (((A—► B) C) C) kaak akk aa kk
Niz črk 'k' in 'a' v tem zapisu ni nič kaj posebej urejen (vsaj na prvi pogled ne). Če pa to isto formulo zapišemo v Lukasiewiczevem slogu, kjer pišemo funktorje (v našem
primeru implikacijo, zanjo bomo tukaj kar ohranili znak'—*' namesto Lukasiewiczevega 'C') pred variablami, dobimo:
——►A B—►ABCC k akak a kakak
Kot vidimo, je implikacijska formula v Lukasiewiczevem zapisu zapisana vedno (kot je pokazal John Bacon) tako, da se v njej konsekvenčni in antecedenčni deli (enakomerno) izmenjavajo, alternirajo, kar nam seveda - ob predpostavki (iz definicije), da je sama formula (svoj lastni) konsekvenčni del, tj. da je prva črka v L. nizu 'k' - nudi zelo enostavno metodo za ločevanje 'k' od 'a', če le formulo zapišemo v L. zapisu.
In zdaj navedimo že napovedani Andersonov & Belnapov Tcorcm2 za zavračanje nerelevantnih implikacijskih formul:
"TEOREM. Če je A teorem E_», potem vsaka variabla, ki nastopa v A, nastopa najmanj enkrat kot antecedenčni in najmanj enkrat kot konsekvenčni del A-ja." (Entailment, str. 34)
Dokaz tega teorema, ki ga imenujemo Teorem2, je zgrajen na osnovi uporabe iste štirivalentne matrice, ki smo jo uporabili za dokaz Teoremai (glej zgoraj). Takole gre: "DOKAZ: Če variabla p nastopa samo kot antecedenčni del A-ja, pripišemo p-ju vrednost -t- 2, in če nastopa samo kot konsekvenčni del, ji pripišemo vrednost -2; vsem drugim variablam A-ja pripišemo vrednost +1. Potem je možno dokazati z indukcijo vzdolž A-ja, da ima vsak pravilno formuliran del B formule A naslednjo lastnost:
(1)ČeB	ne vsebuje p, je vrednost B = +1;
(2)	če B vsebuje p in jc antecedenčni del A-ja, potem je vrednost B = + 2; in
(3)	če B vsebuje p in je konsekvenčni del A-ja, potem je vrednost B = -2.
Iz (3), skupaj z dejstvom, daje A konsekvenčni del samega sebe, sledi, da A dobi vrednost -2 in je torej nedokazljiv." (Entailment, ibid.)
Iz Teorema2 na osnovi kontrapozicije sledi neposreden korolarij:
KOROLARIJ. Če vsaka variabla, ki nastopa v A, ne nastopa niti enkrat kot oboje,
tj. kot antecedenčni in konsekvenčni del A-ja, potem A ni teorem E_...
Tako torej dobimo iz Teorema2 drugi "AB" kriterij za zavrnitev nerelevantnih implikacijskih formul. Tudi ta kriterij opredeljuje relevanco zgolj per negationem, izpolni pa tisto vrzel ("zgosti sito"), kije ostala odprta po Teoremui. Iz zgoraj navedenih
dveh primerov je očitno, da A—»(B—"A) ni relevantna formula v E_„, kajti ne ustreza
kriteriju izTeorema2 (variabla B ne nastopa kot oboje, tj. kot 'k' in 'a', temveč samo kot 'a'), čeprav to formulo "spusti skozi" Teoremi (saj antecedens in konsekvens imata skupno vsaj eno variablo, namreč A). Po drugi strani je očitno, da aksiom (E—.3), ki nastopa v zgornjem primeru, je relevanten po kriteriju Teorema2 - oziroma, natančneje rečeno, da po kriteriju Teorema2 (in tudi po kriteriju Teoremai) ni izločen kot ne-relevanten. (Njegovo relevanco, kakor tudi relevanco drugih formul v E—»,palahko dokažemo zgolj "po ovinku", kot bomo videli pozneje: naprej z metodo naravne dedukcije v sistemu FE_pokažemo, da je (recimo) teorem X relevanten - namreč dokažemo
v pozitivnem smislu, ne zgolj per negationem ne zavrnemo, - potem dokažemo ekvivalen-
co sistemov FE_»in E_ ter formuliramo aksiomatski dokaz za X iz aksiomov sistema
E—► . Q. E. D. Pot do pozitivnega dokaza relevance neke formule X je torej precej dolga. Tukaj lahko navedemo še primer, ko neka formula pri testu relevance "pade skoz sito" Teorema2, vendar pa jo "zadrži" kot nerelevantno Teoremi; gre npr. za formulo (A—*A)—"(B—»B), v kateri obe variabli A in B nastopata kot 'k' in kot 'a', vendar pa je formula zavrnjena preprosto zaradi enostavnega kriterija Teoremai, ker nimata an-tecedens (A—»A) in konsekvens (B—*B) nobene skupne variable. S tem v zvezi je zanimivo ugotoviti, da Teorem2 pravzaprav zagotavlja neke vrste enakomerno porazdelitev ali medsebojno prepletenost variabel v implikacijski formuli, kar je najbolj jasno razvidno iz altcrnacije 'k' in 'a' v Lukasievviczevem zapisu. V relevantni formuli (E—,3) so variable porazdeljene in prepletene, v formuli (A —A) —»(B —6) sicer so "porazdeljene", niso pa prepletene, kar pa ugotovimo s Teorcmomi, v formuli A—»(B—»A) pa variabla B ni "porazdeljena", kar pa ugotovimo s Teoremom2. Iz tega sledi, da sta Teoremi in Teorem2 sicer medsebojno povezana, nista si pa podrejena ne v eni ne v drugi smeri, tj. T2 ni podteorem Ti in tudi Ti ni podteorem T2. Sta relativno neodvisna kriterija za zavrnitev nerelevantnih formul v E_. Iz Tcorema2 pa neposredno sledi še en korolarij:
"Nobena variabla ne more nastopati zgolj enkrat v teoremu sistema E_„."
(Entailment, str. 35)
Vse variable morajo biti namreč "porazdeljene" in "prepletene" po antecedenčnih in konsekvenčnih delih relevantne formule, kar pa ni možno, če vsaka variabla v formuli ne nastopa vsaj dvakrat.
Za konec pričujočega razdelka o metodi "porazdelitve variabel" bomo navedli
nekaj takšnih implikacijskih formul, ki so relevantne (in hkrati teoremi sistema E_,),
in nekaj takšnih, ki niso relevantne, torej so zavrnjene (kar označujemo z zvezdico): A—A	(identiteta)
(A—B)—((B—C)-—(A—C))	(tranzitivnost - konsekvens)
(A—B)—((C—A)—(C—B))	(tranzitivnost - anteccdens)
(A—»(A—»B))—»(A—"B)	(kontrakcija)
(A—»(B—"C))—»((A—»B)—»(A—-C)) (samodistribucija - 1) (A—B)—((A—(B—C))—(A—C)) (samodistribucija - 2) (A—B)—(((A—B)—C)—-C)	(restriktivna asercija)
((A—»A)—»B)—»B	(specializirana asercija)
(B—*A)—"((A—"B)—»(B—"A))	(cikličnost)
itd.
Navedene in še druge teoreme sistema E__» najdemo v Entailment, str. 26, 77, 78 idr. In še nekaj zavrnjenih (gl. str. 18, 35 idr.) formul: (*) A »(B »A) (*) B »(A -A) (*) (A -A) »(B »B) (*) (A—B)—(B—B) (*) (A »B) »(A »A) (*) ((A »B) »A) -A itd.
Vidimo torej, da kriteriji oziroma algoritmi relevance delujejo selektivno v formalnem sistemu, tako da iz njega izločijo vse tiste formule, ki so v logiki sledenja kot
implikacije nerelevantne, tj. ne nastopajo kot teoremi. Za "pozitivno" opredelitev relevance pa je potrebna analiza dokaza. Sistemi logike relevance prav gotovo predstavljajo nove "modele racionalnosti" na področju logike.
CITIRANA LITERA TURA
1.	Ackermann, Wilhelm: "Begriindung einer strenger Implikation", The journal of symbolic logic, zv. 21. št.
2 (1956).
2.	Anderson, A.R. & Belnap, N.D.: "Entailment - the logic of relevance and necessity", zv. I. (Princeton Univ.
Press, 1975); zv. II.: Anderson & Belnap & Dunn J.Michael etal.Je pred nedavnim (1990) izšel pri isti založbi.
3.	Baylis, Charles A.: "Implication and subsumption", Monist, 1933.
4.	Bennett, Jonathan: "Meaning and implication", Mind št. 63,1954.
5.	Duncan-Jones, A.E.: "Is strict implication the same as entailment?", Analysis, 1935.
6.	Hughes,G.E. & Cresswell, MJ.: "An introduction to modal logic", Methuen, I^ondon, 1968; druga izdaja
1972.
7.	Lewis, Clarence Irving: "A survey of symbolic logic", 1918; druga, skrajšana izd.: Dover Publ., New York,
1959.
8.	Lewis, CI. & Langford, C.H.: "Symbolic logic", 1932; druga izd.: Dover Publ., New York, 1959.
9.	Lukasiewicz, Jan: "Elementy logiki matematycznej", predavanja 1928-1929, v knjigi prvič izšlo: Warszawa,
1939, polj. ponatis 1958; tukaj cit. po angl. prev. "Elements of mathematical logic", Pergamon Press, Oxford, 1963.
10.	Meyer, Robert: "A farewell to entailment", vzborniku "Foundations of logic and linguistics", uredn. Dorn
& Weingartner, Plenum Press, New York, London, 1985.
11.	Nelson, Everett J.: "Intensional relations", Mind, zv. 39,1930.
12.	Norman, Jean & Sylvan, Richard (ur.): "Directions in relevant logic", Kluwer Academic Publ., Amster-
dam, 1989.
13.	Prior, Arthur N.: "Facts, propositions and entailment", Mind, 1948.
14.	Routley, Richard et al.: "Relevant logics and their rivals", zv.I., Ridgeview Publ. Comp., Atascaredo, USA.,
1982.
15.	Sugihara, Takeo: "Strict implication free from implicational paradoxes", 1955; cit. po Anderson & Belnap
(1975).
16.	Tarski, Alfred: "Der Wahrheitsbegriff in den formalisierten Sprachen" (1933), angl. prev. v izbranem
delu Tarskega "Logics, semantics, metamathematics", Oxford Univ. Press, 1956.
17.	Uršič, Marko: "Matrice logosa", DZS, Ljubljana, 1987.
18.	Uriič, Marko: "Implikacija in logična nujnost", doktorska disertacija, Ljubljana, 1990.