Uvod
Isfrustiran sam.Više puta sam razgovarao sa pravnicima koji su mi pričali o idealu pravde, koji, (po definiciji) ne možemo da dostignemo, ali (po prirodi) moramo da mu težimo. Neka ideja je da za svaki problem postoji savršeno pravedna odluka kao razrešenje, i pravni sistem bi trebalo da teži ka tome da obezbedi proces donošenja odluke koji omogućava dolaženje do ideala.
Prirodno, moje prvo podpitanje je - kako to da konačnu odluku u pravosudnom sistemu bez izuzetka donose ljudi, i to pritom eksplicitno u skladu sa svojom savešću? Meni to deluje kao teženje u sasvim suprotnom pravcu od ideala, pošto su ljudi inherentno grešni1. Tipičan odgovor se svodi na sleganje ramenima i mumlanje odgovora oblika: "moramo s nečim da se snađemo". Ok.
Kratka digresija - čitava situacija me zapravo asocira na krizu softverske industrije. Ovde nije u pitanju moderna kriza - naime, radi se o problemu o kojem je Dijkstra pričao još daaaaaaavno davno (fazon pre skoro pola veka) u svojim najranijim EWD-ovima2. Ispostavi se da je moderan softver toliko kompleksan da neformalan "ad-hoc" pristup pisanju softvera koji je industrija preuzela može da proizvede u najboljem slučaju softver za koji znamo da ima greše, nikako softver koji ih nema. Trenutno imamo takav razvojni proces da većinu vremena nismo skroz sigurni šta radimo. Čak i softver koji se izvršava u superkritičnim uslovima ume da ima defekte (sa kojom god iole racionalnom definicijom pojma). Ovde bi naš pravnik sa početka teksta ponovo slegnuo ramenima, kao što su učinili i brojni programeri, poslodavci i korisnici. Za to vreme, Dijkstra je u svojoj učionici revnosno pokazivao da korektan softver nije ideal - čovečanstvo poseduje neophodne alate za savladavanje kompleksnosti ... u matematici.
Neću ulaziti u Dijkstrino pokazivanje korektnosti kompleksnih programa (trivijalne smo savladali i bez njega). Ovaj tekst sam i počeo da pišem zato što mi je relativno skoro došlo do šaka parče zakona o zaštiti uzbunjivača. Oduvek mi je malo bolo oči to što pravni tekstovi pokušavaju da budu jednoznačni, ali u startu su dizajnirani tako da to ne budu. Kao da su ih pisali isti ljudi koji su razmišljali o idealu Pravde. Matematički formalizmi nisu nova stvar. Bilo ko ko racionalno pristupi pisanju teksta koji treba da bude jednoznačan ne bi smeo da uzme prirodni jezik kao svoj primarni alat. Prirodni jezici su maltene dizajnirani (evolutivno) tako budu sve samo ne jednoznačni. Ako neko pokuša da mi argumentuje da je pravni tekst pisan prirodnim jezikom da bismo svi mi smrtnici mogli da ih razumemo, predložio bih mu da pročita pomenuti zakon o uzbunjivaču prosečnom fakultetskom amfiteatru, i da trivijalno propita slušaoce nakon čitanja o njihovim pravima. Iracionalno je uopšte pokušavati obezbediti laku razumljivost pravnog teksta - pravni tekst je kompleksna forma, i zahteva veliko angažovanje za razumevanje. Korišćenje prirodnog jezika pomaže neznatno.
Sa svime ovime kao uvodom, nudim prvi nacrt prevoda tek par članova Zakona o uzbunjivaču na adekvatniji zapis3:
$FL$ - skup fizičkih lica
$PL$ - skup pravnih lica
$L = FL \cup PL$ - "lice" je pravno lice ili fizičko lice
$Ov$ - skup svih mogućih ovlašćenja za proizvoljno lice
$O$ - skup opšte štete (opasnost po život, šteta većih razmera, ...)
$KrProp_{test}: L \times FL \rightarrow Bool$ - funkcija koja proverava da li je dato lice izvršilo kršenje propisa prema datom fizičkom licu
$KrPrav_{test}: L \times FL \rightarrow Bool$ - funkcija koja proverava da li je dato lice izvršilo kršenje ljudskih prava datog fizičkog lica
$KrOvl_{test}: L \times Ov \rightarrow Bool$ - funkcija koja proverava da li je dato lice primenilo dato ovlašćenje protivno svrsi ovlašćenja
$O_{test}: L \times O \rightarrow Bool$ - funkcija koja proverava da li je dato lice na neki način načinilo opštu štetu
$InfoUzb: L \times FL \rightarrow Bool$ - funkcija koja proverava da dato fizičko lice zapravo poseduje informaciju o uzbunjivanju povezanu sa datim licem u kontekstu radnog angažovanja, zapošljavanja, ...
\begin{equation}
UInfo: \exists l \in L, \forall ov \in Ov, \forall o \in O, \exists fl \in FL: \\ (KrProp_{test}(l, fl) \lor KrLjPrav_{test}(l,fl) \lor KrOvl_{test}(l, ov) \lor O_{test}(l, o)) \land \\ InfoUzb(l, fl)
\end{equation}
\begin{equation}
UInfo_{test}: Fl \times UInfo \rightarrow Bool
\end{equation}
Ako funkcija $(2)$ instanciranjem konkretnog fizičkog lica kao uzbunjivača i konkretne informacije o uzbunjivanju daje rezultat $\top$, onda možemo da smatramo da su zadovoljeni uslovi za primenu zakona.
Očigledno je da ovde nije u pitanju matematička logika, već sistem koji je zasnovan na njoj. Npr. pojmovi "teorema", "aksiom" i "funkcija" su blago prilagođeni za potrebe primene u pravosuđu. U pitanju je taktika koju je koristio i Dijkstra. Radi. Mada, za njenu primenu je neophodno dosta discipline i rigoroznosti - kao što bi i trebalo da bude slučaj kod nečega tako ozbiljnog kao što je Pravda.
Iako primer nije kompletan, postaje jasno da je jednoznačnost osigurana ovakvim pristupom. Dodatna poboljšanja kompletnog pravosudnog sistema koja bi direktno sledila su:
Original (odlomak)
Glava I, Član 2:Već ovde vidimo probleme koje će formalan jezik inherentno rešiti:
1) "uzbunjivanje" je otkrivanje informacije o kršenju propisa, kršenju ljudskih prava, vršenju javnog ovlašćenja protivno svrsi zbog koje je povereno, opasnosti po život, javno zdravlje, bezbednost, životnu sredinu, kao i radi sprečavanja štete većih razmera;
2) "uzbunjivač" je fizičko lice koje vrši uzbunjivanje u vezi sa svojim radnim angažovanjem, postupkom zapošljavanja, korišćenjem usluga državnih i drugih organa, nosilaca javnih ovlašćenja ili javnih službi, poslovnom saradnjom i pravom vlasništva na privrednom društvu;
- Operacija uzbunjivanja je definisana, a da nismo prethodno definisali skup nad kojim se ona primenjuje (iliti - ko je uzbunjivač). Naknadno definisanje ima smisla u prirodnom jeziku, ali je, sa formalnog stanovišta, apsurdno. Kao trivijalan misaoni eksperiment - pokušajte da objasnite kako funkcioniše množenje razlomaka, bez objašnjenja šta su razlomci.
- Javljaju se pojmovi koji su veoma problematični za tumačenje (npr. "šteta većih razmera", "opasnost po životnu sredinu").
- Da li operacija uzbunjivanja može da se primeni samo ako se uzbunjivanje vrši pod uslovima navedenim u 2)? Ako da, zašto to piše u 2), a ne u 1)? Ako ne, gde piše koji još uslovi mogu/treba da budu zadovoljeni da bi operacija važila kao uzbunjivanje? U ostatku zakona? U ostatku glasnika?
Aksiomi
$FL$ - skup fizičkih lica
$PL$ - skup pravnih lica
$L = FL \cup PL$ - "lice" je pravno lice ili fizičko lice
$Ov$ - skup svih mogućih ovlašćenja za proizvoljno lice
$O$ - skup opšte štete (opasnost po život, šteta većih razmera, ...)
$KrProp_{test}: L \times FL \rightarrow Bool$ - funkcija koja proverava da li je dato lice izvršilo kršenje propisa prema datom fizičkom licu
$KrPrav_{test}: L \times FL \rightarrow Bool$ - funkcija koja proverava da li je dato lice izvršilo kršenje ljudskih prava datog fizičkog lica
$KrOvl_{test}: L \times Ov \rightarrow Bool$ - funkcija koja proverava da li je dato lice primenilo dato ovlašćenje protivno svrsi ovlašćenja
$O_{test}: L \times O \rightarrow Bool$ - funkcija koja proverava da li je dato lice na neki način načinilo opštu štetu
$InfoUzb: L \times FL \rightarrow Bool$ - funkcija koja proverava da dato fizičko lice zapravo poseduje informaciju o uzbunjivanju povezanu sa datim licem u kontekstu radnog angažovanja, zapošljavanja, ...
Teoreme
\begin{equation}
UInfo: \exists l \in L, \forall ov \in Ov, \forall o \in O, \exists fl \in FL: \\ (KrProp_{test}(l, fl) \lor KrLjPrav_{test}(l,fl) \lor KrOvl_{test}(l, ov) \lor O_{test}(l, o)) \land \\ InfoUzb(l, fl)
\end{equation}
\begin{equation}
UInfo_{test}: Fl \times UInfo \rightarrow Bool
\end{equation}
Ako funkcija $(2)$ instanciranjem konkretnog fizičkog lica kao uzbunjivača i konkretne informacije o uzbunjivanju daje rezultat $\top$, onda možemo da smatramo da su zadovoljeni uslovi za primenu zakona.
Očigledno je da ovde nije u pitanju matematička logika, već sistem koji je zasnovan na njoj. Npr. pojmovi "teorema", "aksiom" i "funkcija" su blago prilagođeni za potrebe primene u pravosuđu. U pitanju je taktika koju je koristio i Dijkstra. Radi. Mada, za njenu primenu je neophodno dosta discipline i rigoroznosti - kao što bi i trebalo da bude slučaj kod nečega tako ozbiljnog kao što je Pravda.
Iako primer nije kompletan, postaje jasno da je jednoznačnost osigurana ovakvim pristupom. Dodatna poboljšanja kompletnog pravosudnog sistema koja bi direktno sledila su:
- Operacije koje mogu da se automatizuju bi bile programirane - one kod kojih to nije moguće bi morale ručno da se tumače, ali to deluje kao da bi trebalo da bude relativno mali procenat.
- Dobijamo pravni jezik koji je internacionalno razumljiv, razmenjiv, i koji bilo ko6 može da pročita.
- Matematičari bi bili tumači u sporovima, što je blizu idealnog - matematičari su skoro po definiciji razdvojeni od empatije.
- Argumentacija na sudu bi se svela na dokazivanje teorema.
- Elegantan zapis bi omogućio konstruisanje simbolički zapisane baze zakona, koja bi bila pretraživa. Bilo bi moguće vršiti proizvoljnu automatizovanu obradu nad zakonima, kao što je npr. simuliranje sistema zasnovanog na alternativnim aksiomima.
Zaključak
Malo manje sam isfrustriran sada.1 Ovde bih ponudio "To kill a mockingbird" kao dobar primer problema o kojem pričam.
2 EWD 340
3 Meni lično razumljiviji od originalnog, mada sam voljan da priznam da je to lična preferencija.
4 Prevod može biti netačan jer nisam pravnik i zapravo ne razumem najbolje sve detalje navedenog teksta; korekcije su dobrodošle.
5 Stavke koje su ovde navedene kao aksiomi pretpostavljamo da su ad-hoc istinite, ili da su drugde pokazane kao validne. Neke od njih su, naravno, daleko kompleksnije od posla koji ovde obavljamo. U svrhu konciznosti, težim da primer bude jednostavan i ilustrativan, a ne kompletan. Svakako ne možemo imati oba.
6 Bilo ko ko razume elementarnu matematičku logiku.
No comments:
Post a Comment