C. ?. Case and A. ?. If, then there is a maximal confluent set H ? rpGq with r? rp?q s H ? 0 r?s G for the application r of ? ? to A ? B ? in some ? ? for some ? P G

C. ?. Case and A. ?. Let, By monotonicity of input formulas (Lemma 5.18), A ? B ? P r?s H . By Lemma 5.14, either A ? P r?s H or B ? P r?s H . Thus, for any r?s H ? r?s G , we have by IH

C. ?. Case and 3. If, 14, there is another sequent ? P G with A ? P ? for the child ? of ? ? in tr p?q. Thus, r?s G ( A by IH. Since r?s G R 0 r?s G , we have r?s G ( 3A. Case C ? " 3A ? . Let 3A ? P r?s G and r?s G Rr?s G . Then, by Lemma 5

C. ?. Case and A. If, then there is a maximal confluent set H ? rpGq with r? rp?q s H ? r?s G for the application r of ? to A ? in some ? ? for some ? P G. In that case, A ? P r?s H for the child ? of ? rp?q in tr prp?qq. Thus, by IH r?s H * A

C. Case, A ? combines the monotonicity argument for input implications with the use of Lemma 5

N. Alechina, M. Mendler, E. Valeria-de-paiva, and . Ritter, Categorical and Kripke semantics for constructive S4 modal logic Computer Science Logic, 15th International Workshop, 10th Annual Conference of the EACSL Proceedings, volume 2142 of Lecture Notes in Computer Science, pp.292-307, 2001.
DOI : 10.1007/3-540-44802-0_21

R. Arisaka, A. Das, and L. Straßburger, On nested sequents for constructive modal logic, Logical Methods in Computer Science, vol.11, issue.33, pp.10-2168, 2015.

W. Evert and . Beth, The Foundations of Mathematics: A Study in the Philosophy of Science, Logic and the Foundations of Mathematics. Harper & Row, p.25, 1959.

G. M. Bierman and V. C. De-paiva, On an intuitionistic modal logic, Studia Logica, vol.65, issue.3, pp.383-41610, 2000.
DOI : 10.1023/A:1005291931660

K. Brünnler, Deep sequent systems for modal logic Archive for Mathematical Logic, pp.551-577, 2009.

K. Chaudhuri, S. Marin, and L. Straßburger, Modular focused proof systems for intuitionistic modal logics, 1st International Conference on Formal Structures for Computation and Deduction, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01417603

H. B. Curry, Foundations of Mathematical Logic, 1977.

R. Dyckhoff, Intuitionistic Decision Procedures Since Gentzen, Advances in Proof Theory, pp.245-267, 2016.
DOI : 10.1007/978-3-319-29198-7_6

U. Egly and S. Schmitt, On intuitionistic proof transformations, their complexity, and application to constructive program synthesis, Fundamenta Informaticae, vol.39, issue.12, pp.59-8310, 1999.
DOI : 10.1007/bfb0055908

W. B. Ewald, Intuitionistic tense and modal logic, The Journal of Symbolic Logic, vol.344, issue.01, pp.166-17910, 1986.
DOI : 10.2307/2273953

G. and F. Servi, Axiomatizations for some intuitionistic modal logics, Rendiconti del Seminario Matematico, vol.42, issue.3, pp.179-194, 1984.

F. B. Fitch, Intuitionistic modal logic with quantifiers, Portugaliae Mathematica, vol.7, issue.2, pp.113-118, 1948.

M. Fitting, Prefixed tableaus and nested sequents Annals of Pure and Applied Logic, pp.291-313, 2012.
DOI : 10.1016/j.apal.2011.09.004
URL : https://doi.org/10.1016/j.apal.2011.09.004

C. Melvin and . Fitting, Intuitionistic Logic, Model Theory and Forcing, volume 54 of Studies in Logic and the Foundations of Mathematics, p.54, 1969.

J. Garson, Modal logic The Stanford Encyclopedia of Philosophy URL: https://plato, 2016.

G. Gentzen, Untersuchungen ???ber das logische Schlie???en. I, Mathematische Zeitschrift, vol.39, issue.1, pp.176-21010, 1935.
DOI : 10.1007/BF01201353

S. Maehara, Eine Darstellung der Intuitionistischen Logik in der Klassischen, Nagoya Mathematical Journal, vol.2, pp.45-6410, 1954.
DOI : 10.1017/S0027763000010023

S. Marin and L. Straßburger, Label-free modular systems for classical and intuitionistic modal logics, Advances in Modal Logic, pp.387-406, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01092148

M. Mendler and S. Scheele, Cut-free Gentzen calculus for multimodal CK Information and Computation, pp.1465-1490, 2011.

F. Pfenning and R. Davies, A judgmental reconstruction of modal logic, Mathematical Structures in Computer Science, vol.11, issue.04, pp.511-54010, 2001.
DOI : 10.1017/S0960129501003322

G. Plotkin and C. Stirling, A framework for intuitionistic modal logics Theoretical Aspects of Reasoning About Knowledge Extended abstract, pp.399-406, 1986.

D. Prawitz, Natural Deduction: A Proof-Theoretical Study Originally published as a PhD thesis by Almquist & Wiksell, 1965.

A. K. Simpson, The Proof Theory and Semantics of Intuitionistic Modal Logic, 1994.

L. Straßburger, Cut Elimination in Nested Sequents for Intuitionistic Modal Logics, Foundations of Software Science and Computation Structures, 16th International Conference, FOSSACS 2013 Proceedings, pp.209-22410, 2013.
DOI : 10.1007/978-3-642-37075-5_14

P. Jan-von, Saved from the Cellar: Gerhard Gentzen's Shorthand Notes on Logic and Foundations of Mathematics. Sources and Studies in the History of Mathematics and Physical Sciences, pp.10-1007, 2017.