{\ensuremath{\vdash}}\psi : {\ensuremath{\mathrm{Prop}}}}{                \Gamma {\ensuremath{\vdash}}\varphi \\ \Gamma {\ensuremath{\vdash}}\psi
                                       \Gamma {\ensuremath{\vdash}}(\varphi \supset \psi) : {\ensuremath{\mathrm{Prop}}}}                                                                                }{
                                                                               $                                                                                                    \Gamma {\ensuremath{\vdash}}\varphi \wedge \psi
                                                                                                                                                                                                          }
                                                                                                                                                                                                         $
  ------------------------------------------------------------------------------------------------------------------------------------------------------- ---------------------------------------------------------------------------------------------

Note that in general the elimination rules for $\wedge$ and the rules for $\exists$ cannot be derived from the rules for $\vee$ and $\forall$, because we would not be able to prove the premise $\varphi : {\ensuremath{\mathrm{Prop}}}$ when trying to apply the rule $\supset_i$. It is instructive to try to derive these rules and see where the proof breaks down.

In ${\ensuremath{{\cal I}}}_s$ the only non-standard restriction in the usual inference rules for logical connectives is the additional premise $\Gamma
{\ensuremath{\vdash}}\varphi : {\ensuremath{\mathrm{Prop}}}$ in the rule $\supset_i$. It is certainly unavoidable, as otherwise Curry’s paradox may be derived (see e.g. [@illat01; @Seldin2009]). However, we have standard classical higher-order logic if we restrict to terms of type ${\ensuremath{\mathrm{Prop}}}$, in the sense that the natural deduction rules then become identical to the rules of ordinary logic. This is made more precise in Sect. \[sec\_consistent\] where a sound translation from a traditional system of higher-order logic into ${\ensuremath{{\cal I}}}_s$ is described.

Note that we have the law of excluded middle only in the form $\forall
p : {\ensuremath{\mathrm{Prop}}}\,.\, p 