\input stf \def\NieparzystyHead{\line{\hfill\HeaderFont The norms from the point of view of a certain logic of programs}} \def\ParzystyHead{\line{\HeaderFont Anna Zalewska\hfill}} \startpageno=101 \pageno=\startpageno \pu\pu\pu \pretolerance=10000 \lasta Anna Zalewska\\ %%\a University in Bialystok\\ \t THE NORMS FROM THE POINT OF VIEW \\ \lastt OF A CERTAIN LOGIC OF PROGRAMS \\ \def\rrr #1\\{\pu\pu\centerline{\bf #1}\pu} \def\rrrr #1\\{\pu\centerline{\bf #1}} \def\rrrrbezpu #1\\{\centerline{\bf #1}} \def\<{\langle} \def\>{\rangle} \def\name#1{\bigskip\line{#1\hfill}} \def\zero{\hbox{\bf 0}} \def\one{\hbox{\bf 1}} \font\gothic=eufm10 \font\mgothic=eufm7 \font\mmgothic=eufm5 \font\pisane=eusm10 \font\mpisane=eusm7 \font\msam=msam10 \font\eurb=eurb10 \def\true{\hbox{\bf true}} \def\false{\hbox{\bf false}} \def\IF{\hbox{\rm IF}} \def\Begin{\hbox{\it begin~}} \def\End{\hbox{\it ~end}} \def\If{\hbox{\it if~}} \def\Then{\hbox{\it ~then~}} \def\Else{\hbox{\it ~else~}} \def\Fi{\hbox{\it ~f{}i}} \def\While{\hbox{\it while~}} \def\Do{\hbox{\it ~do~}} \def\Od{\hbox{\it ~od}} \def\Not{\hbox{\it ~not~}} \def\gotM{\hbox{\gothic M}} \def\gotB{\hbox{\gothic B}} \def\mgotM{\hbox{\mgothic M}} \def\mmgotM{\hbox{\mmgothic M}} \def\pisN{\hbox{\pisane N}} \def\pisC{\hbox{\pisane C}} \def\pisE{\hbox{\pisane E}} \def\pisI{\hbox{\pisane I}} \def\pisP{\hbox{\pisane P}} \def\mpisP{\hbox{\mpisane P}} \let\Stopien=\circ \def\stopien{^\Stopien} \let\limp=\Rightarrow \let\bigpi=\prod \let\Over=\slash \def\kwadrat{\hbox{\msam\char3}} \def\Q{\hbox{\eurb Q}} \def\Lemma #1 {\noindent {\bf Lemma #1~~}} \def\Proof.{\noindent {\bf Proof.}~~} \def\Definition #1 {\noindent {\bf Definition #1}~~} \def\Theorem #1 #2\\ #3\par{\noindent {\bf Theorem #1}~~#2\hfill\break #3\par} \def\Corollary #1\\ #2\par{\noindent {\bf Corollary #1}\hfill\break #2\par} \def\CBDO{\par\line{\hfill\msam\char3}} \def\CBDOg{\par\vskip-\baselineskip\line{\hfill\msam\char3}} \def\cbdo{\hbox{\msam\char3}} \def\jedna #1.#2||#3*{ \line{% \hbox to .2\hsize{#1\hfill}\hbox to.8\hsize{$\displaystyle{#2\over#3}$\hfill}\hss}% \medskip } \def\jednadol #1.#2||#3*#4*#5*{ \line{% \hbox to .2\hsize{#1\hfill}\hskip#5\hbox to.8\hsize{$\displaystyle{#2\over\vbox{\hbox{$#3$}\hbox{$#4$}}}$\hss}\hss}% \medskip } \def\jednaprzesunieta #1.#2||#3*#4*{ \line{% \hbox to .2\hsize{#1\hfill}\hskip#4\hbox to.8\hsize{$\displaystyle{#2\over#3}$\hss}\hss}% \medskip } \def\dwie #1.#2||#3* #4* #5.#6||#7*{ \medskip \line{% \hbox to .1\hsize{#1\hfill}\hbox to.35\hsize{$\displaystyle{#2\over#3}$\hfill}% \hfill #4\hfill \hbox to .1\hsize{#5\hfill}\hbox to.35\hsize{$\displaystyle{#6\over#7}$\hfill}}% \medskip } \vskip-\baselineskip \Abstract. In the paper some logical tools for norms (based on logic of programs) are given. It allows us to express some properties of norms and to state some relations between them. \\ \rcenterbezpu 1\\ Stig Kanger in his article {\it Law and Logic} wrote {\it The combination of law and logic is highly problematic, and the results are few and far between. One of the reasons for this is that very few logicians are interested in law, and very few jurists are interested in logic. Moreover, the purpose of such a combination, as well as suitable approaches to the study of it, is a bit unclear}. Next he mentioned that it appeared suitable to start with problems that are relevant for the creation of well-written systems of law. The purpose of the paper is to give some logical tools that allow us to express some properties of norms and to state some relations between them in a formal way. We shall discuss norms from the point of view of a certain logic of programs. The general idea is based on combining the following theories \item{--}von Wright's logic of actions (orders and prohibition) ([4]), \item{--}Hoare's logic as the least logic among logic of programs ([1]), \item{--}Wolniewicz's ontology of situation ([3]). \noindent In Hoare's logic we deal with the formulas $\alpha\{M\}\beta$ that we understand in the following way: if the formula $\alpha$ is satisfied then the formula $\beta$ is satisfied after execution of the program $M$. If we exchange the program $M$ for the norm $N$ then we can read the formulas $\alpha\{N\}\beta$ in the following way: if the formula $\alpha$ describes the situation before application of the norm $N$ then the formula $\beta$ describes the situation after application of the norm $N$. For example: \medskip \centerline{The child is hungry $\{$\hbox{\it Feed the child}$\}$ The child is fed.} \medskip \noindent In Hoare's logic beside simple programs there are complex ones constructed by some program connectives. We will use the program connectives to build more complicated norms. The nature of the norms constructed in this way is algorithmic. \rcenter 2.\\ The alphabet of the language of norms consists of the following sets: \medskip \noindent $V_0$ -- an enumerable set of propositional variables such that for some set I \smallskip \centerline{$V_0=\bigcup\limits_{i\in I} K_{i }$} \medskip \noindent where $\{K_{i}\}_{i \in I}$ is a family of sets of propositional variables satisfying the following conditions: (1) $K_{i} \cap K_{j} = \emptyset$ when $i \neq j$' (2) $K_{i}$ is finite, (3) $K_{i}$ is at least one element set; \noindent the propositional variables will be denoted by the letter p with double indexes i.e. for example $P_{i2} \in K_{i_{j}}$; if $j_{i}$ is a number of elements of $K_{i}$ then the set $\{p_{i1},p_{i2}, ... p_{ij_{i}-1},p_{ij_{i}}\}=K_{i}$, \medskip \noindent $\{\lnot,\lor,\land,\limp\}$ -- the set of {\it logical connectives}, \medskip \noindent $V_n$ -- an enumerable set of norm variables (intuitively representing simple closes); the norm variables will be denoted by the letter N with indexes if necessary, \medskip \noindent $Id$ -- {\it norm constant} (intuitively representing the action ``Do nothing"), \medskip \noindent $\{\Not - , \Begin - ; - \End, \If - \Then - \Else - \Fi \}$ -- the set of {\it connectives of norms} (prohibition norm, complex norm, condition norm), \medskip \noindent $\{(,)\}$ -- the set of {\it auxiliary signs}. \rcenter 3.\\ The set of all elementary situations $S_{E}$ is the least extention of the set $V_{0}$ such that if $\alpha \in S_{E}$, $p_{ij} \in V_{0}$ and for each element $p_{lk}$ occuring in $\alpha$ holds if $i \neq l$ then $\alpha \wedge p_{ij} \in S_{E}$ ($S_{E}$ intuitively represents Wolniewicz's elementary situation). The set of all {\it norms}~$\pisN$ is the least extension of the set~$V_n$ and norm constant~$Id$ such that if $\gamma$ is a~formula $\gamma\in S_{E}$ and $N_{1},N_{2}$ are norms then the expressions $\Not N_{1}$, $\Begin N_{1}; N_{2} \End$, $\If \gamma \Then N_{1} \Else N_{2} \Fi$, are norms. The set of all {\it formulas}~$F_{AN}$ is the least extension of the set~$S_{E}$ such that \item{1)}if $\alpha, \beta \in S_{E}$ and $N$ is a norm then $\alpha\{N\}\beta$ is a formula, \item{2)}if $\alpha, \beta \in F_{AN}$ then $(\alpha \lor \beta)$, $(\alpha \land \beta)$, $(\alpha \limp \beta)$, $\lnot\alpha$ are formulas. Let $\alpha \Leftrightarrow \beta$ will be an abbreviation of the following expression $(\alpha \limp \beta) \wedge (\beta \limp \alpha)$. Let $\alpha \bar\vee \beta$ will be an abbreviation of the following expression $(\alpha \wedge \neg \beta) \vee (\neg \alpha \wedge \beta)$. \rcenter 4.\\ \noindent The axioms given below are taken from Hoare's logic. Some of them (Ax3, Ax5 and Ax6) define norm connectives that are similar to program connectives. The axiom Ax4 is an attempt of describing the connective for prohibition norm. This connective has no counterpart in the logic of programs. The rest of the axioms are useful (in general) in formalization of a system of law. \medskip \smallskip \noindent Ax1. \noindent The schema of tautologies of classical propositional calculus \medskip \noindent Ax2. \noindent $p_{i1} \bar\vee p_{i2} \bar\vee \dots \bar\vee p_{ij_{i}-1} \bar\vee p_{ij_{i}}$ ~~~where $j_{i}$ is a number of elements of the set $K_{i}$ \medskip \noindent Ax3. \noindent $\alpha\{Id\}\alpha$ \medskip \noindent Ax4. \noindent $\alpha\{N\}\beta \vee \alpha\{\Not N~\}\beta \limp (\alpha\{\Not N~\}\beta \Leftrightarrow \neg(\alpha\{N\}\beta))$ \medskip \noindent Ax5. \noindent $\alpha\{\If \gamma \Then N_{1} \Else N_{2} \Fi\}\beta \Leftrightarrow (\gamma \limp \alpha\{N_{1}\}\beta) \wedge (\neg\gamma \limp \alpha\{N_{2}\}\beta)$ \medskip \noindent Ax6. \noindent $\alpha\{N_{1}\}\beta \wedge \beta\{N_{2}\}\delta \limp \alpha\{\Begin N_{1} ; N_{2} \End\}\delta$ \medskip \noindent Ax7. \noindent $\alpha\{N\}\beta \wedge \alpha\{N\}\delta \limp \alpha\{N\}(\beta \wedge \delta)$ \medskip \smallskip \noindent In order obtain a certain calculus for algorithmic norms we can add the following two rules to the axioms: \eject \noindent R1: \vskip-\baselineskip \jedna~.\alpha, \alpha\limp\beta||\beta* \pu \noindent R2: \vskip-\baselineskip \jedna~.\alpha\limp\alpha', \alpha'\{N\}\beta', \beta'\limp\beta||\alpha\{N\}\beta* \pu \noindent \rcenter 5.\\ \noindent The above-mentioned axioms and rules can be enriched by additional extensions of the set of norms connectives and notion of the set $S_{E}$ in the following way: \item{(1)}Some additional norms connectives: \smallskip \itemitem{}$\alpha\{N_{1}~ \hbox{\it or} ~N_{2}\}\beta \Leftrightarrow \alpha\{N_{1}\}\beta \wedge \alpha\{N_{2}\}\beta$ \smallskip \itemitem{}$\alpha\{\hbox{\it either}~ N_{1}~ \hbox{\it or}~ N_{2}\}\beta \Leftrightarrow \alpha\{N_{1}\}\beta \vee \alpha\{N_{2}\}\beta$ \smallskip \itemitem{}$\alpha\{N_{1}~ \hbox{\it and} ~N_{2}\}\beta \Leftrightarrow \alpha\{\Begin N_{1} ; N_{2} \End\}\beta~ \vee$ \noindent ~~~~\kern-2mm ~~~~~$~~~~~~~~~~~~~~~~~~~~~~~~~~~~~\alpha\{\Begin N_{2} ; N_{1} \End\}\beta$ \smallskip \item{(2)}An extension of the notion of the set $S_{E}$ by special situation {\it all} (any situation of our choice from the set $S_{E}$ no matter which one) $S_{E}'=S_{E} \cup \{${\it all}$\}$ \smallskip \itemitem{}$\alpha \wedge (\hbox{\it all}\{N\}\beta) \limp \alpha\{N\}\beta$ \smallskip \itemitem{}$(\alpha\{N\}\hbox{\it all}) \wedge \beta \limp \alpha\{N\}\beta$ \rcenter 6.\\ In the paper some logical tools for norms (based on logic of programs) are given. It allows us to express properties of norms and to state some relations between them. In [2] the explications of some concepts of the theory of law are given. They base on described here concept of norms. \pu \rbezpu References\\ \item{[1]}Hoare, C.A.R.: {\it An Axiomatic Basis for Computer Programming}, Comm. ACM 12, 1969, pp 576-580, 583 \item{[2]}Malec, A.: {\it Norms and Programs}, here \item{[3]}Wolniewicz, B.: {\it On Ontology of Situation}, Warszawa, 1985 \item{[4]}von Wright, G.H.: {\it Norm and Action}, London, 1963 \end