STUDIES IN LOGIC, GRAMMAR AND RHETORIC 1 (14)

Anna Zalewska

THE NORMS FROM THE POINT OF VIEW OF A CERTAIN LOGIC OF PROGRAMS

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.

1

Stig Kanger in his article Law and Logic wrote 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

– von Wright’s logic of actions (orders and prohibition) ([4]),

– Hoare’s logic as the least logic among logic of programs ([1]),

– Wolniewicz’s ontology of situation ([3]). In Hoare’s logic we deal with the formulas α{M}β that we understand in the following way: if the formula α is satisfied then the formula β is satisfied after execution of the program M. If we exchange the program M for the norm N then we can read the formulas α{N}β in the following way: if the formula α describes the situation before application of the norm N then the formula β describes the situation after application of the norm N. For example:

The child is hungry {Feed the child} The child is fed.

Anna Zalewska

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.

2.

The alphabet of the language of norms consists of the following sets:

V_{0} – an enumerable set of propositional variables such that for some set I

V_{0} = ⋃_{i∈I} K_{i}

where {K_{i}}_{i∈I} is a family of sets of propositional variables satisfying the following conditions:

(1) K_{i} ∩ K_{j} = ∅ when i ≠ j’

(2) K_{i} is finite,

(3) K_{i} is at least one element set; the propositional variables will be denoted by the letter p with double indexes i.e. for example P_{i2} ∈ 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},

{¬, ∨, ∧, ⇒} – the set of logical connectives,

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,

Id – norm constant (intuitively representing the action “Do nothing”),

{ not −, begin −; − end, if − then − else − fi} – the set of connectives of norms (prohibition norm, complex norm, condition norm),

{(,)} – the set of auxiliary signs.

3.

The set of all elementary situations S_{E} is the least extention of the set V_{0} such that if α ∈ S_{E}, p_{ij} ∈ V_{0} and for each element p_{lk} occuring in α holds if i ≠ l then α∧p_{ij} ∈ S_{E} (S_{E} intuitively represents Wolniewicz’s elementary situation).

The set of all norms 𝒩 is the least extension of the set V_{n} and norm constant Id such that if γ is a formula γ ∈ S_{E} and N_{1}, N_{2} are norms then the expressions not N_{1}, begin N_{1}; N_{2} end, if γ then N_{1} else N_{2} fi, are norms.

The norms from the point of view of a certain logic of programs

The set of all formulas F_{AN} is the least extension of the set S_{E} such that

1) if α, β ∈ S_{E} and N is a norm then α{N}β is a formula,

2) if α, β ∈ F_{AN} then (α ∨ β), (α ∧ β), (α ⇒ β), ¬α are formulas. Let α ⇔ β will be an abbreviation of the following expression (α ⇒

β) ∧ (β ⇒ α). Let α¯∨β will be an abbreviation of the following expression (α ∧ ¬β) ∨ (¬α ∧ β).

4.

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.

Ax1. The schema of tautologies of classical propositional calculus

Ax2. p_{i1} ¯∨p_{i2} ¯∨ … ¯∨p_{ij_{i}−1} ¯∨p_{ij_{i}} where j_{i} is a number of elements of the set K_{i}

Ax3. α{Id}α

Ax4. α{N}β ∨ α{ not N }β ⇒ (α{ not N }β ⇔ ¬(α{N}β))

Ax5. α{if γ then N_{1} else N_{2} fi}β ⇔ (γ ⇒ α{N_{1}}β) ∧ (¬γ ⇒ α{N_{2}}β)

Ax6. α{N_{1}}β ∧ β{N_{2}}δ ⇒ α{begin N_{1}; N_{2} end}δ

Ax7. α{N}β ∧ α{N}δ ⇒ α{N}(β ∧ δ)

In order obtain a certain calculus for algorithmic norms we can add the following two rules to the axioms:

R1: \frac{α, α ⇒ β}{β}

R2: \frac{α ⇒ α′, α′\{N\}β′, β′ ⇒ β}{α\{N\}β}

5.

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:

(1) Some additional norms connectives:

α{N_{1} or N_{2}}β ⇔ α{N_{1}}β ∧ α{N_{2}}β

α{either N_{1} or N_{2}}β ⇔ α{N_{1}}β ∨ α{N_{2}}β α{N_{1} and N_{2}}β ⇔ α{begin N_{1}; N_{2} end}β ∨

α{begin N_{2}; N_{1} end}β

(2) An extension of the notion of the set S_{E} by special situation all (any situation of our choice from the set S_{E} no matter which one) S′_{E} = S_{E} ∪ {all}

α ∧ (all{N}β) ⇒ α{N}β
(α{N}all) ∧ β ⇒ α{N}β

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.

References

[1] Hoare, C.A.R.: An Axiomatic Basis for Computer Programming, Comm. ACM 12, 1969, pp 576-580, 583

[2] Malec, A.: Norms and Programs, here

[3] Wolniewicz, B.: On Ontology of Situation, Warszawa, 1985

[4] von Wright, G.H.: Norm and Action, London, 1963