\documentclass[12pt]{article}
\usepackage{amsmath,amssymb,amsfonts}
\begin{document}
In this note we show that the intuitionistic theory of polynomial
induction on $\Pi_1^{b+}$-formulas does not imply the
intuitionistic theory $IS_2^1$ of polynomial induction on
$\Sigma_1^{b+}$-formulas. We also show the converse assuming the
Polynomial Hierarchy does not collapse. Similar results hold also
for length induction in place of polynomial induction. We also
investigate the relation between various other intuitionistic
first-order theories of bounded arithmetic. Our method is mostly
semantical, we use Kripke models of the theories.
\end{document}