In previous posts in this series I've been attempting to provide a rough characterization of basic SETL. In Part I, I noted the basics of SETL, in a rough way. In Part II and Part III, I discussed briefly some special cases and how SETL handles them. In Part IV, I discussed some basics of argument using SETL. Part V looked at some simple arguments for which SETL gives us a better sense of what's going on than ordinary predicate logic does. (There will be a post at the end of the series giving references and supplementary readings.)
In this part I want to look a bit at how one might go about incorporating modality into SETL. The work that has been done to this end is still incomplete, but turns out to be immensely promising.
Propositional vs. Predicate Modality
When we have a modality, like necessity, should we take it as modifying the predicate or as modifying the whole proposition? In language we sometimes seem to do one or the other. For instance, we might say,
It is possible that the new animal is a mammal.
And that seems to be propositional modality. However, we might also say,
The new animal is possibly a mammal.
This makes it look like a predicate modification. One could, perhaps, hold that they are equivalent; but this seems very clearly not to be true. A more abstract example might help. Compare:
Necessarily, no B is nonB.
No B is necessarily nonB.
'Necessarily' is clearly doing different work here. In the one, "No B is nonB" is taken as a necessary truth. The second, however, does not imply this. It doesn't rule out the possibility that some B is nonB; the only possibility ruled out is that some B is necessarily nonB. It could be true, for all that we can tell from this sentence alone, that some B is non-necessarily nonB. Very different sorts of modality.
The distinction noted here is often called the de re/de dicto distinction for modality; I'll instead continue to use the terms I've already introduced and call it the distinction between predicate and propositional modality.
Predicate and Propositional Modality in SETL
How would we go about incorporating predicate modality into SETL? It turns out that this is very easy. A proposition with predicate modality is simply a proposition with a modalized predicate. Thus, we can simply add modal functors to our predicates. Then we can simply use our ordinary SETL rules, just adding a few basic modal laws (e.g., if +S+P, we can conclude +S+◊P). Let's put up two axioms:
Axiom 1. If x, then x.
Axiom 2. If x, then x◊.
For instance, +S+P implies +s+◊P; +S+P implies +S+P. With these we can handle all the important logical relations that hold for predicate modality.
Propositional modality is a more complicated affair, and to see how we could handle it, we should perhaps take a moment to look at domains again. Every proposition is put forward relative to a domain of discourse; to contradict each other "There are dragons" and "There are no dragons" have to presuppose the same domain (if the domain of one is fictional beast mentioned in Piers Anthony novels and the domain of the other is real animals, for instance, they simply don't conflict). Any logical relation between two propositions, in fact, requires some connection of domains. We could state this by saying that every statement denotes its domain; and what a statement signifies is what it says of that domain. "Dragons are blue" says of the domain of the sentence that it includes blue dragons. When we say a statement is true, we mean that the domain it denotes includes the feature it signifies.
Putting it this way, however, simplifies matters considerably, because some statements, while having a domain, don't have a determinate domain -- or, if you prefer, their domain is a meta-domain, a domain of domains -- and are therefore harder to pin down. As it happens, all propositionally modalized propositions are of this sort. "Possibly at least one S is P" can't be interpreted as saying that at least one P-characterized S is in a particular domain; rather, it has to be interpreted as saying that there is at least one domain that includes at least one P-characterized S. Likewise, "Necessarily at least one S is P" doesn't mean that there is at least one P-characterized S in a particular domain; it means that in every domain there is at least one P-characterized S.
When we recognize this, it turns out to be fairly easy to see that the contradictory of (Every S is P) is not, as one might think, (Some S is not P), but instead, ◊(Some S is not P); and the contradictory of (No S is P) is ◊(Some S is P); which is actually rather similar to what one finds in predicate modality (the universal + necessity is contradicted by the particular + possibility). If we take SETL and add the following axioms, we can handle all propositionally modal propositions using necessity and possibility:
Axiom 3. If x, then x
Axiom 4. If x, then ◊x
And, it turns out, we can combine our two types of modality if we recognize that the following two statements are true:
If x, then x
If x◊, then ◊x.
This gives us a truly lovely square of opposition or, perhaps more accurately, square of implication, for modal statements, which I borrow from Englebretsen:
Each arrow indicates an implication or possible inference, and gives us an excellent sense of the strongest and weakest modal claims, and, for stronger claims, what weaker claims they entail. Claims that are both necessary and universal are at the top; claims that are both possible and particular are at the bottom; everything else is somewhere in-between.
Inferences with Modality in SETL
With our square of opposition we have already said something about how one would handle simple inferences in a modal version of SETL. But we need a way to handle mediate inference. Since predicate modalities are just modalized predicates, DDO, or the rule of mediate inference, is sufficient to handle them. But propositional modalities are more slippery here as elsewhere. DDO is not sufficient. We need to add another rule:
If x and y, then (x and y)
All this only gives a quick glimpse of a vast and important extension of basic SETL. In any case, any system that cannot distinguish predicate modality from propositional modality is hampered in its handling of real-life modal inferences; and one of the nice things about modalized SETL is that it can handle this distinction very well.
In the next post I'll give another quick glimpse of yet another interesting extension, precise quantification.