  We provide a complete axiomatization of modal inclusion logic - team-based
modal logic extended with inclusion atoms. We review and refine an expressive
completeness and normal form theorem for the logic, define a natural deduction
proof system, and use the normal form to prove completeness of the
axiomatization. Complete axiomatizations are also provided for two other
extensions of modal logic with the same expressive power as modal inclusion
logic: one augmented with a might operator and the other with a single-world
variant of the might operator.
