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?
 A: 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.
A: 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.
A: Modalities modify propositions, predicates modify objects.  
A: 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?
A: 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.)
