In the two previous parts of this paper [Reference Fine8, Reference Fine9], I developed a truthmaker semantics for the logic of categorical imperatives and for the logic of categorical obligation. In the present part, I wish to extend the previous accounts to allow for the introduction of conditional imperatives, of the form ‘if S then do X’. Conditional locutions of this form are clearly of great importance since, in telling someone what to do, we will often want to make what we prescribe conditional on how things are or on how else the agent has acted. In the present part, I shall be almost exclusively concerned with the question of equivalence—of when two imperatives can be taken, on logical grounds alone, to have the same content. This means that one can also extract an account of validity in the sense of containment, since one imperative $\mathrm{Y}$ can be said to contain another $\mathrm{X}$ when it is of the form $\mathrm{X}\wedge \mathrm{Z}$ for some imperative $\mathrm{Z}$ . However, it is not possible in the same way to extract an account of the validity of ‘mixed’ inferences, as when one argues from the indicative S and the conditional imperative ‘if $\mathrm{S}$ then $\mathrm{X}$ ’ to $\mathrm{X}$ ; and it is only in the fourth, and final, part of this series that I will consider such inferences and an extension of the account to the logic of conditional obligation and permission.Footnote 1
Of especial importance to the whole project, as I conceive it, is that the language and logic of imperative (or deontic) statements should provide a guide to action. We might imagine that we wish to relay certain information to a robot in the form of indicative sentences and to relay certain instructions to the robot in the form of imperative sentences. The robot must then work out what to do on the basis of the information and the instructions. And our aim is to construct a canonical form of expression for relaying the information and the instructions to the robot and a canonical form of inference by which the robot might then work out what to do.
There are two constraints which have shaped our overall approach and which I have taken to form an important aspect of the account. The first is a requirement of uniformity. The standard truthmaker clauses for the connectives and the standard definition of validity should carry over to the conditional case. We therefore require something analogous to actions which might serve as the entities in compliance with or in contravention to conditional imperatives. It turns out that we can think of these entities as plans, which tell us what to do in each of a number of particular circumstances. Thus in the case of the imperative ‘take an umbrella if it rains’, the plan of taking an umbrella in the circumstance in which it rains will be in conformity with the imperative, while the plan of not taking an umbrella in the circumstance in which it rains will be in contravention to the imperative.
The second constraint is that the logic of imperatives should conform to a normal form theorem. We are familiar with the disjunctive normal form theorem from classical propositional logic, according to which any formula is equivalent to a disjunction of state-descriptions. Given that the content of a truth-functional formula is given by a truth-table, we naturally expect to be able to represent the truth-table by a disjunction of state-descriptions, where each of the state-descriptions corresponds to an entry of the truth-table in which the formula is true.
The content of an imperative sentence is similarly given by the plans in compliance with the imperative. It is therefore to be expected, at least within a suitably expressive language, that a formula of imperative logic will be equivalent to a disjunction of plan descriptions, where each of the plan descriptions corresponds to a plan that is in compliance with the formula.
This is not only to be expected, but it is also especially desirable if the logic of imperatives is to serve as a guide to action. For the instructions presented to an agent, or our robot, may be of arbitrary complexity. It may consist of the negations of conditional imperatives, for example, as when we wish to reject some imperatives that might already have been issued, or of conditional imperatives in which the consequent is itself a conditional imperative, as when we wish to make some pre-existing imperatives conditional upon some state of affairs. When presented with imperatives in these other forms, it will not in general be evident what they require us to do in this or that situation; and this difficulty may be removed by putting the imperatives in a normal form from which can be read the specific plans that they prescribe. By not requiring that formulas be written in normal form and yet having a normal form theorem, we are able to combine flexibility in the expression of an imperative (or some other form of expression) with the simplicity of its content.
It is important, in this regard, to bear in mind that the inferential demands that we wish to place upon a set of instructions are very different from those that we wish to place upon a body of information. For instructions are to be followed, and so our principal interest is in putting them in such a form that it is then clear how they are to be followed. But a body of information is to be believed, and our interest in the items of information is not in how they are to believed but in what follows from them once they are believed. The importance of a normal form theorem is therefore much greater in the one sphere than in the other.
Our insistence upon being able to put imperatives into normal form has a couple of significant consequences. One is that it seems almost to force upon us certain controversial theses in the logic of conditionals. For consider the conditional imperative ‘if it rains then if there is no wind then take an umbrella’ $(\mathrm{R}\to (\mathrm{N}\to \mathrm{T}))$ . Then to get it into the required form, it looks as if we should take it to be equivalent to ‘if it rains and there is no wind then take an umbrella’ ( $(\mathrm{R}\wedge \mathrm{N})\to \mathrm{T})$ )—the so-called Import–Export rule. Or consider the conditional imperative ‘if it rains or is cold then wear a coat’ ( $(\mathrm{R}\vee \mathrm{C})\to \mathrm{W}$ ). Then to get the required form in this case, it looks as if we should take it to be equivalent to ‘if it rains then wear a coat and if it is cold then wear a coat’ ( $(\mathrm{R}\to \mathrm{W})\wedge (\mathrm{C}\to \mathrm{W})$ )—the so-called rule of Simplification. These rules have usually been accepted on the basis of intuitive considerations. It is therefore of interest that there is a deeper rationale for them in terms of the role they might play in securing a reduction to normal form.
A further consequence is that the rules we require in order to put formulas into normal form more or less force us into adopting a hyper-intensional approach to the logic of imperatives. For one may well wish to endorse the imperative ‘if it rains then take an umbrella’ $(\mathrm{R}\to \mathrm{T})$ but not endorse the imperative ‘if it rains and there is a strong wind then take an umbrella’ ( $\mathrm{R}\wedge \mathrm{S}\to \mathrm{T}$ ). But R is classically equivalent to $\mathrm{R}\vee (\mathrm{R}\wedge \mathrm{S})$ and so, if $\mathrm{R}\vee (\mathrm{R}\wedge \mathrm{S})$ were freely substitutable for R, we could go from $(\mathrm{R}\to \mathrm{T})$ to $(\mathrm{R}\vee (\mathrm{R}\wedge \mathrm{S}))\to \mathrm{T}$ and then, by Simplification, to $(\mathrm{R}\to \mathrm{T})\wedge ((\mathrm{R}\wedge \mathrm{S})\to \mathrm{T})$ . Thus we cannot have Simplification without Antecedent Strengthening within an intensional approach, and so if we want the one but not the other, then we are obliged to adopt a hyper-intensional approach in which classically equivalent antecedents within a conditional cannot be freely substituted for one another.
The present paper is long and so the reader may find it helpful to have a guide to its various sections and sub-sections:
Sections 1 and 2 contain some preliminary material on conditional imperatives. Section 1 considers various interpretations of imperatives that will be relevant to the subsequent formal treatment, and Section 2 specifies the syntax for the language of conditional imperatives. This will call for the use of indicative and imperative formulas and for a certain correspondence between them.
Sections 3–6 outline the pre-conditional framework. Section 3 reviews some standard material on truthmaker semantics, including the concepts of a state space and a model, the evaluation of truth-functional formulas, and the definition of various logical concepts; Section 4 presents the multi-set version of truthmaker semantics for the indicatives which figure as the antecedents of conditional imperatives; Section 5 reviews some earlier results on the logic of exact equivalence and analytic entailment for truth-functional formulas and it presents a result on normal forms for formulas not containing the conditional imperative, which will later be extended to a result on normal forms for formulas that do contain the conditional imperative; and Section 6 extends the basic semantic framework to one which allows for a distinction between situations, which are meant to serve as truth-makers for indicatives, and actions, which are meant to serve as the compliance-makers for imperatives.
One distinctive feature of our approach is that we adopt a multi-set semantics for indicatives under which an indicative may be made true any number of times by a given state (Section 4). It turns out that this generalization of the more usual form of semantics is required in order to establish the extended version of the normal form theorem. Thus the insistence of normal forms has significant consequences for the general form of the semantics.
Sections 7–12 develop the abstract theory of plans by means of which the conditional imperatives of our language are to be interpreted. Section 7 provides an informal explanation of how plans relate to imperatives; Section 8 provides a formal treatment of plans and explains how they may be subject to various constraints and various closure operations; Section 9 deals with the relationship between partial plans (which need not be defined on all situations) and total plans (which must be defined on all situations) and shows how each action may be identified with a total plan; Section 10 explains how a plan may be conditionalized to a situation and establishes some of the basic properties of this notion, while Section 11 does the same for plans that are subject to various constraints or closure operations; Section 12 then extends the operation of conditionalization in two directions, so that we may conditionalize by a proposition, i.e., by a set of situations, rather than by a single situation, and so that we may conditionalize on a prescription, i.e., on a set of plans, rather than on a single plan. It is by means of this abstract notion of conditionalization, as it is defined on propositions and prescriptions, that we interpret the conditional; and it is by means of the formal properties of conditionalization that we establish the logical properties of the conditional.
Sections 13–15 establish the extended normal form theorem. Section 13 provides the positive reduction theses (not involving negation) upon which the positive reduction to normal form rests; Section 14 introduces the negative semantics for conditional imperatives and provides the negative reduction theses (involving negation) upon which the negative reduction to normal form rests; and Section 15 puts the positive and negative results together in establishing a general reduction to normal form and a completeness theorem.
There has been a spate of recent literature on the semantics and logic of imperatives,Footnote 2 but the present approach differs considerably from most of the recent literature both in its goals and in its conclusions. I should remind the reader, in the first place, that my aim throughout the different parts of this paper has been regimentation, not description. I wish to provide, not a faithful description of how imperatives are used in natural language, but a reasonably adequate and perspicuous representation of imperative reasoning. But the focus in the literature has often been on description rather than regimentation, and this means that a comparison on this score is not altogether appropriate.
In the second place, the present approach to imperatives has been developed within the framework of truthmaker semantics, with its ontology of states and ideology of exact truthmaking, whereas most of the more recent approaches have been developed within the possible worlds framework. This has meant that I have not felt obliged to accept the preservation of content under the substitution of classical equivalents, and it has also meant that I have been able to achieve a normal form theorem even though this would not be possible, as we have seen, under any of the intensional approaches. I consider this to be a major advantage of the approach.
There are some similarities, of course. In particular, some other authors have appealed to the idea of a plan in developing a semantics for imperatives or deontic modals. But their conception of a plan and its relationship to an imperative is very different from my own. For me, a plan is a function from states to actions, whereas Yalcin [Reference Yalcin18]—following Gibbard [Reference Gibbard13]—takes it to be a function from propositions (or sets of worlds) to propositions. Thus the critical distinction between situations and actions in my own account is ignored. Or again, a plan should be in exact compliance with an imperative for me, whereas Charlow [Reference Charlow2] in effect only requires it to be in inexact compliance. The structural role of plans in my account, as items in a state space ordered by a relation of part-whole, is also very different and plays an important part in the determination of the logic.
1 The interpretation of conditional imperatives
There are a number of different ways in which, at the purely informal level, a conditional imperative might be understood. Some of them make a difference to the formal semantics and to the logic, while others merely make a difference to how the formal semantics should itself be construed. It will be helpful to make clear where I stand on these various interpretations, and, although my focus is here on the case of imperatives, it should be noted that the same distinctions (and some others) will also apply in the deontic case.
1.1 Single/multi-agent
Our concern will be with imperatives directed at a single agent, whether it be an individual or group agent. We shall not be concerned with imperatives directed at different agents or with the interaction between them, even though this is clearly an important topic in its own right.
1.2 Specific/general
An imperative might concern a specific agent in a specific situation. Thus as someone is preparing to go out, I might say ‘take an umbrella if it is raining’ (or ‘you ought to take an umbrella if it is raining’), where my statement is directed at the particular situation in which the agent finds herself. On the other hand, an imperative might be more general in scope. Thus I might say ‘take an umbrella if it rains’ by way of a piece of standing advice that is meant to apply generally to a range of different agents or different situations.
The formal semantics I give below can be taken to have application in either case, though the understanding of the truth- and compliance-makers will be different, with token situations and actions as the truth- or compliance-makers in the first case and with situation and action types as the truth- or compliance-makers in the second case. In a more extended treatment in which predicates and quantifiers are allowed, it would be possible to deal simultaneously with both kinds of cases by introducing predicates for types of actions.
1.3 Subjective/objective
There is a familiar distinction between a subjective and an objective understanding of deontic conditionals, which also has application to imperative conditionals. Under the subjective interpretation, the antecedent of the conditional is meant to relate to conditions of which the agent has knowledge or some other form of cognitive awareness, whereas, under the objective interpretation, the antecedent relates to the conditions that actually obtain, regardless of whether the agent has any form of cognitive access to them.
There is a natural assumption under which the subjective and objective interpretations will coincide, and this is that the agent should always be aware of the circumstances that are relevant to what she is to do. The situation the agent is in should be the situation in which she ‘finds herself’. Indeed, if a conditional imperative is to be helpful as a guide to action, then the two had better be the same. Someone may tell me to thank the gods if the Continuum Hypothesis is true, but this will be of little use to me if I have no way of knowing whether the Continuum Hypothesis is in fact true.
1.4 Defeasible/indefeasible
This is by far the most important of the distinctions and it has enormous consequences for the resulting semantics and logic.
Consider the conditional imperative ‘if it rains take an umbrella’. If someone is willing to issue this imperative then should they also be willing to issue ‘if it rains and there is a strong wind then take an umbrella’? Under a defeasible interpretation of the conditional, we do not presuppose that the inference will go through while, under the indefeasible interpretation, we do. Thus the antecedent of a conditional imperative can always be conjunctively strengthened under the indefeasible interpretation but not necessarily under the defeasible interpretation.
There are a number of ways in which one might understand the defeasible conditional. But one natural line of thought is that in enjoining someone to take an umbrella if it rains one is enjoining them to take an umbrella if it rains and there are no countervailing circumstances (such as a strong wind). This is not necessarily to presuppose that there are no countervailing circumstances but merely to enjoin someone to do what is to be done under the assumption that such circumstances do not in fact exist.
It is plausible to suppose that to each defeasible conditional of the form ‘if $C$ then do φ’ there will correspond a range of indefeasible conditionals , ‘if ${C}_1$ then do φ’, ‘if ${C}_2$ then do φ’, …, where ${C}_1$ , ${C}_2$ exhaust the different ‘propitious’ circumstances in which $C$ obtains. It might then be wondered why we do not use the indefeasible conditionals, which have a relatively clear interpretation, in place of the defeasible conditional. Now there may indeed be cases, especially when only actual circumstances are under consideration, in which the propitious circumstances ${C}_1$ , ${C}_2$ , … can be circumscribed in advance. But this will not usually be possible, and hence the importance, in many practical contexts, of being able to use the defeasible form of expression.
The defeasible interpretation meshes very well with the subjective interpretation. The antecedent then relates to the information the agent has at a given time and the conditional is telling the agent what to do in the absence of countervailing information. As a special case, then, the conditional will tell the agent what to do when the information embodied in the antecedent is the total (or the total relevant) information available to the agent. The application of the conditional corresponds, in this case, to the principle of total evidence of Carnap [Reference Carnap1] (a point made by Sellars [Reference Sellars15, p. 325]). Just as the probability that you assign to a proposition should be based upon one’s total (or one’s total relevant) evidence, so the application of a conditional imperative should be based on one’s total (or one’s total relevant) information.
In what follows, the reader may find it helpful to regard the combination of the defeasible and subjective interpretations as a paradigm of how the symbolism is to be applied, although I would not wish to exclude other interpretations.
1.5 Inclusive imperatives
A less familiar issue concerns the prescription to do something in a situation in which what is to be done, or part of what is to be done, is itself part of the situation. How, for example, should we regard the imperative: go to the meeting if one goes?
One natural point of view is that such imperatives are not well-formed and that generally, in a well-formed conditional imperative, the action to be undertaken should be disjoint from the situation upon which it is conditional. Unfortunately, this point of view cannot very well be sustained quite apart from the logical difficulties in implementing it. For consider the imperative analogue of the puzzle of the ‘gentle murderer’ from Forrester [Reference Forrester12]. I might enjoin my criminal buddy to kill his rival gently if he kills her. But killing his rival gently entails killing her (and, indeed, has killing her as a part). It therefore appears that in enjoining my buddy to kill his rival gently if he kills her, I am enjoining him (in part) to kill her if he kills her.
One might try to evade this difficulty by reformulating the conditional imperative as one in which, in the situation in which my buddy kills his rival, he should do what in addition to the killing would make the killing gentle. But it is hard to say what this additional thing would be without it also entailing or having as a part the killing. No clean reformulation of the conditional imperative, in which the gentleness is detached from the killing, would appear to be possible, and what I would like to propose instead is that we allow the inference to go through and that we allow, in general, for the imperative ‘do $X$ if you do $X$ ’ to be a consequence of any imperatives whatever. I do not wish to claim that this is in conformity with our ordinary use of conditional imperatives (the matter is far from clear). But no harm will arise from our allowing such imperatives since, given that $X$ is done, there is nothing else that they require of the agent, and it considerably simplifies the formulation of imperatives once they are allowed. This may not provide us with a solution to Forrester’s puzzle, which may be taken to concern our ordinary understanding of conditional imperatives (or conditional obligation), but, under our present understanding of these conditionals, we achieve an admirable evasion of the puzzle.
2 Syntax
We describe the language for the logic of imperatives that we shall be adopting. The primitive vocabulary consists of the following symbols:
-
indicative atoms ${\mathrm{s}}_1$ , ${\mathrm{s}}_2,\dots$
-
imperative atoms ${\mathrm{p}}_1$ , ${\mathrm{p}}_2,\dots$
-
the verum constants $\top$ and $\top !,$
-
the connectives $\neg, \vee, \wedge$ , and $\to,$
-
the parentheses (and).
The indicative atoms ${\mathrm{s}}_1,{\mathrm{s}}_2,\dots$ are meant to signify situations, i.e., to have situations as their truth- and falsity-makers, while the imperative atoms ${\mathrm{p}}_1$ , ${\mathrm{p}}_2$ , … are meant to signify actions or plans, i.e., to have actions or plans as their compliance- and contravention-makers.
The language contains two verum constants: $\top$ for the indicative made true by the null situation and $\top !$ for the imperative with which the null action is in compliance. We use $\perp$ (the falsum constant) as an abbreviation for $\neg \top$ and $\perp !$ as an abbreviation for $\neg \top !$ .
Indicative and imperative formulas are defined by means of the following inductive clauses:
-
IN1. $\top$ and any indicative atom is an indicative formula.
-
IN2. If $\mathrm{S}$ is an indicative formula, then so is $\neg \mathrm{S}$ .
-
IN3. If $\mathrm{S}$ and $\mathrm{T}$ are indicative formulas, then so are $(\mathrm{S}\vee \mathrm{T})$ and $(\mathrm{S}\wedge \mathrm{T})$ .
-
IM1. $\top !$ and any imperative atom is an imperative formula.
-
IM2. If $\mathrm{P}$ is an imperative formula, then so is $\neg \mathrm{P}$ .
-
IM3. If $\mathrm{P}$ and $\mathrm{Q}$ are imperative formulas, then so are $(\mathrm{P}\vee \mathrm{Q})$ and $(\mathrm{P}\wedge \mathrm{Q})$ .
-
IM4. If $\mathrm{S}$ is an indicative formula and $\mathrm{P}$ an imperative formula, then $(\mathrm{S}\to \mathrm{P})$ is an imperative formula.
A formula is any indicative or imperative formula. We use $\mathrm{S},\mathrm{T},$ etc. for indicative formulas and $\mathrm{P},\mathrm{Q},$ etc. for imperative formulas, and we allow ourselves freely to put ‘!’ at the end of an imperative formula as a way of making clear that it is an imperative rather than an indicative formula.
Note that clause IM4 is the only source of ‘hybrids’, in which indicative and imperative formulas come together. It permits an indicative to appear to the left of a conditional, though not to the right, and it permits an imperative to appear to the right of a conditional, though not to the left.
We shall have occasion in part IV to distinguish an infinite subset ${\mathrm{a}}_1!$ , ${\mathrm{a}}_2!$ , … of the imperative atoms and a corresponding infinite subset of indicative atoms ${\mathrm{a}}_1$ , ${\mathrm{a}}_2$ , …. We call them A-atoms and suppose that ${\mathrm{a}}_1!$ , ${\mathrm{a}}_2!$ , … form a co-infinite subset of all the imperative atoms and that ${\mathrm{a}}_1$ , ${\mathrm{a}}_2$ , … form a co-infinite subset of all the indicative atoms. These co-infinite subsets behave in exactly the same way, syntactically speaking, as the regular imperative and indicative atoms, but the intention is that the imperative A-atoms should designate actions (rather than plans) and that the indicative A-atoms should designate corresponding states (to the effect that the given action is performed). It is through the coordination of imperative and indicative atoms that we are able to treat an action as itself part of a situation that may serve as the condition for other actions to be performed.
3 Background
I give a brief overview of standard truthmaker semantics for a propositional language (the reader might like to consult [Reference Fine, Hale, Wright and Miller7] for a general introduction to the topic).
A partial order (p.o.) on a set $S$ is a reflexive, transitive, and anti-symmetric relation on $S$ . Given the p.o. $\sqsubseteq$ on $S$ , we say:
-
$s$ is null if $s$ $\sqsubseteq$ $s^{\prime }$ for all $s^{\prime }$ $\in$ $S$ and otherwise is non-null;
-
$s$ is an upper bound of $T$ if $t$ $\sqsubseteq$ $s$ for each $t$ $\in$ $T$ ;
-
$s$ is a lower bound of $T$ if $s$ $\sqsubseteq t$ for each $t$ $\in$ $T$ ;
-
$s$ is a least upper bound (lub) of $T$ if $s$ is an upper bound of $T$ and $s\sqsubseteq s^{\prime }$ for any upper bound $s^{\prime }$ of $T$ ;
-
$s$ is a greatest lower bound (glb) of $T$ if s is a lower bound of $T$ and $s\sqsubseteq s^{\prime }$ for any lower bound $s^{\prime }$ of $T$ ;
-
$s\sqsubset t$ ( $s$ is a proper part of $t$ ) if $s\sqsubseteq t$ but not $t\sqsubseteq s$ ;
-
$s$ overlaps $t$ if for some non-null $u$ , $u\sqsubseteq s$ and $u\sqsubseteq t$ ;
-
$s$ is disjoint from $t$ if $s$ does not overlap $t$ .
The least upper bound of $T\subseteq S$ if it exists is unique. We denote it by $\bigsqcup T$ and call it the fusion of $T$ (or of the members of $T$ ). When $T=\{{t}_1,{t}_2,\dots \}$ , we shall sometimes write $\bigsqcup T$ more perspicuously as ${t}_1\sqcup {t}_2\sqcup \cdots$ . Likewise, for the greatest lower bound $\sqcap T$ .
A state space $\boldsymbol{S}$ is a pair $(S,\sqsubseteq )$ , where $S$ (states) is a non-empty set and $\sqsubseteq$ (part) is a partial order on $S$ which is complete, i.e., any subset $T$ of $S$ has a least upper bound $\bigsqcup T$ . We use $\square$ (the null state) for the least state $\bigsqcup \varnothing$ of $\boldsymbol{S}$ and $\blacksquare$ (the full state) for the greatest state $\bigsqcup S$ of $\boldsymbol{S}$ . In a state space, any subset $T$ of $S$ will also have a greatest lower bound $\sqcap T$ . For now we are thinking of states in a generic way, which will be compatible with thinking of them as either situations or actions or plans.
A state space $\boldsymbol{S}^{\prime}=(S^{\prime },\sqsubseteq^{\prime})$ is said to be a subspace of the state space $\boldsymbol{S}=(S,\sqsubseteq )$ if $S^{\prime }$ is a subset of $S$ and $\sqsubseteq^{\prime }$ is the restriction $\sqsubseteq \upharpoonleft S^{\prime }$ of $\sqsubseteq$ to $S^{\prime }$ . If $\boldsymbol{S}=(S,\sqsubseteq )$ and $\boldsymbol{T}=(T,\sqsubseteq^{\prime})$ are two state-spaces, then their product $\boldsymbol{S}\times \boldsymbol{T}$ is the structure $(S\times T,{\sqsubseteq}_{\times})$ , where
It is readily verified that $\boldsymbol{S}\times \boldsymbol{T}$ is also a state space.
Let us now suppose that the formulas of our language are constructed from certain atoms ${\mathrm{x}}_1$ , ${\mathrm{x}}_2$ , … and the verum and falsum constants $\top$ and $\perp$ by means of the usual connectives, $\vee, \wedge,$ and $\neg$ (for now we do not allow the conditional). Proceeding in this way allows us to remain neutral as to the exact identity of the atoms. However, we shall, in this and the next section, use $\mathrm{X},\mathrm{Y},\mathrm{Z}$ … for formulas of the present neutral language rather than for the imperative formulas of the previous papers.
A state model $\boldsymbol{M}$ over the state space $\boldsymbol{S}=(S,\sqsubseteq )$ is a triple $(S,\sqsubseteq, | \cdot |)$ , where $| \cdot |$ (the valuation) is a function taking each atom $\mathrm{x}$ into a pair of non-empty subsets ${|\mathrm{x}|}^{+}$ and ${|\mathrm{x}|}^{-}$ of $S$ (the respective truth- and falsity-makers of $\mathrm{x}$ ). Such a valuation is said to be a bilateral valuation over $S$ on the given atoms. It is to be contrasted with a unilateral valuation which simply assigns a subset of states to each atom. We also allow a model, both here and elsewhere, to be defined over a subset of the relevant atoms.
The atom $\mathrm{x}$ is said to be definite in a model if ${|\mathrm{x}|}^{+}$ is singleton, to be bi-definite if both ${|\mathrm{x}|}^{+}$ and ${|\mathrm{x}|}^{-}$ are singleton, and to be non-vacuous if neither ${|\mathrm{x}|}^{+}$ nor ${|\mathrm{x}|}^{-}$ is empty. The model $\boldsymbol{M}$ itself is said to be definite (bi-definite, non-vacuous) if each atom is definite (bi-definite, non-vacuous) in the model.
Given any model $\boldsymbol{M}=(S,\sqsubseteq, | \cdot |)$ , there is a standard way of extending the valuation $| \cdot |$ to all other formulas. For subsets $T$ and $U$ of $S$ , let $T\sqcup U=\{t\sqcup u:t\in T\; and\;u\in U\}$ . We then define $| \cdot |$ on all formulas by means of the following clauses:
-
${|\top |}^{+}=\{\square \}$ .
-
${|\top |}^{-}\kern0.48em =\varnothing$ .
-
${|\neg \mathrm{X}|}^{+}={|\mathrm{X}|}^{-}.$
-
${|\neg \mathrm{X}|}^{-}={|\mathrm{X}|}^{+}$ .
-
${|\mathrm{X}\wedge \mathrm{Y}|}^{+}={|\mathrm{X}|}^{+}\sqcup {|\mathrm{Y}|}^{+}.$
-
${|\mathrm{X}\wedge \mathrm{Y}|}^{-}={|\mathrm{X}|}^{-}\cup {|\mathrm{Y}|}^{-}.$
-
${|\mathrm{X}\vee \mathrm{Y}|}^{+}={|\mathrm{X}|}^{+}\cup {|\mathrm{Y}|}^{+}$ .
-
${|\mathrm{X}\vee \mathrm{Y}|}^{-}={|\mathrm{X}|}^{-}\sqcup {|\mathrm{Y}|}^{-}$ .
The negative clause for the verum constant is somewhat different from that in [Reference Fine9]. We there took ${|\top |}^{-}$ to be $|\blacksquare|$ rather than $\varnothing$ . Each clause has its advantages and disadvantages, but, in the case of conditionals, it will be convenient to adopt the present clause. Note that we have required ${|\mathrm{x}|}^{+}$ and ${|\mathrm{x}|}^{-}$ , for any atom $\mathrm{x}$ , to be non-empty, whereas ${|\top |}^{-}$ is empty. This means that we cannot think of an atom as standing in for $\top$ .
The above clauses can be stated in more orthodox fashion by specifying when a state $s$ is a truth-maker ( $s\ ||\!\text{-}\ \mathrm{X}$ ) or a falsity-maker $s$ $\text{-}\!||\ \mathrm{X}$ for $\mathrm{X}$ . Thus the clauses for $\mathrm{X}\wedge \mathrm{Y}$ and $\neg \mathrm{X}$ now take the following form:
-
$s\ ||\!\text{-}\ \mathrm{X}\wedge \mathrm{Y}$ iff for some $t$ and $u$ , $t\ ||\!\text{-}\ \mathrm{X}$ , $u\ ||\!\text{-}\ \mathrm{Y}$ and $s=t\sqcup u$ .
-
$s\ \text{-}\!||\ \mathrm{X}\wedge \mathrm{Y}$ iff $s\ \text{-}\!||\ \mathrm{X}$ or $s\ \text{-}\!||\ \mathrm{Y}$ .
-
$s\ ||\!\text{-}\ \neg \mathrm{X}$ iff $s\ \text{-}\!||\ \mathrm{X}$ .
-
$s\ \text{-}\!||\ \neg \mathrm{X}$ iff $s\ ||\!\text{-}\ \mathrm{X}$ .
The two kinds of clauses will then be in conformity with one another, in that $| \mathrm{X}|^+=\{s{:}\ s\ ||\!\text{-}\ \mathrm{X}\}$ and $| \mathrm{X}|^- =\{s{:}\ s\ \text{-}\!||\ \mathrm{X}\}$ .
We may define various logical notions. Let $\Delta$ be a well-ordered sequence ${\mathrm{X}}_1,{\mathrm{X}}_2,\dots$ of formulas. Given a model $\boldsymbol{M}$ , we say that:
-
$\Delta$ exactly entails the formula $\mathrm{Y}$ in $\boldsymbol{M}$ if ${s}_1\sqcup {s}_2\sqcup \dots \ ||\!\text{-}\ \mathrm{Y}$ in $\boldsymbol{M}$ whenever ${s}_1\ ||\!\text{-}\ {\mathrm{X}}_1,{s}_2\ ||\!\text{-}\ {\mathrm{X}}_2,\dots$ in $\boldsymbol{M}$ , and that:
-
$\Delta$ contains $\mathrm{Y}$ in $\boldsymbol{M}$ —symbolically, $\Delta\;{>}_{\boldsymbol{M}}\mathrm{Y}$ —if (i) whenever ${s}_1\ ||\!\text{-}\ {\mathrm{X}}_1,{s}_2\ ||\!\text{-}\ {\mathrm{X}}_2,\dots$ in $\boldsymbol{M}$ then for some $t\sqsubseteq {s}_1\sqcup {s}_2\sqcup \dots, t\ ||\!\text{-}\ \mathrm{Y}$ in $\boldsymbol{M}$ , and (ii) whenever $t\ ||\!\text{-}\ \mathrm{Y}$ in $\boldsymbol{M}$ then for some ${s}_1,{s}_2,\dots$ , ${s}_1\ ||\!\text{-}\ {\mathrm{X}}_1,{s}_2\ ||\!\text{-}\ {\mathrm{X}}_2,\dots$ in $\boldsymbol{M}$ and $t\sqsubseteq {s}_1\sqcup {s}_2\sqcup \dots$ .
Given formulas $\mathrm{X}$ and $\mathrm{Y}$ , we also say that:
-
$\mathrm{X}$ and $\mathrm{Y}$ are (positive) (exact) equivalents in $\boldsymbol{M}$ —in symbols, $\mathrm{X}\;{\approx}_{\boldsymbol{M}}\mathrm{Y}$ or $\mathrm{X}\;{\approx}^{+}_{\mathrm{M}}\mathrm{Y}$ —if, for any state s, s $\Vdash$ X in $\boldsymbol{M}$ iff s ╟ Y in $\boldsymbol{M}$ ;
-
$\mathrm{X}$ and $\mathrm{Y}$ are negative (exact) equivalents in $\boldsymbol{M}$ —in symbols, $\mathrm{X}\approx ^{-}_{\mathrm{M}}\;\mathrm{Y}$ —if, for any state $s$ , $s\ \text{-}\!||\ \mathrm{X}$ in $\boldsymbol{M}$ iff $s\ \text{-}\!||\ \mathrm{Y}$ in $\boldsymbol{M}$ ; and
-
$\mathrm{X}$ and $\mathrm{Y}$ are full (exact) equivalents in $\boldsymbol{M}$ —in symbols, $\mathrm{X}\approx ^{\pm}_{\mathrm{M}}\;\mathrm{Y}$ —if they are both positive and negative exact equivalents.
We can also define non-relative analogues of these notions in the obvious way. For example, $\mathrm{X}$ and $\mathrm{Y}$ will be (positive) exact equivalents— $\mathrm{X}\approx \mathrm{Y}$ —if $\mathrm{X}\approx ^{\pm}_{\mathrm{M}}\kern0.24em \mathrm{Y}$ for any model $\boldsymbol{M}$ . We may also sometimes restrict these non-relative analogues to a sub-class of models. (Note that this notation slightly departs from the notation of Fine [Reference Fine8], where $\mathrm{X}\approx \mathrm{Y}$ is used as an abbreviation in the object language.)
Although we shall not give a precise statement or proof, we should mention that full equivalents may be substituted for one another in any formula, preserving full equivalence, while positive equivalents may be substituted within positive contexts (in the usual sense of the term), thereby preserving positive equivalence.
4 Multi-set semantics
For reasons that will later become clear, we shall find it helpful to formulate a slightly more fine-grained form of the semantics. Suppose $s$ is the sole truth-maker for the atom $\mathrm{x}$ . Then we will want to say not merely that $s$ is a truth-maker for $\mathrm{x}\vee \mathrm{x}$ , but that it is a truth-maker twice, once via the left disjunct and once via the right disjunct. To this end, we should take the content of a formula to be a multi-set $[s,s]$ in which the truth-maker $s$ occurs twice.
I shall forgo a precise treatment of multi-sets, but the reader may find it helpful to think of them in graphical terms. [1, 2, 2, 3, 3, 3], for example, is the multi-set in which $1$ occurs once, $2$ twice, and $3$ thrice, $[1,2,3]$ is the multi-set in which $1,2$ , and $3$ occur only once, while $[]$ is the empty multi-set. Given two multi-sets $X=[{x}_1,{x}_2,\dots ]$ and $Y=[{y}_1,{y}_2,\dots ]$ , their union is the multi-set $[{x}_1,{x}_2,\dots, {y}_1,{y}_2,\dots ]$ and their fusion is the multi-set $[{x}_1\sqcup {y}_1,{x}_1\sqcup {y}_2,\dots, {x}_2\sqcup {y}_1,{x}_2\sqcup {y}_2,\dots, \dots ]$ . So, for example, is $[0,1,1,2,2,2,2,3,3,3]$ .
We shall need to make use of multi-maps. Suppose $X=[{x}_1,{x}_2,\dots ]$ is a multi-set and $Y=\{{y}_1,{y}_2,\dots \}$ is a set. Then a multi-map $f$ from $X$ into $Y$ is a multi-set of ordered pairs $[{<}{x}_1,{y}_1{>},{<}{x}_2,{y}_2{>},\dots ]$ . Thus identical members of $X$ may be associated with distinct members of $Y$ .
A multi-set model $\boldsymbol{M}=(S,\sqsubseteq, | \cdot |)$ over a state space $\boldsymbol{S}=(S,\sqsubseteq )$ is the same as before, except now the valuation $| \cdot |$ takes each atom $\mathrm{x}$ into a pair of non-empty multi-sets of states (we might call this a multi-set valuation). The valuation $| \cdot |$ can then be extended to all formulas by means of the following clauses:
-
${|\top |}^{+}=[\square ]$ .
-
${|\top |}^{-}\kern0.6em =\varnothing (=[\;])$ .
-
${|\neg \mathrm{X}|}^{+}={|\mathrm{X}|}^{-}$ .
-
${|\neg \mathrm{X}|}^{-}={|\mathrm{X}|}^{+}$ .
-
.
-
.
-
|.
-
.
Thus, the clauses are essentially the same as before, but the set-theoretic operations have been converted into corresponding operations on multi-sets. We may write ${|\mathrm{X}|}_M^{\pi }$ , for $\pi =+$ or $-$ , to make explicit the relativization of $| \mathrm{X}|$ to the model $\boldsymbol{M}$ .
Suppose $X=[{x}_1,{x}_2,\dots, {y}_1,{y}_2,\dots, {z}_1,{z}_2,\dots, \dots ]$ is a multi-set, specified in such a way that ${x}_1,{x}_2,\dots$ are the same element $x$ , ${y}_1,{y}_2,\dots$ are the same element $y$ , …., ${z}_1,{z}_2,\dots$ are the same element $z$ , …, and $x,y,z,\dots$ are pairwise distinct. We then let $\{X\}$ be the corresponding set {x, y, z, …}. Thus $\{X\}$ is like $X$ but for the fact that each element of $X$ , which may occur many times in $X$ , only occurs once in $\{X\}$ .
Given a multi-set model $\boldsymbol{M}=(S,\sqsubseteq, | \cdot |_{\boldsymbol{M}})$ , let $\{\boldsymbol{M}\}$ be the corresponding (set) model $(S,\sqsubseteq, | \cdot |_{\{\boldsymbol{M}\}})$ , where ${|\mathrm{x}|}_{\{M\}}^{\pi}=\{{|\mathrm{x}|}_M^{\pi}\}$ for each atom $\mathrm{x}$ and where $\pi =+$ or $-$ . Then $\{\boldsymbol{M}\}$ and $\boldsymbol{M}$ evaluate formulas in the same way but for a difference in the ‘count’:
Lemma. For any multi-set model $\boldsymbol{M}$ and formula $\mathrm{X}$ , ${|\mathrm{X}|}_{\{M\}}^{\pi}=\{{|\mathrm{X}|}_M^{\pi}\}$ for $\pi =+$ or $-$ .
Proof. A straightforward induction.
We might compare the present positive clause for disjunction with the conception of intuitionistic disjunction as disjoint union, where the disjoint union $X{\cdot}\! \cup\! {\cdot} Y$ of the sets $X$ and $Y$ might be defined as $\{(x,0):x\in X\}\cup \{(y,1):y\in Y\}$ . In the intuitionistic case, we distinguish between verification on the left and right (so that $X{\cdot}\! \cup \!{\cdot} Y$ will not, in general, be the same as $Y{\cdot}\! \cup \!{\cdot} X$ ), whereas, in the present case, we make no such distinction.
The similarity in the clauses for the two kinds of models belies a fundamental difference. For whereas in the earlier case, we can restate the clauses relationally, in terms of when a state is a truth-maker or falsity-maker for a given formula, this is no longer possible in the present case, since it does not provide us with the means of stating that a formula, such as α ∨ α, will be made true more than once by any given truth-maker for $\alpha$ .
Although this is not a topic I shall pursue here, it is worth noting that the previous order of explanation can be reversed and that, instead of explaining our symbolism in terms of multi-sets, we can use our symbolism to provide a convenient way of specifying multi-sets. Suppose, for example, that we wish to specify the multi-set $[1,1]$ . The usual set-theoretic formulation $[x{:}\ x=1]$ is not then appropriate. However, if we subject the defining conditions to a multi-set semantics, then $[1,1]$ can be specified as $[x{:}\ x=1\vee x=1]$ , which will be different from $[x{:}\ x=1]=[1]$ and, similarly, if f is a function, then we might specify its multi-range as $[y{:}\ \mathrm{for}\kern0.17em \mathrm{some}\;x,f(x)=y]$ , where y now will occur as many times in the multi-set as there are arguments $x$ for which $f(x)=y$ .
Indeed, for these purposes we can adopt a purely extensional quasi-classical version of the multi-set semantics in which there is just one element $\square (=\blacksquare )$ in the state space, corresponding to the actual world. The pair of multi-sets ( $[\square, \square, \dots ],[\square, \square, \dots ]$ ) assigned to a formula will then indicate how many times the formula is true and how many times it is false. So, for example, the condition x = 1 ∨ x = 1, when $1$ is assigned to $x$ , will have ([□, □], []) as its bilateral content, thereby indicating that $1$ is to occur twice in the corresponding multi-set $[x:x=1\vee x=1]$ .
The semantics of each formula in this simple model is given, in effect, by a pair of non-negative integers, where the first indicates how many times the formula is true and the second how many times it is false. Supposing $| \mathrm{X}| =(m,n)$ and $| \mathrm{Y}| =(p,q)$ , we will then have the following clauses for the truth-functional connectives:
-
$| \neg \mathrm{X}| =(n,m)$ .
-
$[(\mathrm{X}\vee \mathrm{Y})]=(m+p,n\times q)$ .
-
$| (\mathrm{X}\wedge \mathrm{Y})| =(m\times p,n+q)$ .
The notions of exact entailment and equivalence can be extended to the multi-set semantics in the obvious way. Thus the formula $\mathrm{X}$ will exactly entail the formula $\mathrm{Y}$ if whenever ${|\mathrm{X}|}^{+}=[{s}_1,{s}_2,\dots ]$ in a model $\boldsymbol{M}$ then ${|\mathrm{Y}|}^{+}$ is of the form $[{s}_1,{s}_2,\dots, \dots ]$ in $\boldsymbol{M}$ and $\mathrm{X}$ will be an exact equivalent of $\mathrm{Y}$ if the multi-sets ${|\mathrm{X}|}^{+}$ and | ${|\mathrm{Y}|}^{+}$ are the same. A related definition of containment could also be given, although it will not be required.
5 Logics
We briefly review some earlier findings concerning the logic of equivalence and containment. Given two formulas $\mathrm{X}$ and $\mathrm{Y}$ , we use $\mathrm{X}\equiv \mathrm{Y}$ to indicate that they are exact equivalents and use $\mathrm{X}>\mathrm{Y}$ to indicate that $\mathrm{X}$ contains $\mathrm{Y}$ .
We shall be interested in the following axioms and rules for $\equiv$ :
-
E1 $\mathrm{X}\equiv \neg \neg \mathrm{X}$ .
-
E2 $\mathrm{X}\wedge \mathrm{Y}\equiv \mathrm{Y}\wedge \mathrm{X}$ .
-
E3 $(\mathrm{X}\wedge \mathrm{Y})\wedge \mathrm{Z}\equiv \mathrm{X}\wedge (\mathrm{Y}\wedge \mathrm{Z})$ .
-
E4 $\mathrm{X}\vee \mathrm{Y}\equiv \mathrm{Y}\vee \mathrm{X}$ .
-
E5 $(\mathrm{X}\vee \mathrm{Y})\vee \mathrm{Z}\equiv \mathrm{X}\vee (\mathrm{Y}\vee \mathrm{Z})$ .
-
E6 $\neg (\mathrm{X}\wedge \mathrm{Y})\equiv (\neg \mathrm{X}\vee \neg \mathrm{Y})$ .
-
E7 $\neg (\mathrm{X}\vee \mathrm{Y})\equiv (\neg \mathrm{X}\wedge \neg \mathrm{Y})$ .
-
E8 $\mathrm{X}\wedge (\mathrm{Y}\vee \mathrm{Z})\equiv (\mathrm{X}\wedge \mathrm{Y})\vee (\mathrm{X}\wedge \mathrm{Z})$ .
-
E9 $\mathrm{X}\equiv \mathrm{Y}/\mathrm{Y}\equiv \mathrm{X}$ .
-
E10 $\mathrm{X}\equiv \mathrm{Y},\mathrm{Y}\equiv \mathrm{Z}/\mathrm{X}\equiv \mathrm{Z}$ .
-
E11 $\mathrm{X}\equiv \mathrm{Y}/\mathrm{X}\wedge \mathrm{Z}\equiv \mathrm{Y}\wedge \mathrm{Z}$ .
-
E12 $\mathrm{X}\equiv \mathrm{Y}/\mathrm{X}\vee \mathrm{Z}\equiv \mathrm{Y}\vee \mathrm{Z}$ .
-
E13 $\mathrm{X}\wedge \top \equiv \mathrm{X}$ .
-
E14 $\mathrm{X}\wedge \perp \equiv \perp$ .
-
E15 $\mathrm{X}\vee \perp \equiv \mathrm{X}$ .
-
E16 $\mathrm{X}\equiv \mathrm{X}\vee \mathrm{X}$ .
-
E17 $\mathrm{x}\wedge \mathrm{x}\equiv \mathrm{x}$ $\mathrm{x}$ an atom.
-
E18 $\neg \mathrm{x}\wedge \neg \mathrm{x}\equiv \neg \mathrm{x}$ $\mathrm{x}$ an atom.
The core system CS is comprised of the axioms and rules E1–E15. A sequent of the form $\mathrm{X}\equiv \mathrm{Y}$ is said to hold in a model $\boldsymbol{M}$ if $\mathrm{X}$ and $\mathrm{Y}$ are exact equivalents in $\boldsymbol{M}$ . A single sequent such as E1 is said to be valid if it is true in all models (or in all models from a pre-designated subclass of models) and a rule such as E9 is said to be valid if its conclusion holds in any model in which its premises hold. It may then be shown that CS is sound and complete for the multi-set semantics, i.e., that the provable sequents coincide with the valid sequents. CS is also sound and complete for the class of multi-set models $\boldsymbol{M}=(S,\sqsubseteq, | \cdot |)$ in which the state space $S$ is singleton.Footnote 3 This is somewhat surprising, and no similar result holds for the set-theoretic semantics. Axiom E16 corresponds to the adoption of a set-theoretic semantics, E17 to the restriction of the semantics to definite models, and E17 and E18 to the restriction of the semantics to bi-definite models. So, for example, the system CS + E16 will be sound and complete for the class of all set-theoretic models, the system CS + E17 sound and complete for the class of all definite multi-set models, and the system CS + E17 + E18 sound and complete for the class of all bi-definite multi-set models.
Let me now state the normal form theorem, which will play an important role in establishing the extended normal form theorem below. For this purpose, it will be helpful to refer to conjunctions of formulas ${\mathrm{X}}_1$ , ${\mathrm{X}}_2$ , …, ${\mathrm{X}}_n$ , where $n$ is allowed to be $0$ or $1$ . When $n=0$ , the conjunction is the verum constant $\top$ , and when $n=1$ , it is the single formula ${X}_1$ . We shall refer similarly to disjunctions of formulas ${\mathrm{X}}_1$ , ${\mathrm{X}}_2$ , …, ${\mathrm{X}}_n$ , where $n$ is again allowed to be 0 or 1. When $n=0$ , the disjunction is the falsum constant $\perp$ , and when $n=1$ , it is the single formula ${\mathrm{X}}_1$ .
A literal $\pm \mathrm{x}$ is an atom $\mathrm{x}$ or its negation $\neg \mathrm{x}$ , a state description is a conjunction (possibly empty) of literals, and a disjunctive normal form is a disjunction (possibly empty) of state descriptions. Say that the formulas $\mathrm{X}$ and $\mathrm{Y}$ are provably equivalent in a given system if $\mathrm{X}\equiv \mathrm{Y}$ is a theorem of the system. Then we can establish along the lines of Fine [Reference Fine5]:
Theorem 1 (Disjunctive Normal Form)
Every formula is provably equivalent in CS to a disjunctive normal form.
Let us note a couple of refinements of this result. We may suppose that the atoms of our language occur in a fixed order ${\mathrm{x}}_1$ , ${\mathrm{x}}_2\dots$ . Let ${\mathrm{x}}_1,\neg {\mathrm{x}}_1,{\mathrm{x}}_2,\neg {\mathrm{x}}_2,\dots$ be a corresponding order for the literals. Then a state description is said to be standard if its literals occur in the fixed order with association from left to right and it is said to be non-repetitive if no literal occurs more than once. Clearly, a standard state description is uniquely determined by the multi-set of its literal conjuncts and a standard non-repetitive state description is uniquely determined by the set of its literal conjuncts. The standard state descriptions might also be given in a fixed order. A disjunctive normal form is then said to be in standard form if it is a disjunction of standard state descriptions that occur in the fixed order with association from left to right. It is said to be conjunctively non-repetitive if each of its state descriptions is non-repetitive, to be disjunctively non-repetitive if none of its state descriptions occurs more than once, and to be fully non-repetitive if it is both conjunctively and disjunctively non-repetitive. Clearly, a standard form is uniquely determined by the multi-set of all those multi-sets of literals that correspond to an occurrence of one of its state descriptions, a fully non-repetitive standard form by the set of all those sets of literals that correspond to one of its state descriptions, and similarly for the other cases.
Corollary 2 (Standard Form)
Every formula $\mathrm{X}$ is provably equivalent in CS to a standard form $\mathrm{Y}$ . Moreover, $\mathrm{Y}$ can be taken to be disjunctively non-repetitive given axiom E16 and conjunctively non-repetitive given axioms E17 and E18.
We turn to the second refinement of the result. Take a realization scheme $\Sigma$ for a set of atoms $\Delta$ to be a set of formulas of the form $\neg \mathrm{x}\equiv ({\mathrm{y}}_1\vee {\mathrm{y}}_2\vee \cdots \vee {\mathrm{y}}_n)$ , one for each atom $\mathrm{x}$ of $\Delta$ , where ${\mathrm{y}}_1,{\mathrm{y}}_2,\dots, {\mathrm{y}}_n$ for $n>0$ , are distinct atoms (though not necessarily in $\Delta$ ) and say that $\Sigma$ is a realization scheme for a formula $\mathrm{X}$ if it is a realization scheme for the set of atoms that occur in $\mathrm{X}$ . Intuitively, a realization scheme provides a positive characterization of when the given atoms are false.
Say that a state description is positive if it is a conjunction of atoms and that a disjunctive normal form is positive if it is a disjunction of positive state descriptions. From Theorem 1, we easily derive:
Corollary 3 (Positive Disjunctive Normal Form)
Let $\mathrm{X}$ be a formula and $\Sigma$ a realization scheme for $\mathrm{X}$ . Then $\mathrm{X}$ is provably equivalent in CS + $\Sigma$ to a positive disjunctive normal form.
Combining the previous results, we obtain:
Corollary 4 (Positive Standard Form)
Let $\mathrm{X}$ be a formula and $\Sigma$ a realization scheme for $\mathrm{X}$ . Then $\mathrm{X}$ is provably equivalent in CS + $\Sigma$ to a positive standard form $\mathrm{Y}$ . Moreover, $\mathrm{Y}$ can be taken to be disjunctively non-repetitive given axiom E16 and conjunctively non-repetitive given axioms E17 + E18.
I have stated these results using the notion of provable equivalence. But we should note that by Soundness corresponding results will hold for the notion of semantic equivalence. Thus in the case of Theorem 1, we will have that every formula is exactly equivalent to a disjunction of state descriptions and, in the case of Corollary 3, we will have that, given a realization scheme $\Sigma$ , every formula $\mathrm{X}$ will be $\Sigma$ -equivalent to a positive disjunctive normal form $\mathrm{Y}$ , i.e., that $| \mathrm{X}|$ and $| \mathrm{Y}|$ will be the same in any model in which the equivalences of $\Sigma$ hold. I should also remark that in the subsequent treatment we could dispense with realization schemes by taking the models to be bi-definite (and adopting axioms E17 and E18). However, the present treatment is more general in that it allows an atom to have any positive finite number of falsity-makers.
Related rules can be given for the logic of containment within the set-theoretic semantics [Reference Fine8, Section 6]. An alternative approach, which we adopt here, builds the logic of containment on top of the logic of equivalence. Using ‘ $\mathrm{X}>\mathrm{Y}$ ’ as a symbolic notation for the containment relation, this requires that the following rules be added to the previous rules E1–E16:
-
$\mathrm{C}1.\ \mathrm{X}>\mathrm{Y},\mathrm{X}\equiv \mathrm{X}^{\prime },\mathrm{Y}\equiv \mathrm{Y}^{\prime }/\mathrm{X}^{\prime }>\mathrm{Y}^{\prime }$ ;
-
$\mathrm{C}2.\ \mathrm{X}\wedge \mathrm{Y}>\mathrm{X}$ as long as $\mathrm{Y}$ does not contain a negative occurrence of $\top$ ;
-
$\mathrm{C}3.\ \mathrm{X}>\mathrm{X}^{\prime },\mathrm{Y}>\mathrm{Y}^{\prime }/\mathrm{X}\vee \mathrm{Y}>\mathrm{X}^{\prime}\vee \mathrm{Y}^{\prime }$ .
Note the restriction on C2. This is required since $\mathrm{X}\ \wedge \perp\ >\mathrm{X}$ , for example, is not valid (for discussion, see the sub-section on partial content in [Reference Fine6]).
Using normal forms, we can also establish completeness for the various underlying systems along the lines of Fine [Reference Fine5]. Thus in the case of the system CS, we have:
Theorem 5 (Soundness and Completeness of CS)
The formula $\mathrm{X}\equiv \mathrm{Y}$ is derivable in CS iff $\mathrm{X}$ is exactly equivalent to $\mathrm{Y}$ .
Or again, in the case of the system for the logic of equivalence and containment described above, we can first use the original rules E1–E16 to put the formulas $\mathrm{X}$ and $\mathrm{Y}$ into appropriate disjunctive normal form and then use the additional rules C1–C3 to establish $\mathrm{X}>\mathrm{Y}$ when $\mathrm{X}$ semantically contains $\mathrm{Y}$ .
6 Situations and actions
The semantics for conditional imperatives will involve both situations and actions. Roughly, the idea is that a situation is a situation in which one acts—as when one takes an umbrella in the situation in which it rains. Actions may themselves be, or may constitute, situations—as when one puts on a rain coat in a situation in which one has taken an umbrella. We accordingly take a situation–action space (or S/A space) ${\boldsymbol{S}\kern-1.2pt}_\mathrm{I,A}$ to be a structure $({S}_{\mathrm{I}},{S}_{\mathrm{A}},\sqsubseteq )$ , where ${\boldsymbol{S}\kern-1.2pt}_{\mathrm{I}}=({S}_{\mathrm{I}},\sqsubseteq )$ is a state space and ${S}_{\mathrm{A}}$ is a subset of ${S}_{\mathrm{I}}$ closed under fusion $(\bigsqcup B\in {S}_{\mathrm{A}}\;\mathrm{whenever}\;B\subseteq {S}_{\mathrm{A}})$ . Intuitively, ${S}_{\mathrm{I}}$ consists of states or situations and ${S}_{\mathrm{A}}$ of actions. We have here presupposed that each action is identical to a situation, but this constitutes no great metaphysical commitment on our part. We could just as well have taken each action to constitute the situation in which that action is performed.
We set ${\boldsymbol{S}\kern-1.2pt}_{\mathrm{A}}=({S}_{\mathrm{A}},\sqsubseteq \upharpoonleft {S}_{\mathrm{A}})$ and call it an action (or A-) space. It should be evident that ${\boldsymbol{S}\kern-1.2pt}_{\mathrm{A}}$ is a subspace of ${\boldsymbol{S}\kern-1.2pt}_{\mathrm{I}}$ , and often we shall use $\sqsubseteq$ in place of $\sqsubseteq \upharpoonleft {S}_{\mathrm{A}}$ when it is clear that the relata are actions. The null action ${\square}_{\mathrm{A}}$ from ${\boldsymbol{S}\kern-1.2pt}_{\mathrm{A}}$ is identical to the null situation ${\square}_{\mathrm{I}}$ from ${\boldsymbol{S}\kern-1.2pt}_{\mathrm{I}}$ (to do nothing and for nothing to be is one and the same)—for which reason, we designate both as $\square$ . But although $\square_{\mathrm{A}}$ and $\square_{\mathrm{I}}$ are the same, the full action ${\blacksquare}_{\mathrm{A}}$ (the fusion of all actions) will not, in general, be the same as the full situation ${\blacksquare}_{\mathrm{I}}$ (the fusion of all situations) but merely a proper part of ${\blacksquare}_{\mathrm{I}}$ .
Given any situation $s\in S,$ there will be a greatest action ${a}_s$ that is a part of $s$ , viz. $\bigsqcup \{a\in {S}_{\mathrm{A}}:a\sqsubseteq s\}$ . Since ${S}_{\mathrm{A}}$ is closed under arbitrary fusions, ${a}_s$ is indeed an action. However, we cannot in general assume that all parts of actions will also be actions.
Call a situation pure if it contains no non-null action (one might for this reason think of it as a pure ‘state of nature’) and otherwise call it impure. We can plausibly assume:
Situation Decomposition: Any situation $s$ is the fusion of a pure situation and an action.
We might, similarly, call an action pure if it does not contain a pure situation (other than the null situation). Although Situation Decomposition has some plausibility, it is not so plausible to assume:
Action Decomposition: Any action is the fusion of a pure situation and a pure action.
Consider, for example, the action of raising my arm. This contains the situation of my arm rising, which arguably is a pure situation, i.e., one that does not contain a non-null action. However, it is far from clear that it fuses with any pure action to form the action of raising my arm since this would appear to require an analysis of the action of my raising my arm into a purely physical and a purely mental component.
There are three kinds of models, corresponding to the three kinds of state space. A situation (or S-) model ${\boldsymbol{M}}_{\mathrm{I}}$ over the situation space ${\boldsymbol{S}\kern-1.2pt}_{\mathrm{I}}=({S}_{\mathrm{I}},{\sqsubseteq}_{\mathrm{I}})$ is a triple $({S}_{\mathrm{I}},{\sqsubseteq}_{\mathrm{I}},{| \cdot |}_{\mathrm{I}})$ , where ${| \cdot |}_{\mathrm{I}}$ (the indicative valuation) is a function taking each indicative atom $\mathrm{s}$ into a pair of multi-sets $| \mathrm{s}|^{+}_{\mathrm{I}}$ and $| \mathrm{s}|^{-}_{\mathrm{I}}$ of situations (the respective truth- and falsity-makers of $\mathrm{s}$ ). Relative to such a model, we can then assign a multi-set of truth-makers $| \mathrm{S}|^{+}_{\mathrm{I}}$ and a multi-set $| \mathrm{S}|^{-}_{\mathrm{I}}$ of falsity-makers to each indicative sentence S in accordance with the clauses given for the multi-set semantics in Section 4.
For the purposes of the extended normal form theorem, we assume that the situation models are definite, i.e., that $| \mathrm{s}| ^{+}_{\mathrm{I}}$ for each indicative atom $\mathrm{s}$ is singleton. This means that we can take the underlying logic for indicative formulas to be given by CS + E17 and that we can assume that, for any realization scheme $\Sigma$ for an indicative formula S, S will be provably $\Sigma$ -equivalent in CS + E17 to a standard conjunctively non-repetitive normal form.
An action (A-) model ${\boldsymbol{M}}_{\mathrm{A}}$ over the action space ${\boldsymbol{S}\kern-1.2pt}_{\mathrm{A}}=({S}_{\mathrm{A}},{\sqsubseteq}_{\mathrm{A}})$ is a triple $({S}_{\mathrm{A}},{\sqsubseteq}_{\mathrm{A}},{| \cdot |}_{\mathrm{A}})$ , where ${| \cdot |}_{\mathrm{A}}$ (the imperative valuation) is a function taking each imperative A-atom $\mathrm{a}!$ into a pair of sets $| \mathrm{a}!| ^{+}_{\mathrm{A}}$ and $| \mathrm{a}!| ^{-}_{\mathrm{A}}$ of actions (the respective actions in compliance with or in contravention to a!). Relative to such a model, we can then assign a set of compliance-makers $| \mathrm{P}| ^{+}_{\mathrm{A}}$ and a set $| \mathrm{P}| ^{-}_{\mathrm{A}}$ of contravention-makers to each $\to$ -free imperative P constructed from the imperative A-atoms in accordance with the clauses given for the standard set-theoretic semantics in Section 3. Since the semantics is set-theoretic, we can take the underlying logic to be CS + E16 and any such formula P will therefore be provably equivalent to a standard disjunctive non-repetitive normal form.
Finally, a situation-action (S/A) model ${\boldsymbol{M}}_\mathrm{I,A}$ over the situation–action space ${\boldsymbol{S}\kern-1.2pt}_{I,A}=({S}_{\mathrm{I}},{S}_{\mathrm{A}},\sqsubseteq )$ is a quintuple $({S}_{\mathrm{I}},{S}_{\mathrm{A}},\sqsubseteq, {| \cdot |}_{\mathrm{I}},{| \cdot |}_{\mathrm{A}})$ , where $({S}_{\mathrm{I}},{S}_{\mathrm{A}},\sqsubseteq, {| \cdot |}_{\mathrm{I}})$ is a situation model and $({S}_{\mathrm{I}},{S}_{\mathrm{A}},\sqsubseteq, {| \cdot |}_{\mathrm{A}})$ is an action model. Thus a situation–action model enables us, separately, to interpret indicative and imperative formulas, though not the conditional imperatives in which the two kinds of formulas come together. We shall make a critical assumption about any situation–action model. Suppose $|\mathrm{a}!|^{+}_{\mathrm{A}}=\{{a}_1,{a}_2,\dots \}$ and $| \mathrm{a}!| ^{-}_{\mathrm{A}}=\{{b}_1,{b}_2,\dots \}$ , where the ${a}_1,{a}_2,\dots$ and the ${b}_1,{b}_2,\dots$ are chosen to be pairwise distinct. Then $| \mathrm{a}| ^{+}_{\mathrm{I}}=[{a}_1,{a}_2,\dots ]$ and $| \mathrm{a}| ^{-}_{\mathrm{I}}=[{b}_1,{b}_2,\dots ]$ . In other words, the interpretation of the A-atom $\mathrm{a}!$ and the corresponding indicative atom $\mathrm{a}$ should be coordinated so that the truth-makers for indicative $\mathrm{a}$ are the actions in compliance with imperatival $\mathrm{a}!$ and the falsity makers for $\mathrm{a}$ are the actions in contravention to $\mathrm{a}!$ .
This assumption gives rise to an issue. For whereas a state that is the truth-maker for ‘you shut the door’ may well be an action in compliance with ‘(you) shut the door’, it is far from clear that any state that is a truth-maker for ‘you did not shut the door’ need be an action in compliance with ‘do not shut the door’. For suppose, upon hearing you command ‘do not shut the door’, that I race to the door with the intention of shutting it but trip and end up leaving the door open. Then it is plausible to suppose that what I do is not in compliance with the imperative ‘do not shut the door’. For this would appear to require, not merely that I fail to shut the door, but that I refrain from shutting the door.Footnote 4
This means that in order to ensure that the truthmakers for ‘you do not shut the door’ are the same as the ‘actions’ compliant with ‘do not shut the door’, we must either adopt a narrower view of what the truth-makers might be or a broader view of what the actions might be. I am inclined to think that for most purposes we should adopt the former view. For we may suppose that under normal circumstances accidents like the one above will not happen and that, given that a negative imperative has been invoked, the agent will only fail to perform the required action by refraining from performing that action.
7 Plans
In extending the semantics that we earlier gave for categorical imperatives in terms of compliance- and contravention-conditions to conditional imperatives, we face a basic question. What should we take to be the nature of the items or ‘states’ in compliance with or in contravention to a conditional imperative? What, for example, should we take to be in compliance with the imperative ‘if it rains then take an umbrella’?
One natural answer is that we should take it to be an action, as before, but one whose compliance with the imperative is relative to a situation. Thus relative to the situation in which it rains, the action of taking an umbrella will be in compliance with the imperative, while, relative to a situation in which it is not rainy, the null action will be in compliance with the imperative. The clauses for the various connectives will then also be relativized to a situation. Thus relative to any given situation, we may take the actions in compliance with a conjunctive imperative to be the fusions of those actions, which, relative to the given situation, are in compliance with its respective conjuncts.
Unfortunately, this will not in general give us what we want. Consider the following two imperatives:
-
(1) (if it rains take an umbrella and if it is sunny take a parasol) or (if it rains wear a coat and if it is sunny wear a hat) ( $(\mathrm{R}\to \mathrm{U}!)\wedge (\mathrm{S}\to \mathrm{P}!)\vee ((\mathrm{R}\to \mathrm{C}!)\wedge (\mathrm{S}\to \mathrm{H}!)$ );
-
(2) (if it rains take an umbrella and if it is sunny wear a hat) or (if it rains wear a coat and if it is sunny take a parasol) ( $(\mathrm{R}\to \mathrm{U}!)\wedge (\mathrm{S}\to \mathrm{H}!)\vee ((\mathrm{R}\to \mathrm{C}!)\wedge (\mathrm{S}\to \mathrm{P}!)$ ).
The two imperatives are clearly different in their import. In preparing for the first, one will have an umbrella and a parasol or a coat and a hat at hand, while, in preparing for the second, one will have an umbrella and a hat or a coat and a parasol at hand. But in any situation, the same actions will be in compliance with each of the two imperatives. Thus in the situation in which it rains, the actions in compliance with either imperative will be taking an umbrella or wearing a coat and, in the situation in which it is sunny, the actions in compliance with either imperative will be taking a parasol or wearing a hat. What the present semantics ignores is an interdependence that may exist between what is required in different situations. Thus in the first case, taking an umbrella in the situation in which it rains is to be paired with taking a parasol in the situation in which it is sunny, while, in the second case, it is to be paired with wearing a hat.
We may avoid this difficulty by packaging the situation s and the action $a$ into a single item, something which we might represent by the ordered pair $(s,a)$ . We might think of $(s,a)$ as a conditional action, the action of doing $a$ conditional upon $s$ , where the performance of this action requires nothing in case $s$ does not obtain and requires the performance of $a$ (or better: the performance of $a$ in the situation $s$ ) in case $s$ does obtain.Footnote 5 These conditional actions can then be fused in a natural way. Thus the fusion of $(s,a)$ and $(t,b)$ , for $s\ne t$ , will be a complex action, which we can represent as $\{(s,a),(t,b)\}$ and which will consist in doing $a$ in situation $s$ and $b$ in situation $t$ . The previous problem then disappears for, using an obvious notation, $\{(r,u),(s,p)\}$ , for example, will be in compliance with the first imperative but not the second.
A pleasing simplification to the present approach is available to us. For presumably, we can identify the fusion of the states $(s,{a}_1),(s,{a}_2),\dots$ , where the first component $s$ is always the same, with $(s,({a}_1\sqcup {a}_2\sqcup \cdots ))$ , and presumably, we can identify the case in which, relative to a situation $s$ , nothing has been required of us, with the conditional action $(s,\square )$ (where □, recall, is the null action). But this means that the items in compliance with a conditional imperative or with a truth-functional compound of conditional imperatives can be taken to be total plans, i.e., with functions which associate each situation with a single action. We can, moreover, identify any action a in compliance with a categorical imperative with the conditional action $(\square, a)$ of doing $a$ in the null situation. This then means that we can treat total plans, telling us what is to be done in each situation, as the compliance- and contravention-makers for all imperatives.
This plan-based semantics is suggestive of a richer, more subjective, understanding of imperatives. It was perhaps true all along that we should think of the action in compliance with an imperative, such as ‘shut the door’, not simply as the action of shutting the door but as the action of shutting the door by way of conforming to the imperative (or what it prescribes). But we can now think of an imperative as telling us, not simply what to do, but what to plan on doing. Thus the item in conformity with the conditional imperative ‘take an umbrella if it rains’ will now be the adoption of a plan to take an umbrella if it rains (or perhaps we should say the effective adoption, so that the plan is indeed acted upon should the occasion arise). Similarly, the item in conformity with the positive categorical imperative ‘shut the door’ will be an (effective) decision to shut the door and the item in conformity with the negative categorical imperative ‘do not shut the door’ will be an effective decision not to shut the door. Thus from this perspective, what an imperative most immediately requires is an internal change in our readiness to act rather than an external change in how we actually do act. I am not saying that this understanding of imperatives is forced upon us, but it is one that naturally arises when conditional imperatives are in play and when the agent is indeed capable of making decisions or of planning for future contingencies. In such a case, the imperative, if successful, will serve to ‘prime’ the agent to do what the imperative requires.
Let us now make the previous informal discussion more precise. Suppose ${\boldsymbol{S}\kern-1.2pt}_\mathrm{I,A}=({S}_{\mathrm{I}},{S}_{\mathrm{A}},\sqsubseteq )$ is an S/A space. A plan $p$ in ${\boldsymbol{S}\kern-1.2pt}_\mathrm{I,A}$ is then a (total) function from ${S}_{\mathrm{I}}$ into ${S}_{\mathrm{A}}$ . Intuitively, a plan tells the agent what to do in each situation $s\in {S}_{\mathrm{I}}$ . We use $S^{+}_{\mathrm{P}}$ to denote the set of all plans in ${\boldsymbol{S}\kern-1.2pt}_\mathrm{I,A}$ (the ‘ $+$ ’ here indicates fullness not positivity), and, given $p,q\in S^{+}_{\mathrm{P}}$ , we define the relation $\sqsubseteq ^{+}_{\mathrm{P}}$ of part on plans in usual point-wise fashion:
Thus one plan $p$ is said to be part of another if what it enjoins in any situation is part of what the other plan enjoins in that situation.
There are two variants on this notion of a plan that we should mention even though they will not be pursued. Under the first, a plan $p$ is a partial function from the set of situations to the set of actions. With each partial plan $p$ may be associated the corresponding total plan ${p}^{+}$ , where:
-
${p}^{+}[s]=p[s]\;\mathrm{when}\;p[s]\;\mathrm{is}\kern0.17em \mathrm{defined}$ ,
-
$= \square\ \mathrm{otherwise}$ .
However, one cannot, conversely, recover $p$ from ${p}^{+}$ since it may be that ${p}^{+}={q}^{+}$ even though $p$ , say, takes the value $\square$ for a specific situation $s$ for which $q$ takes no value, and, on a certain highly fine-grained conceptions of content, this difference in the situations on which a plan is defined may be regarded as relevant to the meaning of an imperative.
The other variant is to allow a plan $p$ to be indeterminate so that its value $p[s]$ for a given situation $s$ can be a non-empty set of actions (or also the empty set if partiality is also allowed). However, it may be argued that any indeterminate plan can just as well be viewed as a disjunction of determinate plans (for which the value $p[s]$ is always a single action). Thus adopting the plan of doing $a$ or $b$ in situation $s$ and $c$ or $d$ in situation $t$ can be viewed as adopting the plan to do $a$ in $s$ and $c$ in $t$ or the plan to do $a$ in $s$ and $d$ in $t$ or the plan to do $b$ in $s$ and $c$ in $t$ or the plan to do $b$ in $s$ and $d$ in $t$ . There would therefore appear to be no need to appeal to indeterminate plans in developing a semantics for conditional imperatives.
However, there may well be a need to consider indeterminate transitions in the case of counterfactuals and other conditional constructions. Thus even though the imperative ‘if it rains then take an umbrella or wear a coat’ can be taken to be equivalent to ‘if it rains then take an umbrella or if it rains then wear a coat’, it is not so clear that the counterfactual ‘if it were to rain then you would take an umbrella or wear a coat’ should be taken to be equivalent to ‘if it were to rain then you would take an umbrella or if it were to rain then you would wear a coat’. Thus in a more general theory of conditionals we should allow for the route from antecedent to consequent to correspond to an indeterminate transition.
With each S/A space ${\boldsymbol{S}\kern-1.2pt}_{I,A}=({S}_{\mathrm{I}},{S}_{\mathrm{A}},\sqsubseteq )$ may be associated the full planning space ${\boldsymbol{S}\kern-1.2pt}_\mathrm{I,A,P}^{+}=({S}_{\mathrm{I}},{S}_{\mathrm{A}},S^{+}_{\mathrm{P}},\sqsubseteq )$ and the full plan space $\boldsymbol{S}^{+}_{\mathrm{P}}=(S^{+}_{\mathrm{P}},\sqsubseteq ^{+}_{\mathrm{P}})$ . $\boldsymbol{S}^{+}_{\mathrm{P}}$ is, of course, the ‘functional’ space from the situation space ${\boldsymbol{S}\kern-1.2pt}_{\mathrm{I}}$ into the action space ${\boldsymbol{S}\kern-1.2pt}_{\mathrm{A}}$ . It is readily verified that $\boldsymbol{S}^{+}_{\mathrm{P}}$ is indeed a state space, whose bottom element ${\square}_{\mathrm{P}}$ is the function $p$ on ${S}_{\mathrm{I}}$ whose value $p(s)$ is always ${\square}_{\mathrm{A}}=\square$ and whose top element ${\blacksquare}_{\mathrm{P}}$ is the function $p$ on ${S}_{\mathrm{I}}$ whose value $p(s)$ is always ${\blacksquare}_{\mathrm{A}}$ .
However, our interest will often not be in all of the plans of $S^{+}_{\mathrm{P}}$ but only in a subset of ‘admissible’ plans that are subject to certain constraints. Accordingly, a (closed) planning space is taken to be a structure ${\boldsymbol{S}\kern-1.2pt}_\mathrm{I,A,P}$ of the form $({S}_{\mathrm{I}},{S}_{\mathrm{A}},{S}_{\mathrm{P}},{\sqsubseteq}_{\mathrm{P}})$ , where the plan space ${\boldsymbol{S}\kern-1.5pt}_{\mathrm{P}}=({S}_{\mathrm{P}},{\sqsubseteq}_{\mathrm{P}})$ is a subspace of the full plan space $\boldsymbol{S}^{+}_{\mathrm{P}}=(S^{+}_{\mathrm{P}},\sqsubseteq ^{+}_{\mathrm{P}})$ subject to the condition that for each plan $p$ in $S^{+}_{\mathrm{P}}$ there is a plan $q\sqsupseteq ^{+}_{\mathrm{P}}\;p$ in ${S}_{\mathrm{P}}$ . Thus, according to this condition, any possible plan can always be extended to an admissible plan. Where it is evident from the context, we may drop the subscript ‘ $\mathrm{P}$ ’ or ‘ $^{+}_{\mathrm{P}}$ ’ from $\sqsubseteq$ .
Since the plan space ${\boldsymbol{S}\kern-1.2pt}_{\mathrm{P}}$ is complete, it follows that there will be a least plan in ${\boldsymbol{S}\kern-1.2pt}_{\mathrm{P}}$ containing any given plan $p$ of $S^{+}_{\mathrm{P}}$ , which we dub the closure ${p}^{* }$ of $p$ . The operation: $p\to {p}^{* }$ has the standard features of a closure operation with respect to $\sqsubseteq_{\mathrm{P}}$ :
-
$p\ {\sqsubseteq}_{\mathrm{P}}\ {p}^{\ast}$
-
$p\ {\sqsubseteq}_{\mathrm{P}}\ q\Rightarrow {p}^{* }{\sqsubseteq}_{\mathrm{P}}\ {q}^{\ast}$
-
${p}^{\ast \ast }\ {\sqsubseteq}_{\mathrm{P}}\ {p}^{* }$
appeal to which will often be implicit in what follows. A plan $p$ of $S^{+}_{\mathrm{P}}$ is itself said to be closed if $p={p}^{* }.$ Clearly, the closed plans of $S^{+}_{\mathrm{P}}$ are simply the plans of $S_{\mathrm{P}}$ .
We should note that the fusion of plans ${p}_1,{p}_2,\dots$ in ${\boldsymbol{S}\kern-1.4pt}_{\mathrm{P}}$ will be ${p}^{* }$ , where $p={p}_1\sqcup {p}_2\sqcup \cdots$ is the fusion of ${p}_1,{p}_2,\dots$ in $\boldsymbol{S}^{+}_{\mathrm{P}}.$ In other words, taking $\bigsqcup^{*}$ to be the fusion operation for the closed subspace, ${\bigsqcup}^*{p}_k= (\bigsqcup {p}_k)^*$ , and there is no reason why ${\bigsqcup }^* {p}_k$ in general should be identical to $\bigsqcup {p}_k$ .
The closure operation: $p\to {p}^{* }$ on plans could, in principle, obliterate all distinctions between plans by making ${p}^{* }$ always equal to ${\blacksquare}_{\mathrm{P}}$ .Footnote 6 We shall therefore sometimes find it helpful to suppose that there is some constraint in how far ${p}^{* }$ can go in extending a given plan $p$ . Set ${p}^{\oplus}[s]=({a}_s\sqcup $ $\bigsqcup Rg(p))$ . Then the operation $p\to {p}^{* }$ is said to be bound if ${p}^{\ast}\sqsubseteq {p}^{\oplus }$ . We might think of this condition as telling us that, in defining ${p}^{* }(s)\sqsupseteq p(s)$ , the only actions we can add to $p(s)$ are those already in $s$ or in the range of $p$ .
8 Conditions on plans
There are a number of natural conditions one might wish to impose on a plan space. They will not make a difference to the logics considered below. However, they will make a significant difference to the logics considered in part IV, once we allow for the coordination $a\iff a!$ between indicative and imperative atoms, so that the indicative atom ${a}_k$ corresponding to an imperative atom ${a}_k!$ is allowed to occur in the antecedent of a conditional imperative.
One condition often introduced in the context of a functional space is
From a technical point of view, this is a very desirable condition. However, under our semantics, it would require us to accept Antecedent Strengthening (so that from ‘if it rains then take an umbrella’ we can infer ‘if it rains and there is a strong wind then take an umbrella’), and since we not wish in general to accept Antecedent Strengthening, nor can we accept Monotonicity.
One condition I have previously suggested is
In other words, when the situation on which a plan operates contains an action then the plan can be taken to require that action. Since ${a}_s$ is the maximal action to be contained in the situation s, we can state the condition more simply in the form
When $s$ is an action $a$ then ${a}_s=a$ and, so in this special case, we get the more familiar
However, we cannot in general assume:
since $p[s]$ will be an action of which the situation $s$ might not be a part.
Another condition we wish to accept is
This says that what we are to do under a given plan should be the same as what we are to do under partial compliance with the plan. Thus we cannot evade or enhance the demands of a plan through partial compliance. This condition will later be of critical importance in establishing the validity of Imperative Detachment.
We may divide the condition into two parts
The first says that what we are to do under a given plan should contain (looking up) what we are to do under partial compliance with the plan, while the second says that what we are to do under partial compliance should contain (looking down) what we are to do under the given plan.
In the special case in which $t=p[s]$ , we get:
What we are to do under a given plan should be the same as what we are to do under complete compliance with the plan. When $s$ is an action $a$ , this becomes:
Given Action Inclusion, $a\sqsubseteq p[a]$ and so this becomes the familiar closure condition:
and so, in particular,
To illustrate: perhaps in the null situation, I am (according to the plan) to turn on the stove and, in a situation in which I turn on the stove, I am to light the stove; it then follows, according to the condition, that in the null situation, I am (according to the plan) to turn on the stove and light it. However, we do not in general have
since $p[s]$ may not contain $s$ .
I wish now to introduce a general method for getting from a plan that may not satisfy some of the above conditions to one that does. To this end, it will be helpful to introduce some familiar material on fixed points, which will be presupposed in what follows. (The less technically inclined reader may omit the rest of this section and the related material in Section 11).
Suppose $F$ is an inclusive operation on plans, i.e., $p\sqsubseteq F(p)$ for any plan $p$ . Given a plan $p$ , define a (transfinite) sequence of plans ${p}_0,{p}_1,\dots$ by
-
${p}_0\kern1.0em =p$ ,
-
${p}_{\beta +1}=F\!({p}_{\beta}),\mathrm{and}$
-
${p}_{\lambda}\kern1.0em =\bigsqcup \{{p}_{\zeta }{:}\ \zeta <\lambda \}$ .
We may then establish by induction that ${p}_{\alpha}\sqsubseteq {p}_{\beta}$ whenever $\alpha <\beta$ ; for ${p}_{\beta}\sqsubseteq F({p}_{\beta})={p}_{\beta +1}$ , given that $F$ is inclusive, and, for $\zeta <\lambda$ , ${p}_{\zeta}\sqsubseteq$ $\bigsqcup \{{p}_{\zeta }:\varsigma <\lambda \}={p}_{\lambda }.$ It follows, by considerations of cardinality, that there will be a least ordinal $\alpha$ for which ${p}_{\alpha}={p}_{\alpha +1}=F({p}_{\alpha})$ . We dub ${p}_{\alpha}$ the inclusive fixed point of $F$ and, where $\alpha$ is this least ordinal, we set ${p}^F={p}_{\alpha }$ .
When the operation $F$ is also monotonic, then ${p}^F$ is the least fixed point of $F$ to contain $p$ . For suppose $q$ is a fixed point containing $p$ , i.e., $F\kern-0.8pt(q){\kern-1pt}={\kern-1pt}q$ and $q{\kern-1pt}\sqsupseteq{\kern-1pt} p$ . We may show by induction on $\alpha$ that ${p}_{\alpha}\sqsubseteq q$ . For: when $\alpha =0$ , ${p}_0=p\sqsubseteq q$ by supposition; when $\alpha =\beta +1$ , then ${p}_{\beta}\sqsubseteq q$ by IH, and so ${p}_{\beta +1}=F\kern-0.8pt({p}_{\beta})\sqsubseteq F\kern-0.8pt({q}_{\beta})=q$ by the monotonicity of $F$ ; and when $\alpha =\lambda$ , ${p}_{\zeta}\sqsubseteq q$ for each $\zeta <\lambda$ by IH and so ${p}_{\lambda}=$ $\bigsqcup \{{p}_{\zeta }:\zeta <\lambda \}.$ Moreover, when $F$ is monotonic, the operation $p\to {p}^F$ is also monotonic. For suppose $p\sqsubseteq q$ . Then ${p}^F$ is the least fixed point of $F$ to contain $p$ . But ${q}^F$ is a fixed point of $F$ that contains $p$ and so ${p}^F\sqsubseteq {q}^F.$
We shall later find it useful to consider a generalization of the above construction. Suppose that ${<}{\boldsymbol{F}}_{\alpha }{>}$ is a sequence of inclusive operations on plans (the ${\boldsymbol{F}}_{\alpha }$ ’s may repeat and, for simplicity, we have taken ${<}{\boldsymbol{F}}_{\alpha }{>}$ to be defined on all ordinals $\alpha$ ). Given a plan $p$ , we define a corresponding sequence of plans ${<}{p}_{\alpha }{>}$ by
-
${p}_0\kern1.0em =p,$
-
${p}_{\beta +1}={\boldsymbol{F}}_{\beta}({p}_{\beta}),\mathrm{and}$
-
${p}_{\lambda}\kern1.0em =\bigsqcup \{{p}_{\zeta }{:}\ \zeta <\lambda \}$ .
The only difference from the previous definition is that the operation applied at the successor stage $\beta +1$ is allowed to vary with $\beta$ . Again, by considerations of cardinality, there will be a least ordinal $\alpha$ for which ${p}_{\alpha}={p}_{\alpha +\zeta }$ for all ordinals $\zeta$ . For this least ordinal $\alpha$ , we may then set ${p}^{\boldsymbol{F}}={p}_{\alpha }.$ And again, we may show, in the same way as before, that when each of the operations $p\to {\boldsymbol{F}\!}_{\alpha }(p)$ is monotonic then ${p}^{\boldsymbol{F}}$ is the least fixed point containing $p$ for all of the ${\boldsymbol{F}\!}_{\alpha }$ and that the operation: $p\to {p}^{\boldsymbol{F}}$ is monotonic.
I now wish to use the above constructions to show how any plan can be minimally extended to a plan subject to the previous constraints.
Lemma 6 (Follow-Up)
For any plan $p$ there is a least plan ${p}^{\uparrow}\sqsupseteq p$ conforming to the condition:
where the operation $p\to {p}^{\uparrow }$ is monotonic.
Proof. Define the operation $p\to p\uparrow$ on plans (to be distinguished from $p\to {p}^{\uparrow }$ ) by:
-
(1) The operation: $p\to p\uparrow$ is inclusive.
Pf: Since $p[s]\sqsupseteq \square$ , $p[s]=p[s\sqcup \square ]\sqsubseteq \bigsqcup \{p[s\sqcup t]:t\sqsubseteq p[s]\}=p\uparrow [s]$ .
Define p↑ as the inclusive fixed point (with respect to the operation: $p\to p\uparrow$ ).
-
(2) Suppose that $p\sqsubseteq q$ and that $q[s]\sqsupseteq q[s\sqcup t]$ whenever $q[s]\sqsupseteq t$ . Then ${p}^{\uparrow}\sqsubseteq q$ .
Pf: We show by induction on $\alpha$ that ${p}_{\alpha}\sqsubseteq q,$ where the sequence of the ${p}_{\alpha }$ is defined as above by reference to the operation $p\to p\uparrow$ . Since ${p}^{\uparrow }$ is of the form ${p}_{\alpha }$ for some $\alpha$ , it will follow that ${p}^{\uparrow}\sqsubseteq q$ .
-
(i) $\alpha =0$ . By supposition.
-
(ii) $\alpha =\beta +1$ . Then ${p}_{\alpha}={p}_{\beta}\uparrow$ , where ${p}_{\beta}\uparrow [s]=\bigsqcup \{{p}_{\beta}[s\sqcup t]:t\sqsubseteq {p}_{\beta}[s]\}$ . So we need to show ${p}_{\beta}[s\sqcup t]\sqsubseteq q[s]$ whenever $t\sqsubseteq {p}_{\beta}[s]$ . But ${p}_{\beta}\sqsubseteq q$ by IH. Hence ${p}_{\beta}[s]\sqsubseteq q[s]$ , and so, given $t\sqsubseteq {p}_{\beta}[s]$ , $t\sqsubseteq q[s]$ . So by the condition imposed upon $q$ in (2), $q[s\sqcup t]\sqsubseteq q[s]$ . But by IH, ${p}_{\beta}[s\sqcup t]\sqsubseteq q[s\sqcup t]$ , and so ${p}_{\beta}[s\sqcup t]\sqsubseteq q[s]$ .
-
(iii) $\alpha =\lambda$ . Then ${p}_{\alpha}=\bigsqcup \{{p}_{\zeta }:\zeta <\alpha \}$ . By IH, ${p}_{\zeta}\sqsubseteq q$ for each $\zeta <\alpha$ , and so ${p}_{\alpha}=$ $\bigsqcup \{{p}_{\zeta }:\zeta <\alpha \}\sqsubseteq q$ .
-
(3) ${p}^{\uparrow}[s]\sqsupseteq t\Rightarrow {p}^{\uparrow}[s]\sqsupseteq {p}^{\uparrow}[s\sqcup t]$ .
Pf: Suppose ${p}^{\uparrow}[s]\sqsupseteq t$ . Then ${p}^{\uparrow}[s]={p}^{\uparrow}\uparrow [s]\sqsupseteq {p}^{\uparrow}[s\sqcup t]$ by definition of ${p}^{\uparrow }$ and $\uparrow$ .
-
(4) The operation: $p\to p\uparrow$ is monotonic.
Pf: Suppose $p\sqsubseteq q$ . Then:
-
$p\uparrow =\bigsqcup \{p[s\sqcup t]:t\sqsubseteq p[s]\}$
-
$\sqsubseteq {\kern-1pt}\bigsqcup \{q[s\sqcup t]{\kern-1pt}:{\kern-1pt}t\sqsubseteq q[s]\}$ $(\mathrm{since}\kern0.17em \mathrm{if}\;t\sqsubseteq p[s]\;\mathrm{then}\;t{\kern-1pt}\sqsubseteq{\kern-1pt} q[s]\;\mathrm{and}\;p[s{\kern-1pt}\sqcup{\kern-1pt} t]\sqsubseteq{\kern-1pt} q[s{\kern-1pt}\sqcup{\kern-1pt} t])$ $=q\uparrow.$
From (2) and (3) it follows that ${p}^{\uparrow }$ is the least plan $q\sqsupseteq p$ conforming to Follow-Up and from (4) it follows, from our earlier observation, that the operation $p\to p^{\uparrow}$ is also monotonic.
Lemma 7 (Follow-Down)
For any plan $p$ there is a least plan ${p}^{\downarrow}\sqsupseteq p$ conforming to the condition
where the operation $p\to {p}^{\downarrow }$ is monotonic.
Pf: Note that the condition imposed on ${p}^{\downarrow }$ is equivalent to
So let us define the operation $p\to p\downarrow$ on plans by
-
(1) The operation $p\to p\downarrow$ is inclusive.
Pf: We set $u=s$ and $t=\square$ in the definition of $p\downarrow [u]$ . Since $u=u\sqcup \square$ and $p[u]\sqsupseteq \square$ , it follows that $p[u]=\bigsqcup \{p[s]:u=s\sqcup \square$ and $p[s]\sqsupseteq \square \}\sqsubseteq \bigsqcup \{p[s]:u=s\sqcup t$ and $p[s]\sqsupseteq t\}=p\downarrow [u]$ .
Define ${p}^{\downarrow }$ as the inclusive fixed point (with respect to the operation: $p\to p\downarrow$ ).
-
(2) Suppose that $p\sqsubseteq q$ and that $q[u]\sqsupseteq q[s]$ whenever $u=s\sqcup t$ and $q[s]\sqsupseteq t$ . Then ${p}^{\downarrow}\sqsubseteq q$ .
Pf: It suffices to show ${p}_{\alpha}\sqsubseteq q$ , where the sequence of ${p}_{\alpha }$ ’s is defined as before, but by reference to the operation $p\to p\downarrow$ . The proof is by induction on $\alpha$ . The cases in which $\alpha =0$ or $\alpha =\lambda$ are straightforward, and so let us focus on the case in which $\alpha =\beta +1$ . Then ${p}_{\alpha}={p}_{\beta}{\downarrow}$ , where ${p}_{\beta}\downarrow [u]=\bigsqcup \{{p}_{\beta}[s]:u=s\sqcup t$ and ${p}_{\beta}[s]\sqsupseteq t\}$ . So we need to show that $q[u]\sqsupseteq {p}_{\beta}[s]$ whenever $u=s\sqcup t$ and ${p}_{\beta}[s]\sqsupseteq t$ , i.e., that $q[s\sqcup t]\sqsupseteq {p}_{\beta}[s]$ whenever ${p}_{\beta}[s]\sqsupseteq t$ . But ${p}_{\beta}\sqsubseteq q$ by IH. Hence ${p}_{\beta}[s]\sqsubseteq q[s]$ , and so, given $t\sqsubseteq {p}_{\beta}[s]$ , $t\sqsubseteq q[s].$ By the condition imposed in (2) upon $q$ , $q[s]\sqsubseteq q[s\sqcup t]$ , and so ${p}_{\beta}[s]\sqsubseteq q[s\sqcup t]$ .
-
(3) ${p}^{\downarrow}[s]\sqsupseteq t\Rightarrow {p}^{\downarrow}[s\sqcup t]\sqsupseteq {p}^{\downarrow}[s]$ .
Pf: Suppose ${p}^{\downarrow}[s]\sqsupseteq t$ . Then ${p}^{\downarrow}[s\sqcup t]={p}^{\downarrow}\downarrow [s\sqcup t]\sqsupseteq {p}^{\downarrow}[s]$ by definition of ${}^{\downarrow }$ and $\downarrow$ .
-
(4) The operation $p\to p\downarrow$ is monotonic.
Pf: Suppose $p\sqsubseteq q$ . Then
From (2) and (3) it follows that ${p}^{\downarrow }$ is the least plan $q\sqsupseteq p$ conforming to Follow-Down and from (4) it follows that the operation $p\to {p}^{\downarrow }$ is also monotonic.
Lemma 8 (Semi-Inclusion)
For any plan $p$ , there is a least plan ${p}^{\to}\sqsupseteq p$ satisfying the condition
where the operation $p\to {p}^{\to}$ is monotonic.
Proof. Given a plan $p$ , define its expansion ${p}^{\to }$ by:
Clearly, ${p}^{\to}\sqsupseteq p$ and satisfies Semi-Inclusion. It is also the least plan containing p to satisfy Semi-Inclusion. For if $q\sqsupseteq p$ and satisfies Semi-Inclusion, then $p[s]\sqsubseteq q[s]$ and ${a}_s\sqsubseteq q[s]$ and so ${p}^{\to}[s]=p[s]\sqcup {a}_s\sqsubseteq q[s]$ .
Also, if $p\sqsubseteq q$ then ${p}^{\to}[s]=p[s]\sqcup {a}_s\sqsubseteq q[s]\sqcup {a}_s={q}^{\to}[s]$ .
Lemma 9 (Monotonicity)
For any plan $p$ there is a least plan $p\,\check{}\ \sqsupseteq p$ satisfying the condition
where the operation $p\to p\,\check{}$ is monotonic.
Proof. Set $p\,\check{}\ [s]=\bigsqcup \{p[s^{\prime}]:s^{\prime}\sqsubseteq s\}$ . Then the operation $s\to p\,\check{}\ (s)$ is monotonic. For suppose $s\sqsubseteq t$ . Then $p\,\check{}\ [s]=\bigsqcup \{p[s^{\prime}]:s^{\prime}\sqsubseteq s\}\sqsubseteq \bigsqcup \{p[s^{\prime}]:s^{\prime}\sqsubseteq t\}=p\,\check{}\ [t]$ .
Now suppose $q$ is a monotonic plan containing $p$ . Then for $s^{\prime}\sqsubseteq s,$ $q[s]\sqsupseteq q[s^{\prime}]$ since $q$ is monotonic and $q[s^{\prime}]\sqsupseteq p[s^{\prime}]$ since $q\sqsupseteq p$ . Consequently, $q\,\check{}\ [s]\sqsupseteq \bigsqcup \{p[s^{\prime}]:s^{\prime}\sqsubseteq s\}=p\,\check{}\ [s]$ .
Also, if $p\sqsubseteq q$ then $p\,\check{}\ [s]=\bigsqcup \{p[s^{\prime}]:s^{\prime}\sqsubseteq s\}\sqsubseteq \bigsqcup \{q[s^{\prime}]:s^{\prime}\sqsubseteq s\}=q\,\check{}\ [s]$ and so the operation $p\to p\,\check{}$ is monotonic.
We are now in a position to combine our various results. Let us call the various conditions mentioned above the standard conditions. Then:
Theorem 10. Given any combination of the standard conditions, there is, for any plan $p$ , a least plan ${p}^{\ast}\sqsupseteq p$ satisfying the combination of conditions.
Proof. Let us illustrate the method of proof for the case of Follow-Through (the combination of Follow-Up and Follow-Down). We wish to show that, for any plan $p$ , there is a least plan ${p}^{\updownarrow}\sqsupseteq p$ satisfying Follow-Through, where the operation: $p\to {p}^{\updownarrow }$ is monotonic. We therefore define a sequence ${<}{\boldsymbol{F}}_{\alpha }{>}$ of operations on plans by letting ${\boldsymbol{F}}_{\alpha }$ be the operation: $p\to {p}^{\uparrow}$ when $\alpha$ is of the form $\lambda +2n$ and letting ${\boldsymbol{F}}_{\alpha }$ be the operation: $p\to {p}^{\downarrow }$ when $\alpha$ is of the form $\lambda +2n+1$ . We then take ${p}^{\updownarrow }$ to be the inclusive fixed point ${p}^{\updownarrow }$ with respect to the sequence ${<}{\boldsymbol{F}}_{\alpha }{>}$ . ${p}^{\updownarrow \uparrow}={p}^{\updownarrow }$ and so ${p}^{\updownarrow }$ conforms to Follow-Up, and ${p}^{\updownarrow \downarrow}={p}^{\updownarrow }$ and so conforms to Follow-Down. Since the operations $p\to {p}^{\uparrow}$ and $p\to {p}^{\downarrow }$ are monotonic, it follows that ${p}^{\updownarrow }$ is the least fixed point of the operations $p\to {p}^{\uparrow }$ and $p\to {p}^{\downarrow }$ to contain $p$ and hence the least plan containing p to conform to Follow-Up.
This result means that if we define the admissible plans ${S}_{\mathrm{P}}$ of a plan space ${\boldsymbol{S}\kern-1.4pt}_{\mathrm{P}}=({S}_{\mathrm{P}},\sqsubseteq ^{+}_{\mathrm{P}}\upharpoonleft {S}_{\mathrm{P}})$ to be those conforming to a combination of standard conditions, then ${\boldsymbol{S}\kern-1.4pt}_{\mathrm{P}}$ will be a state space in which the restricted relation $\sqsubseteq ^{+}_{\mathrm{P}}\upharpoonleft {S}_{\mathrm{P}}$ of part-whole is indeed complete. For given any set $\{{p}_1,{p}_2,\dots \}$ of admissible plans, there will be a least plan conforming to the conditions that contains ${p}_1\sqcup {p}_2\sqcup \cdots$ . Let us also note that, by examining how the standard operations $p\to {p}^{* }$ have been defined, we may easily verify that each of them is bound, i.e., that ${p}^{\ast}\sqsubseteq {p}^{\oplus }$ .
9 Plans, partial plans, and actions
In what follows, I assume given a situation–action space ${\boldsymbol{S}\kern-1.2pt}_{I,A}=({S}_{\mathrm{I}},{S}_{\mathrm{A}},\sqsubseteq )$ and an associated plan space ${\boldsymbol{S}\kern-1.2pt}_{\mathrm{P}}=({S}_{\mathrm{P}},\sqsubseteq )$ . Recall that, for each plan $p$ in $S^{+}_{\mathrm{P}}$ , there will be a smallest plan ${p}^{\ast}\sqsupseteq p$ in ${\boldsymbol{S}\kern-1.4pt}_{\mathrm{P}}$ .
As already noted, there is a natural extension—the completion— ${p}^{+}$ of a partial plan $p$ , which is a function from ${S}_{\mathrm{I}}$ into ${S}_{\mathrm{A}}$ , where, for any state $s$ ,
-
${p}^{+}[s]=p[s]$ when $s\in Dm(p)$ , and
-
${p}^{+}[s]=\square$ otherwise.
Thus ${p}^{+}$ takes the null value $\square$ when $p$ would otherwise be undefined. We may then let the closure ${p}^{* }$ of a partial plan $p$ be ${p}^{+\ast }$ . This definition agrees, of course, with the original definition of ${p}^{* }$ when $p$ is itself a total function.
Given a situation $s$ and an action $a$ , let $s\hookrightarrow a$ be the plan ${\{{<}s,a{>}\}}^{+}$ and let $s\to a$ be the plan ${(s\hookrightarrow a)}^{\ast }$ . Thus $s\hookrightarrow a$ is the plan $p$ such that
-
$p[t]=a$ when $t=s$ , and
-
$=\square$ otherwise
and $s\to a$ is its closure ${p}^{* }$ . We should think of $(s\to a)$ as the singular plan from $s$ to $a$ . It embodies the instruction to do $a$ in situation $s$ , but subject to closure.
Each closed plan is the fusion of its component singular plans:
Lemma 11. For any closed plan $p$ , $p={\bigsqcup}^* \{(s\to p[s]){:}\ s\in {S}_{\mathrm{I}}\}$ .
Proof. Set $q={\bigsqcup}^* \{(s\to p[s]){:}\,s\in {S}_{\mathrm{I}}\}$ . Then $q\sqsubseteq p$ . For by the definition of $\hookrightarrow$ , it follows that, for any $s\in {S}_{\mathrm{I}}$ , $(s\hookrightarrow p[s])[s]=p[s]$ and $(s\hookrightarrow p[s])[t]=\square \sqsubseteq p[s]$ when $t\ne s$ . So $(s\hookrightarrow p[s])\sqsubseteq p$ ; so $(s\to p[s])={(s\hookrightarrow p[s])}^{\ast}\sqsubseteq {p}^{\ast}=p$ (since $p$ is closed); so $\bigsqcup \{(s\to p[s]){:}\ s\in {S}_{\mathrm{I}}\}\sqsubseteq p$ ; and so $q= {\bigsqcup}^* \{(s\to p[s]){:}\ s\in {S}_{\mathrm{I}}\}\sqsubseteq {p}^{\ast}=p$ .
Also, $p\sqsubseteq q$ . For given any $s\in {S}_{\mathrm{I}}$ , $p[s]=(s\hookrightarrow p[s])[s]\sqsubseteq {(s\hookrightarrow p[s])}^{\ast}[s]=(s\to p[s])[s]\sqsubseteq \bigsqcup \{(s\to p[s]){:}\,s\in {S}_{\mathrm{I}}\}\sqsubseteq {\bigsqcup}^* \{(s\to p[s]){:}\,s\in {S}_{\mathrm{I}}\}=q$ .
We may obtain a natural embedding of actions into plans by letting ${p}_a$ , for each action $a$ , be $\square \hookrightarrow a$ and by letting ${p}_a^{\ast}$ be ${({p}_a\!)}^{\ast }$ ( $=(\square \to a)={(\square \hookrightarrow a)}^{\ast }$ ). Thus each action is identified with the plan of doing that action in the null situation. We might think of ${p}_a^{\ast }$ as being reached in three steps: first, by identifying $a$ with the partial function $\{{<}\square, a{>}\}$ ; then, by identifying the partial function with the total function $(\square \hookrightarrow a)={\{{<}\square, a{>}\}}^{+}$ ; and, finally, by taking the closure $(\square \to a)={(\square \hookrightarrow a)}^{\ast }$ of $(\square \hookrightarrow a)$ .
The map: $a\to {p}_a^{\ast }$ will normally constitute an embedding of the action space ${\boldsymbol{S}\kern-1.2pt}_{\mathrm{A}}$ into the plan space ${\boldsymbol{S}\kern-1.2pt}_{\mathrm{P}}$ :
Lemma 12. Let $S^{\mathrm{A}}_{\mathrm{P}}=\{{p}_a^{\ast }:a\in {\boldsymbol{S}\kern-1.2pt}_{\mathrm{A}}\}$ and let $\boldsymbol{S}^{\mathrm{A}}_{\mathrm{P}}$ be the restriction of the plan space ${\boldsymbol{S}\kern-1.2pt}_{\mathrm{P}}$ to $S^{\mathrm{A}}_{\mathrm{P}}$ . Then, as long as the underlying closure operation $p\to {p}^{\ast}$ is bound, the map $a\to {p}_a^{\ast}$ constitutes an isomorphism between ${\boldsymbol{S}\kern-1.2pt}_{\mathrm{A}}$ and $\boldsymbol{S}^{\mathrm{A}}_{\mathrm{P}}$ .
Proof. Recall that ${p}^{\oplus }(s)=({a}_s\sqcup \bigsqcup Rg(p))$ . Setting $p=(\square \hookrightarrow a)$ and $s=\square$ , we see that ${a}_s=\square$ , that $Rg(p)=\{\square, a\}$ , and hence that $\bigsqcup Rg(p))=a.$ So, given that the closure operation $p\to {p}^{* }$ is bound, $a\sqsubseteq {(\square \hookrightarrow a)}^{\ast}[\square ]=p^{*}_{\mathrm{a}}[\square ]\sqsubseteq {p}^{\oplus }(s)=a$ , and so $p^{*}_{\mathrm{a}}[\square ]=a$ . It follows that the map $a\to p^{*}_{\mathrm{a}}$ is one–one. For if $a\ne b$ then $p^{*}_{\mathrm{a}}[\square ]=a$ and $p^{*}_{\mathrm{b}}[\square ]=b$ and so $p^{*}_{\mathrm{a}}\ne p^{*}_{\mathrm{b}}$ .
It remain to establish that the map preserves $\sqsubseteq$ . So suppose $a\sqsubseteq b$ . Then $\square \hookrightarrow a\sqsubseteq \square \hookrightarrow b$ . Hence $p^{*}_{\mathrm{a}}=(\square \hookrightarrow a){}^{\ast})\sqsubseteq {(\square \hookrightarrow b)}^{\ast}=p^{*}_{\mathrm{b}}$ . Now suppose . Then and so .
This result tells us that we may identify an action $a$ with the corresponding plan $p^{*}_{\mathrm{a}}$ and this will enable us to present the semantics for categorical and conditional imperatives exclusively in terms of plans.
10 Core conditionalization
We introduce the key operation of conditionalization on plans—dealing with core non-closed plans in the present section and with closed plans in the following section.
Given a situation $s$ and a plan $p$ , we let the (core) conditionalization $(s\hookrightarrow p)$ of $p$ on $s$ be the plan
Thus the conditional plan $s\hookrightarrow p$ is the fusion of the singular plans that send the state $s\sqcup t$ to the action $p[t]$ . We might think of this definition in terms of resetting the value of the default situation from $\square$ to $s$ , so that $(s\hookrightarrow p)$ will take the same value when $s$ is the default as $p$ takes when $\square$ is the default.
Say $t\equiv u\;(\mathit{\operatorname{mod}}\;s)$ if $t\sqcup s=u\sqcup s$ . Clearly $\equiv (\mathit{\operatorname{mod}}\;s)$ is an equivalence relation. We have the following alternative characterizations and elementary properties of $(s\hookrightarrow p)$ :
Lemma 13. For any situations $s$ , $t$ , and $u$ and plans $p$ and ${p}^{+}$ :
-
(i) $(s\hookrightarrow p)[u]=\bigsqcup \{p[t]:s\sqcup t=u\}$ .
-
(ii) $(s\hookrightarrow p)[t]=\bigsqcup \{p[t^{\prime}]:t\equiv t^{\prime}(\mathit{\operatorname{mod}}\;s)\}\;\mathit{when}\;t\sqsupseteq s$ $= \square \mathit{otherwise}.$
-
(iii) $(s\hookrightarrow p)[t]\sqsupseteq p[t]\;\mathit{when}\;t\sqsupseteq s,\mathit{and}$
-
(iv) For $p\sqsubseteq {p}^{+}$ , $(s\hookrightarrow p)\sqsubseteq (s\hookrightarrow {p}^{+}).$ (Right Monotonicity)
-
(v) For $s\sqsubseteq {s}^{+}\sqsubseteq t$ , $(s\hookrightarrow p)[t]\sqsubseteq ({s}^{+}\hookrightarrow p)[t]$ , and
for $s\sqsubseteq t,p[t]\sqsubseteq (s\hookrightarrow p)[t].$ (Left Monotonicity)
Proof.
-
(i) $(s\hookrightarrow p)[u]=\bigsqcup \{(s\sqcup t)\hookrightarrow p[t]:t\in {S}_{\mathrm{I}}\}[u]$
$=\bigsqcup \{((s\sqcup t)\hookrightarrow p[t])[u]:t\in {S}_{\mathrm{I}}\}$
$=\bigsqcup \{((s\sqcup t)\hookrightarrow p[t])[u]:s\sqcup t=u\}\sqcup \bigsqcup \{((s\sqcup t)\hookrightarrow p[t])[u]:$ $s\sqcup t\ne u\}$
$=\bigsqcup \{p[t]:s\sqcup t=u\}\sqcup \bigsqcup \{\square :s\sqcup t\ne u\}$
$=\bigsqcup \{p[t]:s\sqcup t=u\}$ .
-
(ii) $(s\hookrightarrow p)[t]=\bigsqcup \{p[t^{\prime}]:s\sqcup t^{\prime}=t\}$ by (i). But when $t\sqsupseteq s$ , $s\sqcup t^{\prime}=t$ iff $s\sqcup t^{\prime}=s\sqcup t$ , i.e., iff $t\equiv t^{\prime}(\mathit{\operatorname{mod}}\;s)$ and, when , there are no $t^{\prime }$ such that $s\sqcup t^{\prime}=t$ and so $\bigsqcup \{p[t^{\prime}]:s\sqcup t^{\prime}=t\}=\square$ .
-
(iii) From (ii).
-
(iv) From (i).
-
(v) Suppose $s\sqsubseteq {s}^{+}\sqsubseteq t.$ By (ii), $(s\hookrightarrow p)[t]=\bigsqcup \{p[t^{\prime}]:t^{\prime}\equiv t\;(\mathit{\operatorname{mod}}\;s)\}$ and $({s}^{+}\hookrightarrow p)[t]=\bigsqcup \{p[t^{\prime}]:t^{\prime}\equiv t\;(\mathit{\operatorname{mod}}\;{s}^{+})\}$ . But $t^{\prime}\equiv t\;(\mathit{\operatorname{mod}}\;s)$ implies $t^{\prime}\equiv t\;(\mathit{\operatorname{mod}}\;{s}^{+})$ given $s\sqsubseteq {s}^{+}$ and so $\bigsqcup \{p[t^{\prime}]:t^{\prime}\equiv t\;(\mathit{\operatorname{mod}}\;s)\}\sqsubseteq \bigsqcup \{p[t^{\prime}]:t^{\prime}\equiv t\;(\mathit{\operatorname{mod}}\;{s}^{+})\}$ .
Also when $s\sqsubseteq t$ , $(s\hookrightarrow p)[t]=\bigsqcup \{p[t^{\prime}]:t^{\prime}\equiv t\;(\mathit{\operatorname{mod}}\;s)\}\sqsupseteq p[t]$ since $t\equiv t\;(\mathit{\operatorname{mod}}\;s)$ .
Use of these results, and of (i) in particular, will often be implicit.
These results shows that the conditional plan $s\hookrightarrow p$ only ‘kicks in’ within a situation containing the antecedent situation $s$ and that, when the plan does kick in, it assumes a cumulative interpretation. The value of $s\hookrightarrow p$ at $s\sqcup t$ in such a case is not merely $p[t]$ but the result of adding to $p[t]$ any other values $p[t^{\prime}]$ for which $s\sqcup t=s\sqcup t^{\prime }$ . We might justify the cumulative interpretation on the grounds that there is in general no way to privilege any particular $t^{\prime }$ for which $s\sqcup t=s\sqcup t^{\prime }$ , and so all such $t^{\prime }$ should be included.
The operation $\hookrightarrow$ has been used in the context $s\hookrightarrow a$ , for $a$ an action, and also in the context $s\hookrightarrow p$ , for $p$ a plan. We may show that the two uses are in conformity with one another:
Lemma 14. For any situation $s$ and action $a$ , $s\hookrightarrow {p}_a=s\hookrightarrow a$ .
Proof.
For $t=s$ :
For $t\ne s$ :
But then the $t^{\prime}\ne \square$ and so $(\square \hookrightarrow a)[t^{\prime}]=\square$ . Hence:
Thus, in either case $(s\hookrightarrow {p}_a)[t]=(s\hookrightarrow a)[t]$ and hence $s\hookrightarrow {p}_a=s\hookrightarrow a$ .
We establish some basic algebraic properties of conditionalization:
Lemma 15. For situations $s$ , $s1$ , and $s2$ and plans $p,p1,p2,\dots$ :
-
(i) $(\square \hookrightarrow p)=p$ .
-
(ii) ${s}_1\hookrightarrow ({s}_2\hookrightarrow p)=({s}_1\sqcup {s}_2)\hookrightarrow p$ .
-
(iii) $s\hookrightarrow ({p}_1\sqcup {p}_2\sqcup \cdots )=(s\hookrightarrow {p}_1)\sqcup (s\hookrightarrow {p}_2)\sqcup \cdots$ .
-
(iv) $s\hookrightarrow {\square}_{\mathrm{P}}={\square}_{\mathrm{P}}$ .
Proof.
-
(i) $(\square \hookrightarrow p)[t]=\bigsqcup \{p[t^{\prime}]{:}\ t^{\prime}\sqcup \square =t\}$
$\hspace{42pt}= \bigsqcup \{p[t^{\prime}]{:}\ t^{\prime}=t\}$
$\hspace{42pt}=p[t]$ .
-
(ii) $({s}_1\hookrightarrow ({s}_2\hookrightarrow p))[t]=\bigsqcup \{({s}_2\hookrightarrow p)[t^{\prime}]{:}\ t^{\prime}\sqcup {s}_1=t\}$
$\hspace{74pt}=\bigsqcup \{\;\bigsqcup \{p[t^{\prime\prime}]{:}\ t^{\prime\prime}\sqcup {s}_2=t^{\prime}\}{:}\ t^{\prime}\sqcup {s}_1=t\}$
$\kern7.439995em =\bigsqcup \{p[t^{\prime\prime}]{:}\ t^{\prime\prime}\sqcup {s}_2=t^{\prime}\mathrm{and}\;t^{\prime}\sqcup {s}_1=t\}$
$\hspace{74pt}=\bigsqcup \{p[t^{\prime\prime}]{:}\ t^{\prime\prime}\sqcup {s}_2\sqcup {s}_1=t\}$
$\hspace{74pt}=({s}_1\sqcup {s}_2)\hookrightarrow p$ .
-
(iii) $(s\hookrightarrow ({p}_1\sqcup {p}_2\sqcup \cdots )[t]=\bigsqcup \{({p}_1\sqcup {p}_2\sqcup \cdots )[t^{\prime}]{:}\ t^{\prime}\sqcup s=t\}$
$\hspace{88pt}=\bigsqcup \{({p}_1[t^{\prime}]\sqcup {p}_2[t^{\prime}]\sqcup \cdots ){:}\ t^{\prime}\sqcup s=t\}$
$\hspace{88pt}=\bigsqcup ({p}_1[t^{\prime}]{:}\ t^{\prime}\sqcup s=t\}\sqcup \bigsqcup \{({p}_2[t^{\prime}]{:}\ t^{\prime}\sqcup s=t\}\sqcup \cdots$
$\hspace{88pt}=(s\hookrightarrow {p}_1)[t]\sqcup (s\hookrightarrow {p}_2)[t]\sqcup \cdots$
$\hspace{88pt}= ((s\hookrightarrow {p}_1)\sqcup (s\hookrightarrow {p}_2) \sqcup \cdots) [t]$ .
-
(iv) $(s\hookrightarrow {\square}_{\mathrm{P}})[t]=\bigsqcup \{{\square}_{\mathrm{P}}[t^{\prime}]{:}\ t^{\prime}\sqcup s=t\}$
$\hspace{44pt}=\bigsqcup \{\square {:}\ t^{\prime}\sqcup s=t\}$
$\hspace{44pt}=\square$
$\hspace{44pt}={\square}_{\mathrm{P}}[t]$ .
11 Closed conditionalization
We wish to extend the previous results for core conditionalization to closed conditionalization. Recall that, given a closure operation $p\to {p}^{* }$ on plans, we define closed conditionalization by:
Our aim is to extend the results on $\hookrightarrow$ in Lemmas 14 and 15 to $\to$ . To this end, we assume that the closure operation $\ast$ satisfies the following conditionFootnote 7
In other words, the external closure of a conditional will contain the internal closure of the conditional, in which we close on the consequent of the conditional rather than on the conditional itself. (We shall later show that the standard closure operations on plans conform to Regularity.)
We first note the analogue of Lemma 14:
Lemma 16. Suppose that $\ast$ is a closure operation conforming to Regularity. Then for any situation $s$ and action $a$ ,
Proof. We need to show ${(s\hookrightarrow p^{*}_{\mathrm{a}})}^{\ast}=(s\hookrightarrow a)$ *. Now $(s\hookrightarrow p^{*}_{\mathrm{a}})\sqsubseteq (s\hookrightarrow {p}_a)$ * by Regularity. So: ${(s\hookrightarrow p^{*}_{\mathrm{a}})}^{\ast}\sqsubseteq (s\hookrightarrow {p}_a)$ ** by Monotonicity of $\ast$
$=(s\hookrightarrow {p}_a)$ *
$=(s\hookrightarrow a)$ * by Lemma 14.
Also ${(s\hookrightarrow a)}^{\ast}=(s\hookrightarrow {p}_a)$ * by Lemma 14
$\sqsubseteq (s\hookrightarrow p^{*}_{\mathrm{a}})$ * by Right Monotonicity of $\hookrightarrow$ (Lemma 13(iv)).
We also have the analogue of Lemma 15, with $\hookrightarrow$ replaced by $\to$ and with the operation $\sqcup $ on plans replaced by the operation $\sqcup^{\ast }$ on closed plans:
Lemma 17. Suppose that the closure operation $\ast$ on plans conforms to Regularity. Then for any situations $s$ , $s_1$ , and $s_2$ and closed plans $p,p1,p2,\dots$ :
-
(i) $(\square \to p)=p$ ;
-
(ii) ${s}_1\to ({s}_2\to p)=({s}_1\sqcup {s}_2)\to p$ ;
-
(iii) $s\to ({p}_1\sqcup^{\ast }{p}_2\sqcup^{\ast}\cdots )=(s\to {p}_1)\sqcup^{\ast}(s\to {p}_2)\sqcup^{\ast}\cdots$ ;
-
(iv) $s\to \square ^{*}_{\mathrm{P}}=\square ^{*}_{\mathrm{P}}$ .
Proof.
-
(i) $(\square \to p)=(\square \hookrightarrow p)$ *
$\hspace{30pt}=p$ * by Lemma 15(i)
$\hspace{30pt}=p$ given that $p$ is closed.
-
(ii) For the one direction, observe that:
$$\begin{align*}({s}_1\sqcup {s}_2)\hookrightarrow p&={s}_1\hookrightarrow ({s}_2\hookrightarrow p)\quad \mathrm{by\ Lemma}\ {15}(\mathrm{ii})\\&\sqsubseteq {s}_1\hookrightarrow ({s}_2\hookrightarrow p)\quad \mathrm{by\ Right\ Monotonicity\ of}\ \hookrightarrow.\end{align*}$$
Hence:
For the other direction, observe that:
Hence:
-
(iii) For the one direction, observe that:
$$\begin{align*}s\hookrightarrow {({p}_1\sqcup {p}_2\sqcup \cdots )}^{\ast}&\sqsubseteq {(s\hookrightarrow ({p}_1\sqcup {p}_2\sqcup \cdots ))}^{\ast }\qquad\quad \ \ \ \, \mathrm{by\ Regularity}\\&={((s\hookrightarrow {p}_1)\sqcup (s\hookrightarrow {p}_2)\sqcup \cdots )}^{\ast }\quad \mathrm{by\ Lemma}\ {15}(\mathrm{iii})\ \&\\ &\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad \mathrm{Monotonicity}\\&\sqsubseteq {({(s\hookrightarrow {p}_1)}^{\ast}\sqcup {(s\hookrightarrow {p}_2)}^{\ast}\sqcup \cdots )}^{\ast }\\&=(s\to {p}_1)\sqcup^{\ast}(s\to {p}_2)\sqcup \ast \cdots .\end{align*}$$
Hence:
For the other direction, observe that:
and so ${(s\hookrightarrow {p}_k)}^{\ast}\sqsubseteq {(s\hookrightarrow ({p}_1\sqcup^{\ast }{p}_2\sqcup^{\ast}\cdots ))}^{\ast }$ .
Hence:
-
(iv) For the one direction,
$$\begin{align*}(s\to \square ^{*}_{\mathrm{P}})&={(s\hookrightarrow {(\square_{\mathrm{P}})}^{\ast})}^{\ast }\\&\sqsubseteq {(s\hookrightarrow \square_{\mathrm{P}})}^{\ast \ast }\quad \mathrm{by\ Regularity}\\&={(s\hookrightarrow \square_{\mathrm{P}})}^{\ast }\\& =\square ^{*}_{\mathrm{P}}\qquad\qquad\ \ \ \mathrm{by\ Lemma}\ {15}(\mathrm{iv}).\end{align*}$$
For the other direction, note that $\square ^{*}_{\mathrm{P}}\sqsubseteq {(s\hookrightarrow \square ^{*}_{\mathrm{P}})}^{\ast}=(s\to \square ^{*}_{\mathrm{P}})$ since $\square ^{*}_{\mathrm{P}}\sqsubseteq {q}^{\ast}$ for any plan $q$ .
We now develop a method by which we can show that an operation on plans satisfies Regularity.
Lemma 18. Let ${<}{\boldsymbol{F}}_{\alpha }{>}$ be a sequence of inclusive monotonic operations on plans and, relative to any given plan $p$ , ${<}{p}_{\alpha }{>}$ the corresponding sequence of plans defined by reference to ${<}{\boldsymbol{F}}_{\alpha }{>}$ (as in Section 8). Suppose each ${\boldsymbol{F}\!}_{\alpha}$ conforms to Regularity. Then for each ordinal $\alpha$ :
Proof. By induction on $\alpha$ .
Lemma 19. (Regularity of Follow-Up)
The operation $p\to {p} \uparrow $ conforms to Regularity.
Proof. We first show that for arbitrary plans $p$ and $q$ :
(*) if $p[t]\sqsubseteq q[s\sqcup t]$ for all situations $t$ then ${p} \uparrow[t]\sqsubseteq {q} \uparrow[s\sqcup t]$ for all situations $t$ .
Pf: Suppose $p[t]\sqsubseteq q[s\sqcup t]$ for all situations $t$ . Then $u\sqsubseteq p[t]$ implies $u\sqsubseteq q[s\sqcup t]$ , and so $\{u:u\sqsubseteq p[t]\}\subseteq \{u:u\sqsubseteq q[s\sqcup t]\}$ . Also, given the supposition, $p[t\sqcup u]\sqsubseteq q[s\sqcup t\sqcup u]$ for any situation $u$ (setting $t{\kern-1pt}={\kern-1pt}t{\kern-1pt}\sqcup{\kern-1pt} u$ ). Consequently, ${p} \uparrow[t]{\kern-1pt}={\kern-1pt}\bigsqcup \{p[t\sqcup u]: u\sqsubseteq p[t]\}\sqsubseteq \bigsqcup \{q[s\sqcup t\sqcup u]:u\sqsubseteq q[s\sqcup t]\}={q} \uparrow[s\sqcup t]$ .
We also have
(**) $p[t^{\prime}]\sqsubseteq (s\hookrightarrow p)[s\sqcup t^{\prime}]$ for all $t^{\prime }$
since $(s\hookrightarrow p)[s\sqcup t^{\prime}]=\bigsqcup \{p[u]:s\sqcup u=s\sqcup t^{\prime}\}$
$\sqsupseteq \bigsqcup \{p[u]:u=t^{\prime}\}$
$=p[t^{\prime}]$ .
So applying (*) to (**), it follows that
(***) $({p} \uparrow)[t^{\prime}]\sqsubseteq {(s\hookrightarrow p)} \uparrow[s\sqcup t^{\prime}]$ for all $t^{\prime }$ .
But:
$(s\hookrightarrow ({p} \uparrow))[t]=\bigsqcup \{({p} \uparrow)[t^{\prime}]:s\sqcup t^{\prime}=t\}$
$\sqsubseteq \bigsqcup \{{(s\hookrightarrow p)} \uparrow[s\sqcup t^{\prime}]:s\sqcup t^{\prime}=t\}$ by (***)
= ${(s\hookrightarrow p)} \uparrow[t]$
and hence $\uparrow$ conforms to Regularity.
Lemma 20. (Regularity of Follow-Down)
The operation $p\to {p} \downarrow $ conforms to Regularity.
Proof. We compute $(s\hookrightarrow ({p} \downarrow))[t]$ and $((s\hookrightarrow p)\downarrow )[t]$ .
But it is then clear that $(s\hookrightarrow ({p} \downarrow))[t]\sqsubseteq ({(s\hookrightarrow p)} \downarrow)[t]$ . For $p[v]\sqsubseteq \bigsqcup \{p[x]{:}\ s\sqcup x=s\sqcup v\}$ and so, given that $w\sqsubseteq p[v]$ , $w\sqsubseteq \bigsqcup \{p[x]{:}\ s\sqcup x=s\sqcup v\}\}$ .
Lemma 21. (Regularity of Semi-Inclusion)
The operation $p\to {p}^{\to}\kern0.24em$ conforms to Regularity.
Proof.
while ${(s\hookrightarrow p)}^{\to}[t]=(s\hookrightarrow p)[t]\sqcup {a}_t$ .
But $\bigsqcup \{{a}_u{:}\ s\sqcup u=t\}=\square$ when and $\bigsqcup \{{a}_u{:}\ s\sqcup u=t\}={a}_t$ when $t\sqsupseteq s$ . Thus in either case,
Theorem 22. The operations of Follow-Up, Follow-Down, and Semi-Inclusion conform to Regularity.
The case for Monotonicity is somewhat more straightforward since we can then show:
Lemma 23. If the plan $p$ is monotonic, then:
-
$(s\hookrightarrow p)[t]=\square$ if , and
-
$(s\hookrightarrow p)[t]=p[t]$ otherwise,
and the plan $(s\hookrightarrow p)$ is itself monotonic.
Proof. $(s\hookrightarrow p)[t]=\bigsqcup \{p[u]{:}\ s\sqcup u=t\}$ . If then $(s\hookrightarrow p)[t]=\square$ . So suppose that $s\sqsubseteq t$ and $s\sqcup u=t$ . Then $u\sqsubseteq t$ and so, given that $p$ is monotonic, $p[u]\sqsubseteq p[t]$ . But $s\sqcup t=t$ , and so $(s\hookrightarrow p)[t]=\bigsqcup \{p[u]{:}\ s\sqcup u=t\}=p[t]$ .
Now suppose $t\sqsubseteq t^{\prime }$ . If then $(s\hookrightarrow p)[t]=\square$ and so $(s\hookrightarrow p)[t]\sqsubseteq (s\hookrightarrow p)[t^{\prime}]$ . So suppose $s\sqsubseteq t.$ Then $s\sqsubseteq t^{\prime }$ and so, by the first part, $(s\hookrightarrow p)[t]=p[t]\sqsubseteq p[t^{\prime}]=(s\hookrightarrow p)[t^{\prime}]$ .
We have so far distinguished between $\sqcup $ and $\sqcup^{\ast}$ and between $\square ^{*}_{\mathrm{P}}$ and $\square_{\mathrm{P}}$ , but from now on, when only closed plans are under consideration, we shall use $\sqcup $ in place of $\sqcup^{\ast}$ and $\square ^{*}_{\mathrm{P}}$ in place of $\square_{\mathrm{P}}$ .
12 Conditionalized prescriptions
By a proposition or propositional content is meant a multi-set of situations (i.e., a multi-subset of ${S}_{\mathrm{I}}$ ) and by a prescription or prescriptive content is meant a set of plans (i.e., a subset of ${S}_{\mathrm{P}}$ ). We understand propositions and prescriptions disjunctively. Thus a proposition, qua multi-set of situations, tells us that one of the situations in the multi-set obtains and a prescription, qua set of plans, tells us that one of the plans in the set is to be adopted. We shall use $S,T,U$ and the like for propositions and $P,Q,R$ and the like for prescriptions. Propositions provide the unilateral content of indicative formulas, while prescriptions provide the unilateral content of imperative formulas.
There is a condition on prescriptive content which we shall not accept but which is worth mentioning, since it enables us greatly to simplify the semantics:
Mix and Match: The plan $q\in P$ if for each situation $s$ , $q[s]=p[s]$ for some plan $p\in P$ .
This is a kind of independence condition: it tells us that what are to do in one situation is independent of what we are to do in another situation. Imagine an iterated prisoners’ dilemma with two players and consider a prescription for one of the players that contains the choice of the plans: defect regardless of whether the other player defects or cooperates; cooperate regardless of whether the other player defects or cooperates. If this prescription satisfies Mix and Match, then it must also contain all the other plans, such as defect if the other player cooperates and cooperate if the other player defects.
With each prescription $Q$ satisfying Mix and Match, we may associate the indeterminate plan ${p}_Q$ , where ${p}_Q[s]=\{q[s]:q\in Q\}$ . Conversely, $Q$ will consist of the corresponding determinate plans, i.e., it will be the set $\{q\in {S}_{\mathrm{P}}:q[s]\in {p}_Q[s]\}$ . Acceptance of Mix and Match enables us to simplify the semantics, since we may now represent the content of an imperative as a single indeterminate plan, telling us which actions will be in conformity with the imperative in any given situation. This notion of content, which involves a severe restriction on the semantics, should not of course be confused with the expansion of the semantics, in which the content of a conditional is represented as a set of indeterminate transitions.
We turn to the question of specifying the content of a conditional imperative. We had previously defined a conditionalized plan $s\to p,$ where $\to$ was an operation taking a situation $s$ and a plan $p$ into the plan $s\to p$ . We now wish to extend this operation to one that applies to a proposition $S$ in place of the situation $s$ and to a prescription $P$ in place of the plan $p$ and which delivers as output another prescription. This will then enable us to define the content of a conditional $\mathrm{S}\to \mathrm{P}$ as $S\to P,$ where $S$ is the indicative content of S and $P$ the prescriptive content of P.
We do this by means of the following two rules, the first ‘lifting’ to prescriptions on the right and the second to propositions on the left:
-
$(s\to P)=\{s\to p{:}\ p\in P\}$ ;
-
$(S\to P)=\bigsqcup\ [s\to P{:}\ s\in S]$ .
Some comments are in order:
-
(1) Note that $s\to p$ is a plan, while $s\to P$ and $S\to P$ are prescriptions—with $s\to P=\{s\to p{:}\ p\in P\}$ a set of plans and $S\to P=\bigsqcup\ \{s\to P{:}\ s\in S\}$ a fusion of prescriptions. $(s\to P)=\{s\to p{:}\ p\in P\}$ is understood disjunctively, i.e., as the ‘disjunction’ of the plans $s\to p$ for $p\in P$ , while $(S\to P)=\bigsqcup\ [s\to P{:}\ s\in S]$ is understood conjunctively, as the ‘conjunction’ of the plans $s\to P$ for $s\in S$ . Despite our more expansive employment of $\to$ , it should always be clear which particular use we have in mind.
-
(2) $S$ is a multi-set of situations, while $[s\to P{:}\ s\in S]$ is a corresponding multi-set of prescriptions (hence the use of the square brackets). Thus if $S=[{s}_0,{s}_0]$ then $[s\to P{:}\ s\in S]=[{s}_0\to P,{s}_0\to P]$ and so $(S\to P)=\bigsqcup\ [{s}_0\to P,{s}_0\to P]=({s}_0\to P)\sqcup ({s}_0\to P)$ , which may not be the same as $({s}_0\to P)$ (which is what we get when $S=[{s}_0]$ ), since it will allow the choice of $({s}_0\to p)\sqcup ({s}_0\to p^{\prime})$ for distinct plans $p,p^{\prime}\in P$ .
-
(3) Note the order of the definitions; we first lift to prescriptions and then to propositions. As we shall see, the reverse order can lead to different, and sometimes incorrect results.
-
(4) The three forms of conditionalization— $(s\to p)$ , $(s\to P)$ , and $(S\to P)$ —are in conformity with one another. For:
-
$(s{\kern-1pt}\to{\kern-1pt} \{p\}){\kern-1pt}={\kern-1pt}\{(s{\kern-1pt}\to{\kern-1pt} p)$ }, since $(s{\kern-1pt}\to{\kern-1pt} \{p\}){\kern-1pt}={\kern-1pt}\{s{\kern-1pt}\to{\kern-1pt} q{:}\ q{\kern-1pt}\in{\kern-1pt} \{p\}\}{\kern-1pt}={\kern-1pt}\{(s{\kern-1pt}\to{\kern-1pt} p)\}$ ;
and
-
$[s]{\kern-1pt}\to{\kern-1pt} P=(s{\kern-1pt}\to{\kern-1pt} P),\mathrm{since}\;([s]\to P)=\bigsqcup \{t\to P{:}\ t\in [s]\}=\bigsqcup \{s\to P\}$ $=s\to P$ .
-
(5) When $P=\varnothing$ , $(s\to P)=\{s\to p{:}\ p\in \varnothing \}=\varnothing$ and so, when $S\ne []$ (the empty multi-set) and $P=\varnothing$ , then $(S\to P)=\bigsqcup\ [\varnothing {:}\ s\in S]=\varnothing$ . However, when $S=[],$ $(S\to P)=\bigsqcup\ [s\to P{:}\ s\in []]={\square}_{\mathrm{P}}$ .
-
(6) The second of the two extensions is in line with the truthmaker semantics for the intuitionistic conditional given in [Reference Fine4].
We wish to show that conditional prescriptions $(S\to P)$ have some basic properties, more or less analogous to those under Lemma 17. This could be done algebraically, as before, but, it will turn out to be easier on the eye and something that will in any case be required to establish these results indirectly via their symbolic counterparts over a certain positive fragment of the language of imperatives.
So suppose we are given a (closed) planning space $\boldsymbol{S}=({S}_{\mathrm{I}},{S}_{\mathrm{A}},{S}_{\mathrm{P}},\sqsubseteq )$ . A positive prescriptive model $\boldsymbol{M}$ over $\boldsymbol{S}$ is then an ordered sextuple $({S}_{\mathrm{I}},{S}_{\mathrm{A}},{S}_{\mathrm{P}},\sqsubseteq, {| \cdot |}_{\mathrm{I}}\;{| \cdot |}_{\mathrm{P}})$ , where ${| \cdot |}_{\mathrm{I}}$ is a definite unilateral multi-set valuation over ${S}_{\mathrm{I}}$ for the indicative atoms and ${| \cdot |}_{\mathrm{P}}$ is a unilateral set-theoretic valuation over ${S}_{\mathrm{P}}$ (not ${S}_{\mathrm{A}}$ ) for the imperative atoms. In the results that follows, we shall find it convenient to adopt the notational convention under which the indicative atom $\mathrm{s}\in {S}_{\mathrm{I}}$ signifies the situation $s$ (i.e., ${|\mathrm{s}|}_{\mathrm{I}}=[s]$ ) and the imperative atom $\mathrm{p}$ signifies the plan $p\in {S}_{\mathrm{P}}$ (i.e., ${|\mathrm{p}|}_{\mathrm{P}}=\{p\}$ ) (this restriction on the imperative atoms will later be relaxed). We shall assume in what follows that the closure operation $\ast$ of $\boldsymbol{M}$ is subject to Regularity.
We define the positive indicative and imperative formulas by means of the following clauses:
-
IN1. $\top$ and $\perp$ and any indicative atom is a positive indicative formula.
-
IN2. If ${\mathrm{S}}_1,{\mathrm{S}}_2,\dots$ are two or more positive indicative formulas, then so are $({\mathrm{S}}_1\vee {\mathrm{S}}_2\vee \cdots )$ and $({\mathrm{S}}_1\wedge {\mathrm{S}}_2\wedge \cdots )$ .
-
PP1. ⊤! and ⊥! and any imperative atom is a positive imperative formula.
-
PP2. If ${\mathrm{P}}_1,{\mathrm{P}}_2,\dots$ are two or more positive imperative formulas, then so are $({\mathrm{P}}_1\vee {\mathrm{P}}_2\vee \cdots )$ and $({\mathrm{P}}_1\wedge {\mathrm{P}}_2\wedge \cdots )$ .
-
PP3. If $\mathrm{S}$ is a positive indicative formula and $\mathrm{P}$ a positive imperative formula, then $(\mathrm{S}\to \mathrm{P})$ is a positive imperative formula.
Note that we are not allowed to use $\neg$ in the formation of a positive indicative or prescriptive formula, although we do allow $\perp$ to be a positive indicative formula and $\perp !$ to be a positive prescriptive formula. Note also that we allow disjunctions and conjunctions of arbitrary length, in contrast to our previous definition. The exact identity of these disjunctions and conjunctions is not too important as long as we allow for the repetition of disjuncts and conjuncts.
Given a positive prescriptive model $\boldsymbol{M}$ , we may then:
-
(a) use the obvious extension of the multi-set semantics to define the unilateral content of the indicative formulas $\top$ , $\perp$ , $({\mathrm{S}}_1\vee {\mathrm{S}}_2\vee \cdots )$ and $({\mathrm{S}}_1\wedge {\mathrm{S}}_2\wedge \cdots )$ ;
-
(b) use the obvious extension of the standard set semantics to define the unilateral content of the prescriptive formulas $\top !$ , $\perp !$ , $({\mathrm{P}}_1\vee {\mathrm{P}}_2\vee \cdots )$ and $({\mathrm{P}}_1\wedge {\mathrm{P}}_2\wedge \cdots )$ (where $| \top !|$ is now the null plan ${\square}_{\mathrm{P}}$ ); and
-
(c) set $| \mathrm{S}\to \mathrm{P}| =| \mathrm{S}| \to | \mathrm{P}|$ for any positive indicative formula $\mathrm{S}$ and positive prescriptive formula $\mathrm{P}$ .
We extend the previous notational convention by taking $S$ to be $| \mathrm{S}|$ and $P$ to be $| \mathrm{P}|$ .
Suppose that $S=[{s}_1,{s}_2,\dots ]$ is a proposition within the model $\boldsymbol{M}$ . Then under our convention for designating situations and plans, it should be clear that $| {\mathrm{s}}_1\vee {\mathrm{s}}_1\vee \cdots | =[{s}_1,{s}_2,\dots ]$ , since and, similarly, that $| {\mathrm{p}}_1\vee {\mathrm{p}}_2\vee \cdots | =| {\mathrm{p}}_1| \cup | {\mathrm{p}}_2| \cup \cdots =\{{p}_1,{p}_2,\dots \}$ . It also follows directly from the clause for conjunction that $|{\mathrm{P}}_1\wedge {\mathrm{P}}_2\wedge \cdots |={P}_1\sqcup {P}_2\sqcup \cdots$ .
Recall that $\approx$ is used for identity in (unilateral) content. We can now establish almost directly from the definition of $(S\to P)$ that:
Lemma 24. Relative to any positive prescriptive model $\boldsymbol{M}$ :
-
(i) $\mathrm{s}\to ({\mathrm{p}}_1\vee {\mathrm{p}}_2\vee \cdots )\approx (\mathrm{s}\to {\mathrm{p}}_1)\vee (\mathrm{s}\to {\mathrm{p}}_2)\vee \cdots$ .
-
(ii) $({\mathrm{s}}_1\vee {\mathrm{s}}_1\vee \cdots )\to \mathrm{P}\approx ({\mathrm{s}}_1\to \mathrm{P})\wedge ({\mathrm{s}}_1\to \mathrm{P})\wedge \cdots$ .
Proof.
-
(i) $| s\to ({\mathrm{p}}_1\vee {\mathrm{p}}_2\vee \cdots )| =| \mathrm{s}| \to | {\mathrm{p}}_1\vee {\mathrm{p}}_2\vee \cdots )|$
$=[\mathrm{s}]\to (|{\mathrm{p}}_1|\cup |{\mathrm{p}}_2|\cup \cdots )$
$=[\mathrm{s}]\to (\{{p}_1\}\cup \{{p}_2\}\cup \cdots )$
$=[\mathrm{s}]\to \{{p}_1,{p}_2,\dots \}$
$=s\to \{{p}_1,{p}_2,\dots \}$
$=\{s\to {p}_1,s\to {p}_2,\dots \}$ by definition of $s\to P$
$=\{s\to {p}_1\}\cup \{s\to {p}_2\}\cup \cdots$
$=([\mathrm{s}]\to \{{p}_1\})\cup ([\mathrm{s}]\to \{{p}_2\})\cup \cdots$
$=| (\mathrm{s}\to {\mathrm{p}}_1)\vee (\mathrm{s}\to {\mathrm{p}}_2)\vee \cdots |$ .
-
(ii) $| ({\mathrm{s}}_1\vee {\mathrm{s}}_1\vee \cdots )\to \mathrm{P}| =| (({\mathrm{s}}_1\vee {\mathrm{s}}_1\vee \cdots ))| \to | \mathrm{P}|$
$=[{s}_1,{s}_1,\dots ]\to | \mathrm{P}|$
$=\bigsqcup\ [{s}_1\to |\mathrm{P}|,{s}_1\to |\mathrm{P}|,\dots ]$ by definition of $S\to P$
$=\bigsqcup\ [[s1]\to |\mathrm{P}|,[s2]\to |\mathrm{P}|,\dots ]$
$=| ({\mathrm{s}}_1\to \mathrm{P})\wedge ({\mathrm{s}}_2\to \mathrm{P})\wedge \cdots | $ .
We can, in a similar way, establish semantic counterparts to the results under Lemma 17.
Lemma 35. Relative to any positive prescriptive model $\boldsymbol{M}$ :
-
(i) $(\top \to \mathrm{p})\approx \mathrm{p}$ .
-
(ii) ${\mathrm{s}}_1\to ({\mathrm{s}}_2\to \mathrm{p})\approx ({\mathrm{s}}_1\wedge {\mathrm{s}}_2)\to \mathrm{p}$ .
-
(iii) $\mathrm{s}\to ({\mathrm{p}}_1\wedge {\mathrm{p}}_2\wedge \cdots )\approx (\mathrm{s}\to {\mathrm{p}}_1)\wedge (\mathrm{s}\to {\mathrm{p}}_2)\wedge \cdots$ .
-
(iv) $\mathrm{s}\to \top !=\top !$ .
Proof. Straightforward, given the corresponding results under Lemma 17.
We shall call the equivalences under the two previous lemmas the basic reductions. In the next section, we shall use them to derive other reductions, with a view to establishing a normal form theorem, but for now we shall use them to provide a more direct definition of conditionalization.
Call $\boldsymbol{p}$ a hyper-plan if it is a multi-map from a multi-set of situations $S$ into a set of plans $P$ . Hyper-plans differ from straight plans in two significant respects: first, their range is a set of plans rather than a set of actions, and, second, their domain is a multi-subset of situations rather than the total set of all situations.
Given a hyper-plan $\boldsymbol{p}$ , its collapse $\boldsymbol{p}\Downarrow$ (which we also denote by $p$ ) is $\bigsqcup\ [s\to \boldsymbol{p}[s]:s\in Dm(\boldsymbol{p})].$ Note that each $s\to \boldsymbol{p}[s]$ is a plan and so $p=\bigsqcup\ [s\to \boldsymbol{p}[s]:s\in Dm(\boldsymbol{p})]$ is also a plan. Since $Dm(\boldsymbol{p})$ is a multi-set, we may, for fixed $s\in Dm(\boldsymbol{p})$ , have different $s\to \boldsymbol{p}[s]$ in $[s\to \boldsymbol{p}[s]{:}\ s\in Dm(\boldsymbol{p})]$ . These must then all be fused in forming $\bigsqcup\ [s\to \boldsymbol{p}[s]:s\in Dm(\boldsymbol{p})]$ . We might think of a hyper-plan as a higher-order plan, the plan of performing the first-order plan p [s] in situation s. The collapsing function $\Downarrow$ then enables us to regard this higher plan $\boldsymbol{p}$ as a first-order plan $p$ , obtained by fusing all of the plans $s\to \boldsymbol{p}[s]$ , where each $s\to \boldsymbol{p}[s]$ is the result of conditionalizing the plan recommended by the hyper-plan in the given situation to that very situation.
Lemma 36 (Collapse of the Hyper-Plan)
For any proposition $S$ and prescription $P,(S\to P)=\{\boldsymbol{p}{\Downarrow}\! :{\kern-1.2pt\boldsymbol{p}}\;\mathrm{a}\;\mathrm{multi}-\mathrm{map}\;\mathrm{from}\;S\;\mathrm{to}\;P\}$ .
Proof. Let us suppose $S=[s_1,s_2,\dots ]$ and $P=\{p_1,p_2,\dots \}$ . Then:
$\hspace{-10pt}| S\to P| =| {\bigvee}_m\mathrm{s}_m\to {\bigvee}_n\mathrm{p}_n\;|$
$=| {\bigwedge}_m(\mathrm{s}_m\to {\bigvee}_n\mathrm{p}_n\;)|$ Basic Reduction
$=| {\bigwedge}_m{\bigvee}_n(\mathrm{s}_m\to \mathrm{p}_n)|$ Basic Reduction
$=| {\bigvee}_{p,m}(\mathrm{s}_m\to \mathrm{p}_{\rho (m)})$ : ρ a map from m = 1, 2, … to n = 1, 2, …}| Distribution
$=\{| {\bigwedge}_m({\mathrm{s}}_{\mathrm{m}}\to \mathrm{p}_{\rho (m)}\;)|$ : ρ a map from m = 1, 2, … to n = 1, 2, …}
$=\{| \bigwedge [(\mathrm{s}\to \boldsymbol{\rho} (\mathrm{s})):\mathrm{s}=\mathrm{s}_1,\mathrm{s}_2,\dots ]$ |: ρ a multi-map from [ $\mathrm{s}_1$ , $\mathrm{s}_2$ , …] to {p1, p2, …}}
$=\{\;\bigsqcup\ [|\mathrm{s}\to \boldsymbol{\rho} (\mathrm{s})|:\mathrm{s}=\mathrm{s}_1,\mathrm{s}_2,\dots ]:\boldsymbol{\rho}\;\mathrm{a}\;\mathrm{multi}-\mathrm{map}\;\mathrm{from}$ [ $\mathrm{s}_1$ , $\mathrm{s}_2$ , …] to {p1, p2, …}}
$=\{\;\bigsqcup\ [\mathrm{s}\to \boldsymbol{p}(\mathrm{s}):\mathrm{s}=$ $\mathrm{s}_1$ , $\mathrm{s}_2$ , $\dots ]:\boldsymbol{p}$ a multi-map from [ $\mathrm{s}_1$ , $\mathrm{s}_2$ , …] to { $\mathrm{p}_1$ , $\mathrm{p}_2$ , …}}
$=\{\boldsymbol{p}\Downarrow :\boldsymbol{p}\;\mathrm{a}\;\mathrm{multi}-\mathrm{map}\;\mathrm{from}\;S=[{s}_1$ , ${s}_2,\dots ]\;\mathrm{into}\;P=\{{p}_1$ , ${p}_2,\dots \}\}$ .
This lemma provides us with an alternative clause for the evaluation of the conditional $S\to P$ , which is somewhat analogous to the treatment of the conditional as a functional type. However, instead of using the function $\boldsymbol{p}$ itself as the ‘verifier’ of the conditional, we use its collapsed form $\boldsymbol{p}{\Downarrow}$ . This is in line with the semantics for the conditional of intuitionistic logic adopted in [Reference Fine4]. However, instead of pushing the verifiers of conditionals all the way down to the level of states, we now only push them down to the level of first-order functions (taking states into actions).
In the standard treatment of formulas as ‘types’, the formula $\mathrm{S}\to (\mathrm{T}\to \mathrm{U})$ will denote functions that take elements of $S$ into functions taking elements of $T$ into elements of $U$ , while the formula $(\mathrm{S}\wedge \mathrm{T})\to \mathrm{U}$ will denote functions that take ordered pairs of elements from $S$ and $T$ into elements of $U$ . Under our approach, by contrast, $(\mathrm{S}\wedge \mathrm{T})$ will denote fusions of elements of $\mathrm{S}$ and $\mathrm{T}$ and $\mathrm{S}\to (\mathrm{T}\to \mathrm{P})$ is so defined that it no longer denotes higher-order functions but certain first-order functions—indeed, the very same functions as those denoted by $(\mathrm{S}\wedge \mathrm{T})\to \mathrm{P}$ . Thus it is through this reinterpretation of formulas as types that we are able to retain the treatment of the conditional as a functional type while still being able to preserve some significant logical identities between different complex types.
13 Positive reduction
We present the reduction theses that will later be used in establishing the extended normal form theorem. We state these at the level of syntax, although each will have an abstract counterpart at the level of content. In stating the theses, we shall assume given a positive prescriptive model $\boldsymbol{M}$ conforming to Regularity in which $| \mathrm{S}| =[s_1,s_2,\dots ]$ and $| \mathrm{P}|$ is $\{{p}_1,{p}_2,\dots \}$ (and similarly for variants of $\mathrm{S}$ and $\mathrm{P}$ ). Thus it will be automatic that $\mathrm{S}\approx (\mathrm{s}_1\vee \mathrm{s}_2\vee \cdots )$ and that $\mathrm{P}\approx ({\mathrm{p}}_1\vee {\mathrm{p}}_2\vee \cdots )$ in $\boldsymbol{M}$ .
Left Vacuity:
-
(i) $(\top \to \mathrm{P})\approx \mathrm{P}$ .
-
(ii) $(\perp \to \mathrm{P})\approx \top !$
Proof.
-
(i) $(\top \to \mathrm{P})\approx \top \to ({\mathrm{p}}_1\vee {\mathrm{p}}_2\vee \cdots )$ Stipulation
$\approx (\top \to {\mathrm{p}}_1)\vee (\top \to {\mathrm{p}}_2)\vee \cdots$ Basic Reduction
$\approx {\mathrm{p}}_1\vee {\mathrm{p}}_2\vee \cdots$ Basic Reduction
$\approx \mathrm{P}$ .
-
(ii) $(\perp \to \mathrm{P})\approx (\bigvee \varnothing \to \mathrm{P})$
$\approx \bigwedge \varnothing$
$\approx \top !$ .
Right Vacuity:
-
(i) $\mathrm{S}\to \top !\ \approx \top !$ .
-
(ii) $\mathrm{S}\to \perp !\ \approx\ \perp !$ for $| \mathrm{S}| \ne []$ .
Proof.
-
(i) $\mathrm{S}\to \top !\approx (({\mathrm{s}}_1\vee {\mathrm{s}}_2\vee \cdots )\to \top !)$
$\approx ({\mathrm{s}}_1\to \top !)\wedge ({\mathrm{s}}_2\to \top !)\wedge \cdots$ Basic Reduction
$\approx \top !\wedge \top !\wedge \cdots$ Basic Reduction
$\approx \top !$ .
-
(ii) Let us first note that
$| \mathrm{s}\to \perp !| =| \mathrm{s}| \to | \perp !|$
$=[s]\to \varnothing$
$=\bigsqcup\ [s\to \varnothing ]$
$=\bigsqcup\ [\{s\to p:p\in \varnothing \}]$
$=\bigsqcup\ [\varnothing ]$
$=\varnothing$ .
In the general case,
$\mathrm{S}\to \perp !\ \approx ({\mathrm{s}}_1\vee {\mathrm{s}}_2\vee \cdots )\to \perp !$
$\approx ({\mathrm{s}}_1\to \perp !)\wedge ({\mathrm{s}}_2\to \perp !)\wedge \cdots$
$\approx\ \perp !\wedge \perp !\wedge \cdots$ by the special case above
$\approx\ \perp !$ since, given that $| \mathrm{S}| \ne []$ , the conjunction is non-empty.
We should note that (ii) will not hold when $| \mathrm{S}| =[]$ . In that case, (ii) of Left Vacuity takes precedence and has the consequence that $(\perp \to \perp !)\approx \top !$ .
Disjunctive Simplification on the Left:
Proof. $(({\mathrm{S}}_1\vee {\mathrm{S}}_2\vee \cdots )\to \mathrm{P})\approx (({\mathrm{s}}_{11}\vee {\mathrm{s}}_{12}\vee \cdots )\vee ({\mathrm{s}}_{21}\vee {\mathrm{s}}_{22}\vee \cdots )\vee \cdots )\to \mathrm{P}$
$\approx ({\mathrm{s}}_{11}\vee {\mathrm{s}}_{12}\vee \cdots \vee {\mathrm{s}}_{21}\vee {\mathrm{s}}_{22}\vee \cdots \vee \cdots )\to \mathrm{P}$
$\approx ({\mathrm{s}}_{11}\to \mathrm{P})\wedge ({\mathrm{s}}_{12}\to \mathrm{P})\wedge \cdots \wedge ({\mathrm{s}}_{21}\to \mathrm{P})\wedge$ $({\mathrm{s}}_{22}\to \mathrm{P})\wedge \cdots \wedge \cdots$ Basic Reduction
$\approx (({\mathrm{s}}_{11}\to \mathrm{P})\wedge ({\mathrm{s}}_{12}\to \mathrm{P})\wedge \cdots )\wedge (({\mathrm{s}}_{21}\to \mathrm{P})\wedge$ $({\mathrm{s}}_{22}\to \mathrm{P})\wedge \cdots )\wedge \cdots$
$\approx (({\mathrm{s}}_{11}\vee {\mathrm{s}}_{12}\vee \cdots )\to \mathrm{P})\wedge (({\mathrm{s}}_{21}\vee {\mathrm{s}}_{22}\vee \cdots )$ $\to \mathrm{P})\wedge \cdots$ Basic Reduction
It is important to note that this result will not hold without adopting the multi-set semantics for disjunction. For under the regular set semantics, $(\top \vee \top )\to \mathrm{P}$ , for example, is equivalent to $\top \to \mathrm{P}$ and hence to $\mathrm{P}$ , but it is also equivalent by Disjunctive Simplification to $(\top \to \mathrm{P})\wedge (\top \to \mathrm{P})$ and hence to $\mathrm{P}\wedge \mathrm{P}$ , which is not in general equivalent to $\mathrm{P}$ . It is for precisely this reason that we have felt compelled to adopt the multi-set semantics for the indicative antecedents of conditional imperatives.
Disjunctive Simplification on the Right:
Proof. $\mathrm{s}\to ({\mathrm{P}}_1\vee {\mathrm{P}}_2\vee \cdots )\approx (\mathrm{s}\to (({\mathrm{p}}_{11}\vee {\mathrm{p}}_{12}\vee \cdots )\vee ({\mathrm{p}}_{21}\vee {\mathrm{p}}_{22}\vee \cdots )\vee \cdots )$
$\approx (\mathrm{s}\to ({\mathrm{p}}_{11}\vee {\mathrm{p}}_{12}\vee \cdots \vee {\mathrm{p}}_{21}\vee {\mathrm{p}}_{22}\vee \cdots \vee \cdots ))$
$\approx (\mathrm{s}\to {\mathrm{p}}_{11})\vee (\mathrm{s}\to {\mathrm{p}}_{12})\vee \cdots \vee (\mathrm{s}\to {\mathrm{p}}_{21})\vee (\mathrm{s}\to {\mathrm{p}}_{22})$
$\vee \cdots \vee \cdots$ Basic Reduction
$\approx ((\mathrm{s}\to {\mathrm{p}}_{11})\vee (\mathrm{s}\to {\mathrm{p}}_{12})\vee \cdots )\vee ((\mathrm{s}\to {\mathrm{p}}_{21})\vee$ $ (\mathrm{s}\to {\mathrm{p}}_{22})\cdots )\vee \cdots$
$\approx (\mathrm{s}\to ({\mathrm{p}}_{11}\vee {\mathrm{p}}_{12}\vee \cdots ))\vee (\mathrm{s}\to ({\mathrm{p}}_{21}\vee {\mathrm{p}}_{22}\vee \cdots ))\vee \cdots$
Basic Reduction
$\approx (\mathrm{s}\to {\mathrm{P}}_1)\vee (\mathrm{s}\to {\mathrm{P}}_2)\vee \cdots$ .
This result will not hold for arbitrary antecedents. Suppose $S=[{s}_1,{s}_2]$ , $P_1=\{{p}_1\}$ , and $P_2=\{{p}_2\}$ . Then:
whereas if we first apply Disjunctive Simplification on the Right to obtain $(({\mathrm{s}}_1\vee s2)\to p1)\vee (({\mathrm{s}}_1\vee {\mathrm{s}}_2)\to {\mathrm{p}}_2)$ , we then get
which limits the choice to doing ${p}_1$ regardless or ${p}_2$ regardless. However, under Mix-and-Match semantics, the result will hold for arbitrary antecedents. It is for this reason that the order in which we reduce $\mathrm{S}\to \mathrm{P}$ to $\mathrm{s}\to \mathrm{p}$ is important—with Simplification on the Left applied first, followed by Simplification on the Right.
Conjunctive Simplification on the Right:
Proof. We first establish the result for the case in which $S$ is the definite formula $s$ and for simplicity, though without any essential loss of generality, we consider the case in which there are two conjuncts $\mathrm{P}$ and $\mathrm{Q}$ on the right.
$\mathrm{s}\to (\mathrm{P}\wedge \mathrm{Q})\approx (\mathrm{s}\to ({\bigvee}_k{\mathrm{p}}_k\wedge {\bigvee}_l{\mathrm{q}}_l))$
$\approx (\mathrm{s}\to {\bigvee}_{k,l}({\mathrm{p}}_k\wedge {\mathrm{q}}_l)$ ) Distribution
$\approx {\bigvee}_{k,l}(\mathrm{s}\to (({\mathrm{p}}_k\wedge {\mathrm{q}}_l))$ ) Basic Reduction
$\approx {\bigvee}_{k,l}((\mathrm{s}\to {\mathrm{p}}_k)\wedge (\mathrm{s}\to {\mathrm{q}}_l))$ Basic Reduction
$\kern0.6em \approx ({\bigvee}_k(\mathrm{s}\to {\mathrm{p}}_k)\wedge {\bigvee}_l(\mathrm{s}\to {\mathrm{p}}_l))$ Distribution
$\approx (\mathrm{s}\to {\bigvee}_k{\mathrm{p}}_k)\wedge (\mathrm{s}\to {\bigvee}_l{\mathrm{q}}_l))$ Basic Reduction
$\approx (\mathrm{s}\to \mathrm{P})\wedge (\mathrm{s}\to \mathrm{Q})$ .
We turn to the general case:
$\mathrm{S}\to ({\mathrm{P}}_1\wedge {\mathrm{P}}_2\wedge \cdots )\approx ({\bigvee}_k{\mathrm{s}}_k\to ({\mathrm{P}}_1\wedge {\mathrm{P}}_2\wedge \cdots ))$
$\approx {\bigwedge}_k({\mathrm{s}}_k\to ({\mathrm{P}}_1\wedge {\mathrm{P}}_2\wedge \cdots ))$ Disj. Simplification on the
Left
$\approx {\bigwedge}_k(({\mathrm{s}}_k\to {\mathrm{P}}_1)\wedge ({\mathrm{s}}_k\to {\mathrm{P}}_2)\wedge \cdots ))$ Previous Case
$\approx$ ${\bigwedge}_k({\mathrm{s}}_k\to {\mathrm{P}}_1)\wedge {\bigwedge}_k({\mathrm{s}}_k\to {\mathrm{P}}_2)\wedge \cdots$
$\approx$ $({\bigvee}_k{\mathrm{s}}_k\to {\mathrm{P}}_1)\wedge ({\bigvee}_k{\mathrm{s}}_k\to {\mathrm{P}}_1)\wedge \cdots$ Disj. Simplification on the
Left
$\approx (\mathrm{S}\to {\mathrm{P}}_1)\wedge (\mathrm{S}\to {\mathrm{P}}_2)\wedge \cdots$ .
Conditional Import-Export:
Proof. We first establish the result for the case in which $\mathrm{S}$ and $\mathrm{T}$ are the definite formulas $\mathrm{s}$ and $\mathrm{t}$ :
$\mathrm{s}\to (\mathrm{t}\to P)\approx (\mathrm{s}\to (\mathrm{t}\to {\bigvee}_m{\mathrm{p}}_m)$
$\approx (\mathrm{s}\to {\bigvee}_m(\mathrm{t}\to {\mathrm{p}}_m))$ Basic Reduction
$\approx {\bigvee}_m(\mathrm{s}\to (\mathrm{t}\to {\mathrm{p}}_m))$ Basic Reduction
$\approx {\bigvee}_m(\mathrm{s}\wedge \mathrm{t}\to {\mathrm{p}}_m)$ Basic Reduction
$\approx (\mathrm{s}\wedge \mathrm{t}\to {\bigvee}_m{\mathrm{p}}_m)$ Basic Reduction
$\approx (\mathrm{s}\wedge \mathrm{t}\to P)$ .
We turn to the general case:
$\mathrm{S}\to (\mathrm{T}\to \mathrm{P})\approx {\bigvee}_k{\mathrm{s}}_k\to ({\bigvee}_l{\mathrm{t}}_l\to \mathrm{P})$
$\approx {\bigvee}_k{\mathrm{s}}_k\to {\bigwedge}_l({\mathrm{t}}_l\to \mathrm{P})$ Disjunctive Simplification on the Left
$\approx$ ${\bigwedge}_k({\mathrm{s}}_k\to {\bigwedge}_l({\mathrm{t}}_l\to \mathrm{P}))$ Disjunctive Simplification on the Left
$\approx {\bigwedge}_{k,l}({\mathrm{s}}_k\to ({\mathrm{t}}_l\to \mathrm{P}))$ Basic Reduction
$\approx {\bigwedge}_{k,l}({\mathrm{s}}_k\wedge {\mathrm{t}}_l\to \mathrm{P}))$ Previous Case
$\approx ({\bigvee}_{k,l}({\mathrm{s}}_k\wedge {\mathrm{t}}_l)\to \mathrm{P})\kern1.32em$ Disjunctive Simplification on the Left
$\approx (({\bigvee}_k{\mathrm{s}}_k\wedge {\bigvee}_l{\mathrm{t}}_l)\to \mathrm{P})$ Distribution
$\kern0.6em \approx (\mathrm{S}\wedge \mathrm{T})\to \mathrm{P}$ .
14 Negative reduction
We have not, up to now, stated a clause for when a plan is in contravention to a conditional imperative. To this end, we stipulate
A plan is in contravention to the conditional $S\to P$ if it is of the form $s\to p^{\prime }$ with $s$ a truth-maker for the antecedent $\mathrm{S}$ and $p^{\prime }$ in contravention to the consequent $\mathrm{P}$ .
The clause may be motivated as follows. Suppose that $\mathrm{S}\approx {\mathrm{s}}_1\vee {\mathrm{s}}_2\vee \cdots$ . Then $(\mathrm{S}\to \mathrm{P})\approx ({\mathrm{s}}_1\to \mathrm{P})\wedge ({\mathrm{s}}_2\to \mathrm{P})\wedge \cdots$ , and so a plan in contravention to $\mathrm{S}\to \mathrm{P}$ will be a plan in contravention to one of $({\mathrm{s}}_1\to \mathrm{P}),({\mathrm{s}}_2\to \mathrm{P}),\dots$ . Now suppose that $\mathrm{P}\approx {\mathrm{p}}_1\vee {\mathrm{p}}_2\vee \cdots$ . Then $({\mathrm{s}}_k\to \mathrm{P})\approx ({\mathrm{s}}_k\to ({\mathrm{p}}_1\vee {\mathrm{p}}_2\vee \cdots ))\approx ({\mathrm{s}}_k\to {\mathrm{p}}_1)\vee ({\mathrm{s}}_k\to {\mathrm{p}}_2)\vee \cdots$ , and so a plan in contravention to $({\mathrm{s}}_k\to \mathrm{P})$ will be a plan ${q}_k$ that is the fusion ${q}_{k1}\sqcup {q}_{k2}\sqcup \cdots$ of plans ${q}_{k1},{q}_{k2},\dots$ , respectively, in contravention to ( ${\mathrm{s}}_k\to$ ${\mathrm{p}}_1$ ), ( ${\mathrm{s}}_k\to$ ${\mathrm{p}}_2$ ), …. We now make the assumption that a plan $q$ will be in contravention to $\mathrm{s}\to \mathrm{p}$ if it is of the form $s\to p^{\prime }$ for some plan $p^{\prime }$ in contravention to $p$ . Thus each plan ${q}_{km}$ will be of the form ${\mathrm{s}}_k\to p^{\prime}_{\mathrm{m}}$ , where $p^{\prime}_{\mathrm{m}}$ is a plan in contravention to ${p}_m$ , and so ${q}_k=({\mathrm{s}}_k\to p^{\prime}_{\mathrm{1}})\sqcup ({\mathrm{s}}_k\to p^{\prime}_{\mathrm{2}})\sqcup \cdots ={\mathrm{s}}_k\to (p^{\prime}_{\mathrm{1}}\sqcup p^{\prime}_{\mathrm{2}}\sqcup \cdots)$ . But the plans $p^{\prime }$ in contravention to $\mathrm{P}\approx ({\mathrm{p}}_1\vee {\mathrm{p}}_2\vee \cdots)$ will be those of the form $(p^{\prime}_{\mathrm{1}}\sqcup p^{\prime}_{\mathrm{2}}\sqcup \cdots )$ for $p^{\prime}_{\mathrm{1}},p^{\prime}_{\mathrm{2}},\dots$ plans, respectively, in contravention to ${\mathrm{p}}_1,{\mathrm{p}}_2,\dots$ , and so a plan in contravention to $\mathrm{S}\to \mathrm{P}$ will be of the form ${\mathrm{s}}_k\to p^{\prime }$ , as required.
Given these new clauses, the semantics can be extended to the full language, with the unrestricted application of negation and the formation of disjunctions and conjunctions of arbitrary length. A prescriptive model $\boldsymbol{M}$ over $\boldsymbol{S}$ is now an ordered sextuple $({S}_{\mathrm{I}},{S}_{\mathrm{A}},{S}_{\mathrm{P}},\sqsubseteq, {| \cdot |}_{\mathrm{I}},{| \cdot |}_{\mathrm{P}})$ , where ${| \cdot |}_{\mathrm{I}}$ is a definite bi-lateral multi-set valuation over ${S}_{\mathrm{I}}$ for the indicative atoms and ${| \cdot |}_{\mathrm{P}}$ is a bi-lateral set-theoretic valuation over ${S}_{\mathrm{P}}$ for the imperative atoms. We may then use the standard clauses for negation, disjunction, and conjunction and the previous positive and negative clauses for the conditional imperative to assign a positive and negative content to each imperative formula of the language. Within this semantics, exact equivalence and the like are defined in the usual way.
We have the following reduction thesis for negative imperatives:
Negative Import:
Proof. ${|\neg (s\to \mathrm{P})|}^{+}={|(s\to \mathrm{P})|}^{-}$
$=\{s\to p^{\prime }{:}\ p^{\prime}\in {|\mathrm{P}|}^{-}\}$
$=\{s\to p^{\prime }{:}\ p^{\prime}\in {|\neg \mathrm{P}|}^{+}\}$
$={|(s\to \neg \mathrm{P})|}^{+}$ .□
This result (which is sometimes associated with connexive logic) does not hold generally for disjunctive antecedents. Thus we do not want to say $\neg (({\mathrm{S}}_1\vee {\mathrm{S}}_2)\to \mathrm{P})$ $\approx$ $(({\mathrm{S}}_1\vee {\mathrm{S}}_2)\to \neg \mathrm{P})$ . For the left-hand side would then be equivalent to $\neg (({\mathrm{S}}_1\to \mathrm{P})\wedge ({\mathrm{S}}_2\to \mathrm{P}))$ , hence to $\neg ({\mathrm{S}}_1\to \mathrm{P})\vee \neg ({\mathrm{S}}_2\to \mathrm{P})$ , and hence to $({\mathrm{S}}_1\to \neg \mathrm{P})\vee ({\mathrm{S}}_2\to \neg \mathrm{P})$ , while the right-hand side is equivalent to $({\mathrm{S}}_1\to \neg \mathrm{P})\wedge ({\mathrm{S}}_2\to \neg \mathrm{P})$ .
A possible problem can arise even when the antecedent is not disjunctive. For given Semi-Inclusion, the null plan □ will be in compliance with both $(\mathrm{a}\wedge \neg \mathrm{a})\to \mathrm{a}$ and $(\mathrm{a}\wedge \neg \mathrm{a})\to \neg \mathrm{a}$ and yet, by the above rule, $\neg ((\mathrm{a}\wedge \neg \mathrm{a})\to \mathrm{a})\approx (\mathrm{a}\wedge \neg \mathrm{a})\to \neg \mathrm{a}$ , and so the null plan will be both in compliance with and in contravention to $(\mathrm{a}\wedge \neg \mathrm{a})\to \mathrm{a}$ . You are, as a matter of logic, damned if you do and damned if you don’t. I will discuss in part IV how this problem might be circumvented.
We have so far established results on positive equivalence (i.e., on identity of positive content). But positive equivalence only allows us to substitute in positive contexts (preserving positive equivalence) even though, for the purposes of the normal form theorem, we will sometimes need to substitute in negative contexts as well. It will therefore be helpful to see when our previous results on positive equivalence can be extended to full equivalence.
In regard to the core system CS, all of the axioms and rules E1–E15 hold for full equivalence with the exception of E8 (Distribution). The additional axiom E16 $((\mathrm{X}\vee \mathrm{X})\approx \mathrm{X})$ will not hold for full equivalence even under the set-theoretic semantics (since, in general, we do not have $(\neg \mathrm{X}\wedge \neg \mathrm{X})\approx \neg \mathrm{X})$ , while the additional axiom E17 $(\mathrm{x}\wedge \mathrm{x}\approx \mathrm{x})$ will hold for full equivalence under the definite set-semantics although not under the definite multi-set semantics (since, in general, we do not have $(\neg \mathrm{x}\vee \neg \mathrm{x})\approx \neg \mathrm{x})$ .
We turn to the principles of full equivalence governing the conditional:
Lemma 37.
-
(i) $(\top \to \mathrm{P})\ {\approx}_{\pm}\mathrm{P}$ .
-
(ii) $({\mathrm{S}}_1\vee {\mathrm{S}}_2\vee \cdots )\to P\approx_{\pm}({\mathrm{S}}_1\to \mathrm{P})\wedge ({\mathrm{S}}_2\to \mathrm{P})\wedge \cdots$ .
-
(iii) $\mathrm{s}\to ({\mathrm{P}}_1\vee {\mathrm{P}}_2\vee \cdots )\approx_{\pm}(\mathrm{s}\to {\mathrm{P}}_1)\vee (\mathrm{s}\to {\mathrm{P}}_2)\vee \cdots$ .
-
(iv) $\mathrm{S}\to ({\mathrm{P}}_1\wedge {\mathrm{P}}_2\wedge \cdots )\approx_{\pm}(\mathrm{S}\to {\mathrm{P}}_1)\wedge (\mathrm{S}\to {\mathrm{P}}_2)\wedge \cdots$ .
-
(v) $\mathrm{S}\to (\mathrm{T}\to \mathrm{P})\approx_{\pm}(\mathrm{S}\wedge \mathrm{T})\to \mathrm{P}$ .
-
(vi) $\neg (\mathrm{s}\to \mathrm{P})\;\approx_{\pm}(\mathrm{s}\to \neg \mathrm{P})$ .
-
(vii) $(\perp \to \mathrm{P})\approx_{\pm}\top !$ .
-
(viii) $\mathrm{S}\to \top !\approx_{\pm}\top !$ .
-
(ix) $\mathrm{S}\to \perp !\approx_{\pm}\perp !\ \mathrm{for}\ | \mathrm{S}| \ne []$ .
-
(x) $\mathrm{S}\approx_{+}\mathrm{T}\Rightarrow (\mathrm{S}\to \mathrm{P})\approx_{\pm}(\mathrm{T}\to \mathrm{P})$ .
Proof. Since we have previously established the positive equivalences for the cases (i)–(vii), we need only establish the corresponding negative equivalences in these cases (or, equivalently, the corresponding positive equivalences for the negations).
-
(i) $\neg (\top \to \mathrm{P})\approx \top \to \neg \mathrm{P}$ Negative Import
$\approx \neg \mathrm{P}$ Left Vacuity.
-
(ii) $q\ \text{-}\!||\ ({\mathrm{S}}_1\vee {\mathrm{S}}_2\vee \cdots )\to P\;\mathrm{iff}\;q=s\to p^{\prime}\ \mathrm{for}\kern0.17em \mathrm{some}\;s\in {|\;{\mathrm{S}}_1|}^{+}\cup {|\;{\mathrm{S}}_2|}^{+}\cup \cdots \mathrm{and} \mathrm{for}\kern0.17em \mathrm{some}\;p^{\prime}\in {|\mathrm{P}|}^{-}$
iff $q=s\to p^{\prime }$ for some $k$ , some $s\in {|{\mathrm{S}}_k|}^{+}$ and some $p^{\prime}\in {|P|}^{-}$
iff $q\ \text{-}\!||\ ({\mathrm{S}}_k\to \mathrm{P})\;\mathrm{for}\kern0.17em \mathrm{some}\;k$
iff $q\ \text{-}\!||\ ({S}_1\to \mathrm{P})\wedge ({S}_2\to \mathrm{P})\wedge \cdots$ .
-
(iii) $\neg (\mathrm{s}\to ({\mathrm{P}}_1\vee {\mathrm{P}}_2\vee \cdots ))\approx (s\to \neg ({\mathrm{P}}_1\vee {\mathrm{P}}_2\vee \cdots ))$ Negative Import
$\approx (\mathrm{s}\to \neg {\mathrm{P}}_1\wedge \neg {\mathrm{P}}_2\wedge \cdots )$
$\approx (\mathrm{s}\to \neg {\mathrm{P}}_1)\wedge (\mathrm{s}\to \neg {\mathrm{P}}_2)\wedge \cdots$ Conj. Simpl. on the Right
$\approx \neg (\mathrm{s}\to {\mathrm{P}}_1)\wedge \neg (\mathrm{s}\to {\mathrm{P}}_2)\wedge \cdots$ Negative Import
$\approx \neg ((\mathrm{s}\to {\mathrm{P}}_1)\vee (\mathrm{s}\to {\mathrm{P}}_2)\vee \cdots )$ .
-
(iv) We first consider the case in which $\mathrm{S}=\mathrm{s}$ . We then have
$\neg (\mathrm{s}\to ({\mathrm{P}}_2\wedge {\mathrm{P}}_2\wedge \cdots ))\approx \mathrm{s}\to \neg ({\mathrm{P}}_1\wedge {\mathrm{P}}_2\wedge \cdots )$ Negative Import
$\approx \mathrm{s}\to (\neg {\mathrm{P}}_1\vee \neg {\mathrm{P}}_2\vee \cdots )$
$\approx (\mathrm{s}\to \neg {\mathrm{P}}_1)\vee (\mathrm{s}\to \neg {\mathrm{P}}_2)\vee \cdots$ Disj. Simplification
on the Right
$\approx \neg (\mathrm{s}\to {\mathrm{P}}_1)\vee \neg (\mathrm{s}\to {\mathrm{P}}_2)\vee \cdots$ Negative Import
$\approx \neg ((\mathrm{s}\to {\mathrm{P}}_1)\wedge (\mathrm{s}\to {\mathrm{P}}_2)\wedge \cdots )$ .
We now consider the general case:
$\neg (\mathrm{S}\to ({\mathrm{P}}_1\wedge {\mathrm{P}}_2\wedge \cdots ))\approx \neg (({\mathrm{s}}_1\vee {\mathrm{s}}_2\vee \cdots )\to ({\mathrm{P}}_1\wedge {\mathrm{P}}_2\wedge \cdots ))$
$\approx \neg (({\mathrm{s}}_1\to ({\mathrm{P}}_1\wedge {\mathrm{P}}_2\wedge \cdots ))\wedge ({\mathrm{s}}_2\to ({\mathrm{P}}_1\wedge {\mathrm{P}}_2\wedge \cdots ))\wedge \cdots )$
$\approx \neg ({\mathrm{s}}_1\to ({\mathrm{P}}_1\wedge {\mathrm{P}}_2\wedge \cdots ))\vee \neg ({\mathrm{s}}_2\to ({\mathrm{P}}_1\wedge {\mathrm{P}}_2\wedge \cdots ))\vee \cdots )$
$\approx ({\mathrm{s}}_1\to \neg ({\mathrm{P}}_1\wedge {P}_2\wedge \cdots ))\vee \neg (\mathrm{s}_2\to \neg (\mathrm{P}_1\wedge \mathrm{P}_2\wedge \cdots ))\vee \cdots )$ Neg. Import
$\approx (({\mathrm{s}}_1\to (\neg {\mathrm{P}}_1\vee \neg {\mathrm{P}}_2\vee \cdots ))\vee ({\mathrm{s}}_2\to (\neg {\mathrm{P}}_1\vee \neg {\mathrm{P}}_2\vee \cdots ))\vee \cdots )$
$\approx ((({\mathrm{s}}_1\to \neg {\mathrm{P}}_1)\vee ({\mathrm{s}}_1\to \neg {\mathrm{P}}_2)\vee \cdots ))\vee (({\mathrm{s}}_2\to \neg {\mathrm{P}}_1) $
$\vee (\mathrm{s}_2\to \neg {P}_2)\vee \cdots ))\vee \cdots$ Disj. Simpl. on the Right
$\approx (\neg ({\mathrm{s}}_1\to {\mathrm{P}}_1)\vee \neg ({\mathrm{s}}_1\to {\mathrm{P}}_2)\vee \cdots \vee \neg ({\mathrm{s}}_2\to {\mathrm{P}}_1)\vee (\neg \mathrm{s}_2\to {\mathrm{P}}_2)\vee \cdots \vee \cdots$
Neg. Import
$\approx (\neg (({s}_1\to {P}_1)\wedge ({s}_2\to {\mathrm{P}}_1)\wedge \cdots )\vee \neg (({\mathrm{s}}_1\to {\mathrm{P}}_2)\wedge ({\mathrm{s}}_2\to {\mathrm{P}}_2)\wedge \cdots ))\vee \cdots$
$\approx \neg (({\mathrm{s}}_1\vee {\mathrm{s}}_2\vee \cdots )\to {\mathrm{P}}_1)\vee \neg (({\mathrm{s}}_1\vee {\mathrm{s}}_2\vee \cdots )\to {\mathrm{P}}_2)\vee \cdots$ by (ii) above
$\approx \neg (\mathrm{S}\to {\mathrm{P}}_1)\vee \neg (\mathrm{S}\to {\mathrm{P}}_2)\vee \cdots$
$\approx \neg ((\mathrm{S}\to {\mathrm{P}}_1)\wedge (\mathrm{S}\to {\mathrm{P}}_2)\wedge \cdots )$ .
-
(v) $q\ \text{-}\!||\ \mathrm{S}\to (\mathrm{T}\to \mathrm{P})$ iff $q=s\to r$ for some $s\ ||\!\text{-}\ \mathrm{S}$ and $r\ \text{-}\!||\ (\mathrm{T}\to \mathrm{P})$
iff $q=s\to (t\to p^{\prime})$ for some $s\ ||\!\text{-}\ \mathrm{S},t\ ||\!\text{-}\ \mathrm{T}\;\mathrm{and}\;p^{\prime}\ \text{-}\!||\ \mathrm{P}$
iff $q=(s\sqcup t\to p^{\prime})$ for some $s\ ||\!\text{-}\ \mathrm{S}$ , $t\ ||\!\text{-}\ \mathrm{T}$ and $p^{\prime}\ \text{-}\!||\ \mathrm{P}$ Lemma 17(ii)
iff $q=(u\to p^{\prime})$ for some $u\ ||\!\text{-}\ \mathrm{S}\wedge \mathrm{T}$ and $p^{\prime}\ \text{-}\!||\ \mathrm{P}$
iff $q\ \text{-}\!||\ (\mathrm{S}\wedge \mathrm{T})\to \mathrm{P}$ .
-
(vi) $\neg \neg (\mathrm{s}\to \mathrm{P})\approx (\mathrm{s}\to \mathrm{P})$
$\approx (\mathrm{s}\to \neg \neg \mathrm{P})$
$\approx \neg (\mathrm{s}\to \neg \mathrm{P})$ Negative Import.
-
(vii) $\ \neg (\perp \to \mathrm{P})\approx \neg (\vee \varnothing \to \mathrm{P})$
$\approx \neg \wedge \varnothing $ by (ii) above
$\approx \neg \top !$ .
-
(viii) First note that $\neg (\mathrm{s}\to \top !)\approx (\mathrm{s}\to \neg \top !)$ by Negative Import. But $(\mathrm{s}\to \neg \top !)=(\mathrm{s}\to \perp !)\approx\ \perp !=\neg \top !$ by Right Vacuity. Thus the result holds when $\mathrm{S}=\mathrm{s}$ .
In the general case, we have:
$\neg (\mathrm{S}\to \top !)\approx \neg (\;({\mathrm{s}}_1\vee {\mathrm{s}}_2\vee \cdots )\to \top !)$
$\approx \neg (\;(\mathrm{s}_1\to \top !)\wedge ({s}_2\to \top !)\wedge \cdots )$ by (ii) above
$\approx \neg (\top !\wedge \top !\wedge \cdots )$ by the special case above
$\approx \neg \top !$ .
-
(ix) First note that $\neg (\mathrm{s}\to \perp !)\approx (\mathrm{s}\to \neg \perp !)$ by Negative Import. But $(\mathrm{s}\to \neg \perp !)=(\mathrm{s}\to \top !)\approx \top !=\neg \perp !$ by Right Vacuity. Thus the result holds when ${S=\mathrm{s}}$ .
In the general case in which $| S| \ne []$ we have:
$\neg (\mathrm{S}\to \perp !)\approx \neg (\;(\mathrm{s}_1\vee \mathrm{s}_2\vee \cdots )\to \perp !)$
$\approx \neg (\;(\mathrm{s}_1\to \perp !)\wedge (\mathrm{s}_2\to \perp !)\wedge \cdots )$ by (ii) above
$\approx \neg (\perp !\wedge \perp !\wedge \cdots )$ by the special case above
$\approx \neg \perp !$ since the conjunction is non-empty.
-
(x) Since ${|\mathrm{S}\to \mathrm{P}|}^{+}$ and |S → P $| {}^{-}$ depend only upon ${|S|}^{+}$ , not upon ${|S|}^{-}$ .
15 Normal forms
We establish the central result of the paper, that each imperative formula is equivalent to one in normal form. This may then be used as a basis for constructing a complete set of axioms and rules for demonstrating the equivalence of imperative formulas.
We first extend the terminology for normal forms from Section 5. An indicative description is a standard conjunctively non-repetitive state description formed from indicative atoms and an imperative description is a standard conjunctively non-repetitive state description formed from imperative atoms (where the null indicative state description is taken to be ⊤ and the null imperative state description is taken to be ⊤!). A component plan description is a formula of the form $\mathrm{S}\to \mathrm{P}$ where $\mathrm{S}$ is a positive (i.e., negation-free) indicative description and $\mathrm{P}$ is an imperative description. A plan description is a conjunction of component plan descriptions, and it is said to be full in the set of indicative atoms Δ if it is of the form $({\mathrm{S}}_1\to {\mathrm{P}}_1)\wedge ({\mathrm{S}}_2\to {\mathrm{P}}_2)\wedge \cdots \wedge ({\mathrm{S}}_n\to {\mathrm{P}}_n),n\ge 0$ , where ${\mathrm{S}}_1$ , ${\mathrm{S}}_2$ , …, ${\mathrm{S}}_n$ are all of the positive indicative descriptions formed from the atoms of Δ (which we may suppose to be given in a pre-determined order). Thus a full plan will tell one what to do in each positive scenario that might be specified by a conjunction of atoms from Δ.
We understand (exact) equivalence by reference to the class of definite models, i.e., those in which each indicative atom is definite. Thus each positive indicative description S will also be definite.
Theorem 38 (Semantical Normal Form)
Let $\mathrm{P}$ be an imperative formula and $\Sigma$ a realization scheme for the indicative atoms of $\mathrm{P}$ . Then $\mathrm{P}$ is $\Sigma$ -equivalent to a disjunction of full plan descriptions in the atoms of $\Sigma$ .
Proof. We obtain the required normal form in a number of steps.
Step 1: By Lemma 37(i), each imperative atom p is fully equivalent to $\top \to p$ and, likewise, ⊤! is fully equivalent to $\top \to \top !$ . So each occurrence of an imperative atom p or of the constant ⊤! in P which does not occur within the scope of $\to$ may be replaced, respectively, with $\top \to \mathrm{p}$ or $\top \to \top !$ , preserving full equivalence, and we may therefore suppose that $\mathrm{P}$ is a truth-functional compound of conditional imperatives.
Step 2: By Corollary 3 (and Soundness), any indicative formula $\mathrm{S}$ is positively $\Sigma$ -equivalent to a positive disjunctive normal form $\mathrm{S}^{\prime}=(\mathrm{S}_1\vee {\mathrm{S}}_2\vee \cdots \vee {\mathrm{S}}_n),n\ge 0$ . By Lemma 37(x), if $\mathrm{S}$ and $\mathrm{S}^{\prime }$ are positively equivalent then $\mathrm{S}\to \mathrm{Q}$ and $\mathrm{S}^{\prime}\to \mathrm{Q}$ are fully equivalent. So each antecedent $\mathrm{S}$ of a conditional subformula $\mathrm{S}\to \mathrm{Q}$ of $\mathrm{P}$ may be replaced with $\mathrm{S}^{\prime}\to \mathrm{Q}$ , preserving full equivalence, and we may therefore suppose that the conditional subformulas of $\mathrm{P}$ are of the form $\mathrm{S}^{\prime}\to \mathrm{Q}$ with $\mathrm{S}^{\prime }$ a positive disjunctive normal form $({\mathrm{S}}_1\vee {\mathrm{S}}_2\vee \cdots \vee {\mathrm{S}}_n),n\ge 0$ .
Step 3: By Lemma 37(ii), each subformula $({\mathrm{S}}_1\vee {\mathrm{S}}_2\vee \cdots \vee {\mathrm{S}}_n)\to \mathrm{Q}$ may be replaced, preserving full equivalence, by $({\mathrm{S}}_1\to \mathrm{Q})\wedge ({\mathrm{S}}_2\to \mathrm{Q})\wedge \cdots \wedge ({\mathrm{S}}_n\to \mathrm{Q})$ . In order to do this in an orderly manner, we might first make the replacement in the innermost subformulas $\mathrm{S}^{\prime}\to \mathrm{Q}$ in which $\mathrm{S}^{\prime }$ is not already an indicative description. Should $\mathrm{S}^{\prime }$ be the null disjunction ⊥ then $\mathrm{S}^{\prime}\to \mathrm{Q}$ will be fully equivalent to ⊤! and thence to $\top \to \top !$ . Thus in each case we may replace $\mathrm{S}^{\prime}\to \mathrm{Q}$ with a conditional whose antecedent is a positive indicative description, and proceeding in this way, we end up with a formula in which the antecedent of every conditional subformula is a positive indicative description.
Step 4: We now drive negations inwards, thereby preserving full equivalence. Thus $\neg \neg \mathrm{P}$ is replaced with $\mathrm{P},\neg (\mathrm{P}\wedge \mathrm{Q})$ with $(\neg \mathrm{P}\vee \neg \mathrm{Q}),\neg (\mathrm{P}\vee \mathrm{Q})$ with $(\neg \mathrm{P}\wedge \neg \mathrm{Q})$ , and $\neg (\mathrm{S}\to \mathrm{Q})$ with $(\mathrm{S}\to \neg \mathrm{Q})$ . The last step is legitimated by Lemma 37(vi), since $\mathrm{S}$ is a positive indicative description, which is definite. Thus we end up with a formula in which the negation operator only governs imperative atoms or the constant ⊤!.
Step 5: Each conditional subformula of the resulting formula $\mathrm{P}$ is therefore of the form $(\mathrm{S}\to \mathrm{Q})$ , where $\mathrm{Q}$ is either a (i) conditional formula or (ii) a conjunction of two imperatives or (iii) the disjunction of two imperatives or (iv) an imperative literal or (v) one of the constants ⊤! or ⊥!. We deal with each case in turn:
-
(i) By Lemma 37(v), we may replace $\mathrm{S}\to (\mathrm{Q}\to \mathrm{R})$ with $(\mathrm{S}\wedge \mathrm{Q})\to \mathrm{R}$ .
-
(ii) By Lemma 37(iv), we may replace $\mathrm{S}\to ({\mathrm{Q}}_1\wedge {\mathrm{Q}}_2)$ with $(\mathrm{S}\to {\mathrm{Q}}_1)\wedge (\mathrm{S}\to {\mathrm{Q}}_2)$ .
-
(iii) By Lemma 37(iii), we may replace $\mathrm{S}\to ({\mathrm{Q}}_1\vee {\mathrm{Q}}_2)$ with $(\mathrm{S}\to {\mathrm{Q}}_1)\vee (\mathrm{S}\to {\mathrm{Q}}_2)$ , bearing in mind that $\mathrm{S}$ is definite.
-
(iv) In this case, leave the formula alone.
-
(v) We leave $\mathrm{S}\to \top !$ alone and, by Lemma 37(ix), we may replace $\mathrm{S}\to \perp !$ with ⊥!.
We perform these replacements, starting with the innermost subformulas of the form $\mathrm{S}\to \mathrm{Q}$ . Proceeding in this way, the procedure will terminate in a positive truth-functional compound of the constant ⊥! and component plan descriptions of the form $\mathrm{S}\to \pm \mathrm{p}$ where $\pm \mathrm{p}$ is an imperative atom or its negation.
Step 6: Put the resulting formula $\mathrm{P}$ in standard disjunctive normal form in which the ‘atoms’ are now taken to be the conditional imperatives $(\mathrm{S}\to \pm \mathrm{p})$ . Thus each ‘state description’ in the normal form will be a conjunction of component plan descriptions (and when the normal form contains no disjuncts it will be identical to ⊥!). If one of the component plan descriptions contains several conjuncts of the form $\mathrm{S}\to \pm {\mathrm{p}}_1$ , $\mathrm{S}\to \pm {\mathrm{p}}_2$ , …, $\mathrm{S}\to \pm {\mathrm{p}}_m$ , in which the antecedent $\mathrm{S}$ is the same, then, by *, we may replace them with $\mathrm{S}\to ({\mathrm{p}}_1\wedge {\mathrm{p}}_2\wedge \cdots \wedge {\mathrm{p}}_m)$ . Also, if one of the component plan description omits any conditionals of the form $\mathrm{S}\to \mathrm{Q}$ whose antecedent is a positive indicative description in the atoms of $\Sigma$ then, by Lemma 37(xiii), we may add $\mathrm{S}\to \top !$ as a conjunct. We thereby obtain a formula of the required form.
The above proof establishes a semantic equivalence between an imperative formula and its normal form. We may also establish a corresponding proof-theoretic equivalence. To this end, we adopt CS + E17 for indicative formulas and CS + E16 + E17 for imperative formulas. To these subsystems, we then add the following axioms and rules governing the conditional (where $\mathrm{P}\equiv \pm \mathrm{Q}$ is used to indicate the pair of equivalences $\mathrm{P}\equiv \mathrm{Q}$ and $\neg \mathrm{P}\equiv \neg \mathrm{Q}$ and ${\mathrm{S}}^{+}$ is used to indicate a positive indicative description, i.e., a conjunction of indicative atoms of arbitrary finite length):
-
ES1 $(\top \to \mathrm{P})\equiv \mathrm{P}$ .
-
ES2 $(\mathrm{S}_1\vee \mathrm{S}_2)\to \mathrm{P}\;{\equiv}_{\pm}\;({\mathrm{S}}_1\to \mathrm{P})\wedge ({\mathrm{S}}_2\to \mathrm{P})$ .
-
ES2′ $(\perp \to \mathrm{P})\ {\equiv}_{\pm}\ \top !$ .
-
ES3 $\mathrm{S}\to ({\mathrm{P}}_1\wedge {\mathrm{P}}_2)\equiv (\mathrm{S}\to {\mathrm{P}}_1)\wedge (\mathrm{S}\to {\mathrm{P}}_2)$ .
-
ES3′ $(\mathrm{S}\to \top !)\equiv \top !$ .
-
ES4 ${\mathrm{S}}^{+}\to$ ( ${\mathrm{P}}_1$ $\vee$ ${\mathrm{P}}_2$ ) $\equiv$ $({\mathrm{S}}^{+}\to {\mathrm{P}}_1)\vee ({\mathrm{S}}^{+}\to {\mathrm{P}}_2)$ .
-
ES4′ ${\mathrm{S}}^{+}\to\ \perp\ \equiv\ \perp !$ .
-
ES5 $\mathrm{S}\to (\mathrm{T}\to \mathrm{P})\equiv (\mathrm{S}\wedge \mathrm{T})\to \mathrm{P}$ .
-
ES6 $\neg ({\mathrm{S}}^{+}\to \mathrm{P})\equiv ({\mathrm{S}}^{+}\to \neg \mathrm{P})$ .
-
ES7 $\mathrm{S}\equiv \mathrm{S}^{\prime }/(\mathrm{S}\to \mathrm{P})\ {\equiv}_{\pm}\ (\mathrm{S}^{\prime}\to \mathrm{P})$ .
-
ES8 $\mathrm{P}\equiv \mathrm{P}^{\prime }/(\mathrm{S}\to \mathrm{P})\equiv (\mathrm{S}\to \mathrm{P}^{\prime})$ .
The idea behind the paired axioms ES2–ES4 to ES2–ES4′ is that the primed axiom represents the vacuous case of the logical operation involved in the unprimed axiom. Thus ES3′ corresponds to the case in which the conjunctive consequent in ES3 is empty.
Although we have only stated the axioms ES1 and ES3–ES6 as positive equivalences, they can also be shown to be derivable as negative equivalences. There is a certain inelegance in regard to the pair ES2 and ES2′ since we seem to need to postulate full equivalence in these cases and not just positive equivalence. We could remove the disparity in the case of ES2 by combining it with ES6 and having in their place the single axiom
And we might remove the disparity in the case of ES2′ by adopting the rule
This rule says, in effect, that there is only one proposition whose sole truthmaker is □, and the rule and the corresponding constraint on models are not unreasonable since if they hold for some given propositions they will hold for all propositions that might be formed from them by means of disjunction and conjunction. Given such a rule, the negative form of ES2′ can then be derived from the positive form.
Let us call the resulting system ${\mathrm{CS}}^{\to }$ . Then in analogy to Theorem 38, we have:
Theorem 39 (Provable Normal Form)
Let $\mathrm{P}$ be an imperative formula and $\Sigma$ a realization scheme for the indicative atoms of $\mathrm{P}$ . Then $\mathrm{P}$ is provably $\Sigma$ -equivalent in ${\mathrm{CS}}^{\to }$ to a disjunction of full plan descriptions in the atoms of $\Sigma$ .
The proof is essentially the same as for the previous theorem, the main difference being that we must now derive the various reduction theses that are required to obtain the normal form.
We can, as before, use the reduction to normal form to establish completeness:
Theorem 40 (Soundness and Completeness for ${\mathbf{CS}}^{\mathbf{\to}}$ )
Let $\mathrm{P}$ and $\mathrm{Q}$ be two imperative formulas and let $\Sigma$ be a realization scheme for the indicative atoms of $\mathrm{P}$ and $\mathrm{Q}$ . Then $\mathrm{P}\equiv \mathrm{Q}$ is derivable in ${\mathrm{CS}}^{\to }$ + $\Sigma$ iff $\mathrm{P}$ and $\mathrm{Q}$ are $\Sigma$ -equivalent in any prescriptive model.
Proof (Sketch)
Soundness is straightforward and largely follows from previously established results.
For the purposes of establishing completeness, we first write $\mathrm{P}$ and $\mathrm{Q}$ in positive standard form, as $\mathrm{P}^{\prime }$ and $\mathrm{Q}^{\prime }$ . We then show that if $\mathrm{P}^{\prime }$ and $\mathrm{Q}^{\prime }$ are not the same then there is a $\Sigma$ - model in which ${|\mathrm{P}^\prime |}^{+}$ and ${|\mathrm{Q}^\prime |}^{+}$ are also not the same. This is done by appeal to a canonical model.
Suppose that ${\mathrm{s}}_1$ , ${\mathrm{s}}_2$ , …, ${\mathrm{s}}_m$ are the indicative atoms occurring in $\mathrm{P}^{\prime }$ or $\mathrm{Q}^{\prime }$ and that ${\mathrm{p}}_1$ , ${\mathrm{p}}_2$ , …, ${\mathrm{p}}_n$ are the imperative atoms occurring in $\mathrm{P}^{\prime }$ or $\mathrm{Q}^{\prime }$ , m, n ≥ 0, and for each indicative atom ${\mathrm{s}}_k$ , k = 1, …, m, suppose that the realization scheme $\Sigma$ contains the formula $\neg {\mathrm{s}}_k\equiv ({\mathrm{s}}_{k1}\vee {\mathrm{s}}_{k2}\vee \cdots \vee {\mathrm{s}}_{k{n}_k})$ . We then let the canonical planning space be ${\boldsymbol{S}\kern-1.2pt}_{I,A,P}^{+}=({S}_{\mathrm{I}},{S}_{\mathrm{A}},S^{+}_{\mathrm{P}},\sqsubseteq )$ , where:
-
(i) S I = ℘({s: s is an indicative atom that occurs in $\mathrm{P}^{\prime }$ or $\mathrm{Q}^{\prime }$ or $\Sigma$ ∪ {±p: p is an imperative atom that occurs in $\mathrm{P}^{\prime }$ or $\mathrm{Q}^{\prime }$ });
-
(ii) ${S}_{\mathrm{A}}=\wp (\{\pm \mathrm{p}:\mathrm{p}$ is an imperative at $\mathrm{into}\ {S\kern-2pt}_{\mathrm{A}}\}$ ;
-
(iii) $S^{+}_{\mathrm{P}}$ = {p: p is a function from S I into S A}; and
-
(iv) $\sqsubseteq\ =\{(s,t)\in {S}_{\mathrm{I}}\times {S}_{\mathrm{I}}:s\subseteq t\}$ .
Note that we have treated the imperative literals ±p as actions rather than plans. The canonical model over ${\boldsymbol{S}\kern-1.2pt}_{I,A,P}^{+}$ is then taken to be the structure $({S}_{\mathrm{I}},{S}_{\mathrm{A}},S^{+}_{\mathrm{P}},\sqsubseteq, {| \cdot |}_{\mathrm{I}},{| \cdot |}_{\mathrm{P}}))$ , where:
-
(v) $| \mathrm{s}| ^{+}_{\mathrm{I}}=[\{\mathrm{s}\}]$ for each indicative atom $\mathrm{s}$ in $\mathrm{P}^{\prime }$ or $\mathrm{Q}^{\prime }$ or $\Sigma$ ,
$| \mathrm{s}_k| ^{-}_{\mathrm{I}}=[\{{\mathrm{s}}_{k1}\},\{{\mathrm{s}}_{k2}\},\dots, \{{s}_{k{n}_k}\}]$ for $k=1,2,\dots, m$ , and
$| \mathrm{s}| ^{-}_{\mathrm{I}}=[\varnothing ]$ for any indicative atom $\mathrm{s}$ of $\Sigma$ that does not occur in $\mathrm{P}^{\prime }$ or $\mathrm{Q}^{\prime }$ ;
-
(vi) $| \mathrm{p}| ^{+}_{\mathrm{P}}=\{{p}_a\in S^{+}_{\mathrm{P}}:a=\{\mathrm{p}\}\}$
$| \mathrm{p}| ^{-}_{\mathrm{P}}=\{{p}_a\in S^{+}_{\mathrm{P}}:a=\{\neg \mathrm{p}\}\}$ .
Note that we have set $| \mathrm{s}| ^{-}_{\mathrm{I}}=[\varnothing ]$ , since for the purposes of evaluating $\mathrm{P}^{\prime }$ or $\mathrm{Q}^{\prime }$ we do not care what $| \mathrm{s}| ^{-}_{\mathrm{I}}$ is for $\mathrm{s}$ neither in $\mathrm{P}^{\prime }$ nor $\mathrm{Q}^{\prime }$ .
If two plan descriptions ${P}^{\#}$ and ${Q}^{\#}$ that occur respectively in $\mathrm{P}^{\prime }$ and $\mathrm{Q}^{\prime }$ are not the same then they will have definite prescriptive contents | ${P}^{\#}$ | $=$ $\{\mathrm{p}\}$ and | ${Q}^{\#}$ | $=\{\mathrm{q}\}$ which are also not the same, and so when P′ and Q′ are not the same, the prescriptive content of one will contain a plan not contained in the prescriptive content of the other.
Imposing the conditions of Semi-Inclusion and Follow-Through makes no difference to the result, since the imposition of these conditions leaves intact the behavior of plans on the ‘pure’ states that do not contain acts as parts. However, the result will fail once coordination between indicative and imperative atoms is allowed. Given Semi-Inclusion, for example, the two imperatives $a\to \top !$ and $\mathrm{a}\to \mathrm{a}!$ would be exactly equivalent.
We should also note the role played by realizations in the above results. We are, in effect, taking the indicative atoms to have a single truth-maker and a finitely number of specifiable falsity makers. Without this assumption, the proposed reduction to normal form would no longer go through and it no longer seems clear whether a reduction to normal form might still be achieved or what a complete set of axioms and rules might reasonably be taken to be.
16 Conclusion
Of primary importance in this paper has been the reduction of truth-functional compounds of conditional imperatives to normal form—one which states the content of the compound formula in terms of a choice between different plans. A secondary aim has been to establish a theory of plans as a basis for a truthmaker semantics in which the plans are the items in exact compliance with or in exact contravention to a given imperative. The reduction calls for a hyperintensional logic in which the import of classically equivalent indicatives needs to be distinguished and, in the absence of such a logic, it is hard to see how the desired reduction is to be achieved.