Why modal logic needs modalities

Why does modal logic need modalities like provability or others like necessity and possibility? Could they be replaced with equivalent predicates?

-
I don't understand the question. If there weren't any modalities, it wouldn't be modal logic. –  Qiaochu Yuan Aug 24 '12 at 15:34
@QiaochuYuan My question was why do I need modalities? Can't these be replaced by equivalent predicate? –  Trismegistos May 28 at 10:57

Many (most?) modal logics can indeed be translated into non-modal predicate logics, such as by replacing the modalities by quantification over a "time" variable and giving every existing predicate an extra argument, meaning intuitively "at time $t$ it holds that such-and-such".

One reason not to do this is that the quantification over "time" that modalities represent is a particular restricted use of quantification, and knowing that all quantification has that particularly restricted form can be very useful. In other words, the point of modal logics is not to be able to express brand new things that there wasn't any way to express before, but to be able to say about some process or algorithm that it only works for formulas of such-and-such particularly nice form.

For example, many modal propositional logics are decidable -- but it is not at all obvious that the formulas you get by translating them into predicate calculus are decidable. Yet, introducing modalities here clearly adds in expressive power compared to non-modal propositional calculus. It is very useful for (possibly automatic) reasoning about such properties that we can get this increase in expressive power without paying the large price in complexity it would be to handle the full predicate calculus.

-
So is in most cases modality just syntactic sugar to get rid of ominous presence of quantifiers? –  Trismegistos Aug 27 '12 at 14:05
@Trismegistos: No, because syntactic sugar does not have rules of inference and/or logical axioms of its own. Just because a modal logic can be modeled in some more more expressive system doesn't mean that the more expressive system is "more real", or that the modal logic "is just" a restriction of the more expressive system. –  Henning Makholm Aug 27 '12 at 14:13
That would be like learning Euclidean geometry and insisting that you don't want to bother with theorems about circles because "circle" is just syntactic sugar for "ellipse with equal major and minor axis", so can we please formulate everything as being about ellipses instead. –  Henning Makholm Aug 27 '12 at 14:14
That is what I meant by syntactic sugar -- that it does not add any power to a system. So for me notion of circle can be viewed as syntactic sugar for ellipse. Syntactic sugar makes system easier to work with so circle makes particular kind of ellipse more accessible. –  Trismegistos May 28 at 11:03

Modalities modify propositions, predicates modify objects.

-
Not quite this simple, it seems to me. You do have modal predicates, for instance, (so called, de re interpretation of a modal sentence). It is not agreed whether all de re claims can be reduced to de dicto claims without unacceptably distorting the meaning. –  Dennis Apr 8 '13 at 6:04

They can't — while you don't need, e.g., both necessity and possibility (because either is expressible in terms of the other via DeMorgan laws), it can be proven that there are models of modal logic that use these predicates in an essential way (that is, that the expressive power of these predicates is necessary). You might want to look at the two notions of Kripke semantics and Temporal logic.

Provability is another matter - it's not generally taken as a modality in any particular sense that I know. Can you be a bit more specific about what you mean there, possibly with an example?

-
There is a very nice modal logic $G$ where $\Box$ models provability in the proof theory of arithmetic. See Boolos's beautiful book "The unprovability of consistency". –  Rob Arthan Aug 24 '12 at 15:43
@RobArthan Ahhh, yes, thank you for the reminder - I got my intro to modal logic from Smullyan's wonderful 'casual' writing on the topic, so I should really have remembered $G$! –  Steven Stadnicki Aug 24 '12 at 20:10
@StevenStadnicki I have also read Smullyan's "Forever Undecided" it was very interesting but as all of his puzzle books it misses some rigor. Could you propose me some not too hard book that can be read after Smullyan's one? –  Trismegistos Aug 27 '12 at 13:54
According to "Mathematical Modal Logic: A View of its Evolution", by Robert Goldblatt: "Gödel formulated assertions of provability by a propositional connective $B$ (from "beweisbar"), reading $B\alpha$ as '$\alpha$ is provable'." (p.8) –  MJD Sep 2 '12 at 18:36

One common answer is along these lines. Using "$\diamond$" for "it is possible that", we have these or similar semantic or model-theoretic requirements:

• the value assigned to $\diamond p$ must depend only on the value assigned to $p$;
• $p \rightarrow \diamond p$ must be valid;
• $\diamond p \rightarrow p$ must not be valid.

But model-theoreticaly, there are only four (equivalence classes of) functions of $p$ in two-valued logic:

• $p$

• $\neg p$

• $p \vee \neg p$

• $p \wedge \neg p$

