The polymodal logic of provability