$k_i + 1$ times, $\Gamma {\ensuremath{\vdash}}\forall x_1 :
  \alpha_1 \ldots \forall x_n : \alpha_n \,.\, t_{i,j,k} : \alpha_k$ for $j=1,\ldots,k_i$, $k=1,\ldots,n$, $x_1,\ldots,x_n \notin
  FV(f,\alpha_1,\ldots,\alpha_n,\beta)$ and $$\begin{aligned}
  \Gamma {\ensuremath{\vdash}}\forall x_1 : \alpha_1 \ldots \forall x_n :
  \alpha_n \,.\, \varphi_i &\supset& (f x_1 \ldots x_n = \\ && \;t_i (f t_{i,1,1}
  \ldots t_{i,1,n}) \ldots (f t_{i,k_i,1} \ldots t_{i,k_i,n})).
  \end{aligned}$$ If there is a term $g$ such that $\Gamma {\ensuremath{\vdash}}g : \alpha_1 \to
  \ldots \to \alpha_n \to {\ensuremath{\mathrm{Nat}}}$ and for $i=1,\ldots,m$ $$\begin{aligned}
  \Gamma {\ensuremath{\vdash}}\forall x_1 : \alpha_1 \ldots \forall x_n : \alpha_n
  \,.\, \varphi_i &\supset& (\left((f x_1 \ldots x_n) :
  \beta\right) \lor \\ && \;((g t_{i,1,1} \ldots t_{i,1,n}) < (g x_1 \ldots
  x_n) \land \ldots \land \\ && \;\;(g t_{i,k_i,1} \ldots t_{i,k_i,n}) < (g x_1
  \ldots x_n)))
  \end{aligned}$$ where $x_1,\ldots,x_n \notin FV(g)$, then $$\Gamma {\ensuremath{\vdash}}f : \alpha_1 \to \ldots \to \alpha_n \to \beta.$$

Conservativity and Consistency {#sec_consistent}
==============================

In this section we show a sound embedding of ordinary classical higher-order logic into ${\ensuremath{{\cal I}}}_s$, which we also conjecture to be complete. We have a completeness proof only for a restriction of this embedding to first-order logic. We also give a brief overview of the model construction used to establish consistency of ${\ensuremath{{\cal I}}}_s$.