None of these four satisfies the above semantic requirements, so if we want a possibility operator it cannot be defined. (This argument-outline raises additional questions, but that's logic.)

-
Sorry but I do not understand. I do not understand where are requirements for "⋄" from. Also I do not understand why do you claim that there are only four functions of p and why those are one you specified. –  Trismegistos Aug 27 '12 at 13:59
The requirements come from what we usually mean by "possible": whatever is true is possible, but not conversely. -- I mentioned equivalence classes. "(p v p)" is not identical with "p" but is logically equivalent to it. Do you have an example in mind that's not equivalent to one of the four? –  MikeC Aug 27 '12 at 17:32
If there are only two values (T, F) so why you listed four equivalence classes? There should be only two. –  Trismegistos Aug 28 '12 at 12:08

A notable example of what you describe (if I understand you correctly) is Lewis's Counterpart Theory (cf. "Counterpart Theory and Quantified Modal Logic")

Counterpart Theory

Counterpart theory seeks to provide an alternate formalization of QML (Quantified Modal Logic). The language of counterpart theory contains four primitive predicates: $Wx$ ($x$ is a possible world), $Ixy$ (an individual $x$ inhabits a possible world $y$), $Ax$ ($x$ is actual) and $Cxy$ ($x$ is a counterpart of $y$). The domain of quantification consists of possible worlds and the individuals that make up everything in those worlds. The following postulates help to constrain the use of these predicates:

P1: $\forall x\forall y\,(Ixy\rightarrow Wy)$ (Nothing is in anything except a world)

P2: $\forall x\forall y\forall z\,(Ixy\wedge Ixz\rightarrow y=z)$ (Nothing is in two worlds)

P3: $\forall x\forall y\,(Cxy\rightarrow\exists z\, Ixz)$ (Whatever is a counterpart is in a world)

P4: $\forall x\forall y\,(Cxy\rightarrow\exists z\, Iyz)$(Whatever has a counterpart is in a world)

P5: $\forall x\forall y\forall z\,(Ixy\wedge Izy\wedge Cxz\rightarrow x=z)$ (Nothing is a counterpart of anything else in its world)

P6: $\forall x\forall y\,(Ixy\rightarrow Cxx)$ (Anything in a world is a counterpart of itself)

P7: $\exists x\,(Wx\wedge\forall y\,(Iyx\leftrightarrow Ay))$ (Some world contains all and only actual things)

P8: $\exists x\, Ax$ (Something is actual)

The Translation Procedure

Where $\phi$ is a closed sentence (i.e. a sentence with no free variables), the possibilist sentence $\exists\beta(W\beta\,\&\,\phi^{\beta})$ ($\phi$ holds in some possible world $\beta$) coincides in truth conditions with the sentence $\Diamond\phi$. The sentence $\phi^{\beta}$ ($\phi$ holds in world $\beta$) coincides in truth-conditions with $\phi$ (of QML) when the quantifiers in $\phi$ are restricted to the inhabitants of $\beta$. This restriction is achieved by replacing every existential quantifier in $\phi$ with $\exists\alpha(I\alpha\beta\,\&\,\cdots)$ and every universal with $\forall\alpha(I\alpha\beta\supset\cdots)$.

Let $\iota\, x\,\forall y\,(Iyx\,\equiv\, Ay)$ denote the actual world, abbreviate this $@$ (Lewis 1968, p. 114). The sentence $\phi^{@}$ (i.e., $\exists\beta(\forall\alpha\,(I\alpha\beta\equiv A\alpha)\,\&\,\phi^{\beta})$) is equivalent to the sentence $\phi$ of QML. We can then go on to fix the truth-conditions of $\phi^{\beta}$ ($\phi$ holds at world $\beta$) for an infinite range of contexts as follows:

$\phi^{\beta}$ iff $\phi$, for atomic $\phi$

$(\sim\phi)^{\beta}$ iff $\sim\phi^{\beta}$

$(\phi\,\&\,\psi)^{\beta}$ iff $\phi^{\beta}\,\&\,\psi^{\beta}$

$(\phi\,\vee\,\psi)^{\beta}$ iff $\phi^{\beta}\,\vee\,\psi^{\beta}$

$(\phi\supset\psi)^{\beta}$ iff $\phi^{\beta}\supset\psi^{\beta}$

$(\phi\equiv\psi)^{\beta}$ iff $\phi^{\beta}\equiv\psi^{\beta}$

$(\forall\alpha\phi)^{\beta}$ iff $\forall\alpha(I\alpha\beta\supset\phi^{\beta})$

$(\exists\alpha\phi)^{\beta}$ iff $\exists\alpha(I\alpha\beta\,\&\,\phi^{\beta})$

$(\Box\phi\alpha_{1}\ldots\alpha_{n})^{\beta}$ iff $\forall\beta_{1}\forall\gamma_{1}\ldots\forall\gamma_{n}(W\beta_{1}\,\&\, I\gamma_{1}\beta_{1}\,\&\, C\gamma_{1}\alpha_{1}\,\&\ldots\,\&\, I\gamma_{n}\beta_{1}\,\&\, C\gamma_{n}\alpha_{n}\supset\phi^{\beta_{1}}\gamma_{1}\ldots\gamma_{n})$

$(\Diamond\phi\alpha_{1}\ldots\alpha_{n})^{\beta}$ iff $\exists\beta_{1}\exists\gamma_{1}\ldots\exists\gamma_{n}(W\beta_{1}\,\&\, I\gamma_{1}\beta_{1}\,\&\, C\gamma_{1}\alpha_{1}\,\&\ldots\,\&\, I\gamma_{n}\beta_{1}\,\&\, C\gamma_{n}\alpha_{n}\,\&\,\phi^{\beta_{1}}\gamma_{1}\ldots\gamma_{n})$

This provides you with a means of ridding yourself of the modal operators by re-interpreting them quantificationally (as quantifiers over worlds and possible individuals). Strictly speaking it isn't equivalent. While everything sentence of QML has a counterpart theoretic equivalent, not every sentence of Counterpart Theory has an equivalent in QML.

What I mean to show here is eliminability of the modal operators. This is one (famous) example of the sort of thing I imagine Henning had in mind in his answer. It is non-modal in the sense that it doesn't have modal operators.

-