Freedom and enforcement in action. A study in formal action theory (Q2018240)

Chapter 1 defines the notion of an \textit{elementary action system} as a triple of the form \((W,R,{\mathcal{A}})\) where \(R\) is a binary relation on \(W\), the set of \textit{states}, and \({\mathcal{A}}\) is a nonempty set of binary relations on \(W\) each of whose members is called an \textit{atomic action}. A number of examples are provided, one of which is washing a bed linen in an automatic washing machine (the following description is slightly adapted from the one provided). Let \(\alpha\), \(\beta\) and \(\gamma\) denote the sentences ``the bed linen is washed'', ``the linen is in the machine'', and ``the machine is turned on'', respectively. For all members \(\sigma\) of \(\{0,1\}^3\) of the form \(abc\), let \(w_\sigma\) be the state denoting the situation where \(\alpha\), \(\beta\), \(\gamma\) holds iff \(a\), \(b\), \(c\) are equal to 1, respectively. Then \(W\) is set to \(\bigl\{w_\sigma\mid\sigma\in\{0,1\}^3\bigr\}\). The relation \(R\) is meant to capture all transitions from one state to another that are not ruled out (because they are physically impossible, or unwanted, \dots). With this example, \(R\) is defined as a set of 14 elements, containing in particular \((w_{000},w_{010})\) -- if the bed linen is not washed, it is not in the machine and the machine is turned off, then one can put the bed linen in the machine -- and \((w_{011},w_{111})\) -- if the bed linen is not washed, it is in the machine and the machine is turned on, then the bed linen can get washed. As for \({\mathcal{A}}\), it is defined as the set consisting of the 5 actions meant to capture the actions of putting the bed linen into the machine, taking the bed linen out of the machine, turning the machine on, turning the machine off, and washing the bed linen, respectively, with for instance turning the machine on defined as the set consisting of the 4 pairs of the form \((w_{ab0},w_{ab1})\). A number of properties of elementary action systems are defined, in particular: {\parindent=6mm \begin{itemize} \item[--] \textit{separative} if two actions are disjoint; \item [--] \textit{normal} if every action is included in \(R\); \item [--] \textit{deterministic} if every action is functional. \end{itemize}} The notion of \textit{performability} of an action \(A\) in a state \(u\) is defined as the existence of a state \(w\) such that \((u,w)\) belongs to both \(A\) and \(R\), whereas \(A\) is \textit{totally performable} in state \(u\) iff \((u,w)\in R\) for all states \(w\) with \((u,w)\in A\). A sequence of performable actions can then satisfy a \textit{task}, defined as a pair whose members are subsets of \(W\), the sets of \textit{initial} and \textit{terminal conditions}, respectively, by leading from an initial state to a final state. Generalisation to probabilistic elementary action systems is discussed. The relationship to regular automata over a set \(\Sigma\) of nonterminals is established, which is immediate by taking for \({\mathcal{A}}\) the set of all sets of the form \(A_a\) with \(a\in\Sigma\), consisting of all pairs \((w,w')\) such that there is a transition from state \(w\) to state \(w'\) labeled with \(a\), and defining \(R\) as \(\bigcup_{a\in\Sigma}R_a\). The chapter ends with a relationship to programs viewed semantically. For instance, given a set \(\Phi\) of states and an action \(A\), ``while \(\Phi\) do \(A\)'' can be identified as the set of all sequences of states of the form \((w_0,w_1,\dots, w_{m+1})\) such that for all \(i\leq m\), \((w_i,w_{i+1})\in A\), \(w_0\), \dots, \(w_m\) all belong to \(\Phi\), and \(w_{m+1}\notin\Phi\). The second chapter starts with a discussion on the game of noughts and crosses and the game of chess to justify the need for extending the notion of elementary action system to a framework in a way that can, in particular, account for players taking turns. The proposed extension is that of a \textit{situational action system}, one of whose particular cases is that of an \textit{iterative action system}. An iterative action system complements an elementary action system \((W,R,{\mathcal{A}})\) with an \textit{iterative algorithm}, that is, a quintuple of the form \(D=(W,V,\alpha,\omega,{ LA})\) where \(V\) is a finite set of so-called \textit{labels} containing \(\alpha\) and \(\omega\), the \textit{initial} and \textit{terminal} labels, respectively, and \textit{LA} is a finite subset of \(V\setminus\{\omega\}\times{\mathcal{A}}\times V\setminus\{\alpha\}\), whose members are called \textit{labeled atomic actions}. The set \(W\times V\) is then called the set of \textit{possible situations}: rather than moving from state to state, one moves from a situation \((u,a)\) to a situation \((w,b)\) provided that there exists an atomic action \(A\) such that \((a,A,b)\in{ LA}\) and \((u,w)\) belongs to both \(A\) and \(R\) -- a generalisation of the notion of performability of action \(A\). With the example of chess, (i) \(W\) is the set of chessboard configurations, (ii) \(R\) is the binary relation between two chessboard configurations as determined by the rules of chess, (iii) for each type \(A\) of chess pieces (e.g., rook), \({\mathcal{A}}\) contains the set of pairs of successive configurations \(A^{\mathrm{White}}\) and \(A^{\mathrm{Black}}\) as determined by a possible move of a piece of type \(A\) by the black or white player, respectively, (iv) \(V\) is the set \(\{\alpha,\omega,{\mathrm{BLACK}},{\mathrm{WHITE}}\}\), and (v) \textit{LA} contains, besides all triples involving the initial and final labels for the beginning and end of the game, all triples of the form \(({\mathrm{WHITE}}, A^{\mathrm{White}},{\mathrm{BLACK}})\) and \(({\mathrm{BLACK}}, A^{\mathrm{Black}},{\mathrm{WHITE}})\) where \(A\) is a type of chess pieces such as rook. One can then define the \textit{resultant relation} of \(D\) as consisting of all pairs of states \((u,w)\) for which there exists a finite sequence of states \(s_0\), \dots, \(s_n\) with \(a_0=u\) and \(w=s_n\), a sequence of labels \(l_1\), \dots, \(l_n\) with \(l_1=\alpha\) and \(l_n=\omega\), and a sequence of actions \(A_1\), \dots, \(A_{n-1}\) such that for all \(i<n\), one can move from situation \((s_i,l_i)\) to situation \((s_{i+1},l_{i+1})\) thanks to action \(A_i\). After these formal notions and related ones have been put in place, Chapter 2 establishes precisely the clear relationship between finite automata and iterative action systems. It then generalises the framework to a larger class of situational action systems than iterative action systems, essentially by letting \textit{LA} be a finite subset of \(V\setminus\{\omega\}\times{\mathcal{A}}\times V^\star\setminus\{\alpha\}\) (with \(V^\star\) denoting the set of finite sequences of members of \(V\)). Situations are then no longer pairs of the form \((w,a)\) but pairs of the form \((w,a_1\dots a_k)\) where \(a_1\dots a_k\in V^\star\) can play the role of a stack with \(a_1\) at the top of the stack if \(k\neq 0\). One then moves from a situation \((u,aa_1\dots a_k)\) to a situation \((w,b_1\dots b_{k'}a_1\dots a_k)\) provided that there exists an atomic action \(A\) such that \((a,A,b_1\dots b_{k'})\in{ LA}\) and \((u,w)\) belongs to both \(A\) and \(R\). The clear relationship with pushdown automata is established. After informal considerations on the notion of agent, the chapter ends with a way to extend the formalism and draw further relationships with games and winning strategies, cellular automata, and Hamiltonian equations provided that situational action systems be generalised to continuous systems. Chapter 3 extends the notions of elementary action system and situational action system to \textit{ordered} elementary action systems and situational action systems, respectively, adding an order relation \(\leq\) on the set of states, with \((W,\leq)\) possibly constrained in some way such as being \(\sigma\)-complete (which constrains every sequence \((x_i)_{i\in{\mathbb{N}}}\) of members of \(W\) such that \(x_i\leq x_{i+1}\) for all \(i\in{\mathbb{N}}\) to have a least upper bound). Most of the chapter exposes standard material on partially ordered sets and fixed-point theorems, equivalent or not to the axiom of choice, and various other set- or model-theoretic results stated or proved. In particular, this chapter includes the traditional proof based on the back-and-forth method that two countable linear dense orders without endpoints are isomorphic, with a relationship to situational action systems by taking as situations pairs of the form \((u,\mathrm{FORTH})\) or \((u,\mathrm{BACK})\) with \(u\) a partial isomorphism. There is also a proof of the downward Löwenheim-Skolem-Tarski theorem that if \(\mathbf{A}\) is a model of a countable language \(L\) of cardinality \(\alpha\) and \(X_0\) is a subset of the domain of \(\mathbf{A}\) of infinite cardinality \(\beta\leq\alpha\), then \(\mathbf{A}\) has an elementary submodel of cardinality \(\beta\) whose domain contains \(X_0\). The proof makes use of one of the fixed-point theorems provided in the first part of the chapter in a way that establishes some relationship to ordered elementary action systems, by {\parindent=6mm \begin{itemize} \item[--] taking for \(W\) the set of subsets of the domain of \(\mathbf{A}\) that contain \(X_0\) and of cardinality \(\beta\), \item [--] taking for \(\leq\) the subset relation, \item [--] taking for \(R\) the set of all \((X,Y)\in W^2\) such that for all \(L\)-formulas \(\Phi(x,x_1,\dots,x_n)\) and members \(a_1\), \dots, \(a_n\) of \(X\), if \(\mathbf{A}\models\exists x\Phi(a,a_1,\dots,a_n)\) then there exists \(a\in Y\) with \(\mathbf{A}\models\Phi(a,a_1,\dots,a_n)\), \item [--] the previous condition on \(\Phi(x,x_1,\dots,x_n)\) defining the atomic action \(A_\Phi\), then taking for \(\mathcal{A}\) the set of all \(A_\Phi\) with \(\Phi\) an \(L\)-formula. \end{itemize}} Chapter 4 starts with general considerations on the concept of norm before applying it to actions and introducing, w.r.t. an elementary action system \((W,R,{\mathcal{A}})\), an action \(A\in{\mathcal{A}}\) and a state \(u\in W\), the formal notions of: {\parindent=6mm \begin{itemize} \item[--] \(A\) being \textit{\(R\)-permitted} in \(u\) iff there is \(w\in W\) with \(uRw\) and \(uAw\); \item [--]\(A\) being \textit{\(R\)-forbidden} in \(u\) iff there is no \(w\in W\) with \(uRw\) and \(uAw\); \item [--] \(A\) being \textit{\(R\)-obligatory} in \(u\) iff \(uRw\) for some \(w\in W\) and for all \(w\in W\), if \(uRw\) then \(uAw\). \end{itemize}} An example of obligatory actions is provided with as actions, turning left, turning right or going straight at a crossroads: such an action is obligatory if the driver can and has no other option but take the associated direction. A logical language and logical interpretations of the form \((W,R,V_0,V_1)\) is proposed where \(V_0\) maps a sentential sentence \(p\) to the set of states where \(p\) holds, \(V_1\) maps an action to the member of \({\mathcal{A}}\) that defines it, three deontic symbols, \(\mathbf{P}\), \(\mathbf{F}\) and \(\mathbf{O}\) being interpreted as described above. Formulas of the form \(\Phi\rightarrow\mathbf{P}a\), \(\Phi\rightarrow\mathbf{F}\alpha\) and \(\Phi\rightarrow\mathbf{O}\alpha\) then express that in a state where \(\Phi\) holds, action \(\alpha\) is permitted, forbidden or obligatory, respectively, and are claimed to capture the corresponding norms. Using standard technique, a completeness result is shown based on a proof system that besides classical propositional axioms and inference rules, contains all axioms of the form \(\mathbf{O}\alpha\rightarrow\mathbf{P}\alpha\) (what is obligatory is permitted) and all axioms of the form \(\mathbf{F}\alpha\leftrightarrow\neg\mathbf{P}\alpha\) (being forbidden is not being permitted). The \textit{closure principle}, namely, the implication \(\neg\mathbf{F}\alpha\rightarrow\mathbf{P}\alpha\), is then questioned, giving rise to a weaker system whose semantics is defined in terms of \textit{open} action systems, of the form \((W,R^+,R^-,{\mathcal{A}})\): \(R^+(u,w)\) expresses that the transition from \(u\) to \(w\) is certain, while \(R^-(u,w)\) expresses that the transition from \(u\) to \(w\) is excluded with certainty. The notions of an action being permitted, forbidden or obligatory are redefined accordingly, and a second completeness result is proven. A section is dedicated to compound actions -- sequences of actions replacing single actions --, which give even greater latitude in defining the three norms. \textit{Righteous} systems of atomic norms are defined, which essentially capture the situation where the propositions \(\Phi\rightarrow\mathbf{P}a\), \(\Phi\rightarrow\mathbf{F}\alpha\) and \(\Phi\rightarrow\mathbf{O}\alpha\) are true at all states. The chapter ends with more general considerations. Chapter 5 discusses the \textit{stit} (for ``See To It That'') semantics, aimed at giving formal meaning to statements of the form: agent \(a\) sees to it that \(\phi\). Starting with a \textit{branching system}, that is, a pair \((W,\leq)\) where \(\leq\) is an order relation on \(W\) such that for all \(w\in W\), \(\{u\in W\mid u\leq w\}\) is totally ordered, \textit{indexes} are defined as pairs denoted \(u/h\) that represent a point in time \(u\) (a member of \(W\)) in a possible history \(h\) (a maximal chain in \((W,\leq)\)). Formulas are evaluated in this framework with a valuation \(V\) -- a function from formulas to indexes --, that makes it possible to express a number of notions, such as: {\parindent=6mm \begin{itemize} \item[--] ``it was the case that \(\phi\)'', or \(P\phi\) (with \(P\) for ``past''), whose interpretation \(V(P\phi)\) is the set of indexes \(u/h\) for which there exists \(u'<u\) with \(u'/h\in V(\phi)\); ``it will be the case that \(\phi\)'', or \(F\phi\) (with \(F\) for ``future'') is interpreted similarly; \item [--] ``\(\phi\) is settled'', or \(\square\phi\), whose interpretation \(V(\square\phi)\) is the set of indexes \(u/h\) such that all indexes of the form \(u'/h\) belong to \(V(\phi)\); ``it is still open that \(\phi\)'', or \(\lozenge\phi\) is interpreted similarly. \end{itemize}} Such branching systems are extended to \textit{stit frames} with the addition of two sets \textit{Agent} and \textit{Choice}, the latter assigning to each agent \(a\) and state \(u\) a partition \(\mathit{Choice}^u_a\) of all indexes of the form \(u/h\) (\(u\) and any history that goes through it). This allows one to extend \(V\) to interpretations of formulas of the form \([a\;\mathit{cstit}:\phi]\) (\(c\) is for Chellas) that consist of all indexes \(u/h\) such that the member of the partition \(\mathit{Choice}^u_a\) to which \(u/h\) belongs is a subset of the set of all indexes of the form \(u/h\) which make \(\phi\) true according to \(V\). Then stit frames are reconstructed as action systems thanks to a sightly intricate construction, before moving on to more general considerations on the ``it ought to be'' operator. The last chapter is about knowledge, and borrows bits and pieces from modal logics of knowledge, common knowledge, dynamic epistemic logic, the frame problem, nonmonotonic reasoning, preference frames and more, mostly semi-formally. The relationship to action systems is essentially in the last section with definitions on a notion of ``rule of conduct''. The end of Section 6.3.2 summarises the tone of the chapter: \textit{How should the above semantics be combined with action theory? A realistic theory of action should not assume the omnipotence and omniscience of agents. Some natural limitations should be assumed \([...]\) Any reasonable theory should not ignore these aspects of action; it should however point the sources of the problem and repair work}. It is difficult to see how a very generic framework could solve problems and fix the issues of more specialised formalisms. When one finishes the book, one has the impression that the aim was to cast by all means all kinds of frameworks into the formalism of action systems, which often has to be done awkwardly, incurring oversimplifications, and yielding no insight whatsoever on the framework being cast. There is a plethora of definitions, sometimes with a sense of arbitrariness, especially when they are some of many alternatives, and very few results, almost all of which are rather immediate observations. Unifying, casting many theories in a common framework is a noble aim, but the reader cannot fail to feel that action systems might not be natural, powerful and fruitful enough to unify so many frameworks, and that the book lacks coherence, touching on so many concepts from so many fields, sometimes only sketched, sometimes developed more -- possibly with reminders and proofs on some of their results --, jumping from concept to concept. Still readers are likely to discover notions and formalisms that can potentially pike their interest, independently of whether further research will be from the point of view of action systems or within those formalisms themselves.