@ARTICLE{INTPRO_2.MIZ,
  AUTHOR = {Inou\'e, Takao and Hanaoka, Riku},
  TITLE = {Intuitionistic Propositional Calculus in the Extended Framework with 
  Modal Operator, {P}art {II} (Negation, Deduction Theorem for IPC)},
  MSC2010 = {03B20,03F03},
  SECTION1 = {The notion of proof in intuitionistic setting},
  SECTION2 = {A consequence as a set of all intuitionistic provable formulas},
  SECTION3 = {The intuitionistic provable relation},
  SECTION4 = {The first deduction theorem for IPC},
  SECTION5 = {A family of deduction theorems for IPC},
  SECTION6 = {Intuitionistic provable formulas and theorems},
  DAY = {30},
  MONTH = {April},
  YEAR = {2022},
  ADDRESS1 = {Department of Medical Molecular Informatics\\Meiji Pharmaceutical University\\ 
  Tokyo, Japan\\ \\Graduate School of Science and Engineering\\Hosei University\\Tokyo, Japan\\ \\
  Department of Applied Informatics\\Faculty of Science and Engineering\\Hosei University\\Tokyo, Japan},
  ADDRESS2 = {Keyaki-Sou 403\\Midori-cho 5-17-27\\Koganei-city\\184-0003, Tokyo\\Japan},
  SUMMARY = {This paper is a continuation of Inou\'e \cite{INTPRO_1.ABS}. 
  As already mentioned in the paper, a number of intuitionistic 
  provable formulas are given with a Hilbert-style proof. For that, 
  we make use of a family of intuitionistic deduction theorems, which 
  are also presented in this paper. Our axiom system of intuitionistic 
  propositional logic IPC is based on the propositional subsystem of 
  H_1-IQP in Troelstra and van Dalen \cite[p. 68]{TroelstraDalen:1988}. 
  We also owe Heying \cite{Heyting:1971} and van Dalen \cite{vanDalen:2013}. 
  Our treatment of a set-theoretic intuitionistic deduction theorem is 
  due to Agata Darmochwa\l's Mizar article "Calculus of Quantifiers. 
  Deduction Theorem" \cite{CQC_THE2.ABS}.}
}


@Book{vanDalen:2013,
 Author = {Dirk {van Dalen}},
 Title = {{Logic and structure}},
 FJournal = {{Universitext}},
 Journal = {{Universitext}},
 ISSN = {0172-5939},
 ISBN = {978-1-4471-4557-8; 978-1-4471-4558-5},
 Pages = {x + 263},
 Year = {2013},
 Publisher = {London: Springer},
 Language = {English},
 DOI = {10.1007/978-1-4471-4558-5},
 MSC2010 = {03-01 03-02 03B05 03B10 03B15 03B20 03C07 03C20},
 Zbl = {1262.03002}
}


@Book{TroelstraDalen:1988,
 Author = {A. S. {Troelstra} and D. {van Dalen}},
 Title = {{Constructivism in mathematics. An introduction. Volume I}},
 FJournal = {{Studies in Logic and the Foundations of Mathematics}},
 Journal = {{Stud. Logic Found. Math.}},
 Volume = {121},
 ISBN = {0-444-70506-6},
 Pages = {xv + 355},
 Year = {1988},
 Publisher = {Amsterdam etc.: North-Holland},
 Language = {English},
 MSC2010 = {03F50 03F55 03F60 03F65 03-02 03-01},
 Zbl = {0653.03040}
}


@Book{Heyting:1971,
 Author = {A. {Heyting}},
 Title = {{Intuitionism. An introduction. 3rd revised ed}},
 FJournal = {{Studies in Logic and the Foundations of Mathematics}},
 Journal = {{Stud. Logic Found. Math.}},
 Year = {1971},
 Publisher = {Elsevier, Amsterdam},
 Language = {English},
 MSC2010 = {03F55 03-01},
 Zbl = {0219.02013}
}

