In the line of a syntactic treatment of modalities, many proposals have been presented consisting in an extension of a logic calculus with ameta-language for expressing facts about terms and sentences, and with an axiomatization of provability. These proposals differ in the use of the inference rules used to link the object level and meta-level theories; the formulation of these reflection rules is crucial since it affects the consistency of the extended calculus. We argue that reflection rules resulting in a conservative extension are too weak. On the other hand, well known results show that nonconservative extensions often run into paradoxes. We propose a non conservative extension where useful theorems can be proved while consistency is retained.