@MISC{INTPRO_1.MIZ,
  AUTHOR = {Inou\'e, Takao},
  TITLE = {Intuitionistic Propositional Calculus in the Extended Framework with Modal Operator. {P}art {I}},
  SECTION1 = {Intuitionistic Propositional Calculus IPC in the Extended 
  Language with Modal Operator},
  SECTION2 = {Formulas Provable in IPC: Implication},
  SECTION3 = {Formulas Provable in IPC: Conjunction},
  SECTION4 = {Formulas Provable in IPC: Disjunction},
  SECTION5 = {Classical Propositional Calculus CPC},
  SECTION6 = {Modal Calculus S4},
  DAY = {03},
  MONTH = {April},
  YEAR = {2003},
  ADDRESS1 = {The Iida Technical High School\\Nagano},
  SUMMARY = {In this paper, we develop intuitionistic
   propositional calculus IPC in the extended language
   with single modal operator. The formulation that
   we adopt in this paper is very useful not only
   to formalize the calculus but also to do a number
   of logics with essentially propositional character.
   In addition, it is much simpler than the past
   formalization for modal logic. In the first section,
   we give the mentioned formulation which the author
   heavily owes to the formalism of Adam Grabowski's \cite{HILBERT1.ABS}.
   After the theoretical
   development of the logic, we prove a number of valid
   formulas of IPC in the sections 2--4. The last two
   sections are devoted to present classical propositional calculus
   and modal calculus S4 in our framework, as a preparation
   for future study. In the forthcoming Part II of this paper,
   we shall prove, among others, a number of intuitionistically
   valid formulas with negation.}}

