We study the logic of proofs and some extensions in this thesis. The logic of proof are initiated by Sergei Artemov in 1994. One of the motivations of logic of proofs was to present an arithmetical provability semantics for S4 and to formalize the classical BHK semantics for IPC. LP is an extension of classical prepositional logic with additional atoms t : F representing the proof predicate “ t is a proof of F ”. We introduce the system LP and prove the arithmetical completeness. Also we show that LP is sufficient to realize S4. Then we introduce the logic if proofs and provability (LPP), that incorporates both the modality £ for provability and the proof operator t : F . this system is proved to be arithmetically complete, and it is provided with the appropriate kripke style semantics. In conclusion we state the logic of proofs for HA (i.e. BILP). Admissible rules in HA, that are admissible rules in IPC, have an important role in aximatizing BILP.