\lor \neg p$. Adding $\Gamma {\ensuremath{\vdash}}\varphi \vee
\neg\varphi$ as an axiom for an arbitrary term $\varphi$ gives an inconsistent system.[^3]

It is well-known (see e.g. [@SorensenUrzyczyn2006 Chapter 11]) that in higher-order logic all logical connectives may be defined from $\forall$ and $\supset$ as follows. $$\begin{aligned}
  \bot &\equiv& \forall p : {\ensuremath{\mathrm{Prop}}}\,.\, p \\
  \neg \varphi &\equiv& \varphi \supset \bot \\
  \varphi \wedge \psi &\equiv& \forall p : {\ensuremath{\mathrm{Prop}}}\,.\, (\varphi \supset \psi \supset p) \supset p \\
  \varphi \vee \psi &\equiv& \forall p : {\ensuremath{\mathrm{Prop}}}\,.\, (\varphi \supset p) \supset (\psi \supset p) \supset p \\
  \exists x : \alpha \,.\, \varphi &\equiv& \forall p : {\ensuremath{\mathrm{Prop}}}\,.\, (\forall x : \alpha \,.\, \varphi \supset p) \supset p\end{aligned}$$ One may therefore wonder why we take $\vee$ and $\bot$ as primitive. The answer is that if we defined the connectives by the above equations, then the inference rules that could be derived for them would need to contain additional restrictions. For instance, we would be able to derive only the following variants of $\vee$-introduction.

  ------------------------------------------------------------------------------ ----------------------------------------------------------------------------------------------------------------------------------------
  $                                                                                                                                                                                                                     $
      {\vee_{i1}':}\; \inferrule{\Gamma {\ensuremath{\vdash}}\varphi \\ \Gamma         {\vee_{i2}':}\; \inferrule{\Gamma {\ensuremath{\vdash}}\psi \\ \Gamma {\ensuremath{\vdash}}\varphi : {\ensuremath{\mathrm{Prop}}}}
        {\ensuremath{\vdash}}\psi : {\ensuremath{\mathrm{Prop}}}}                                                                                                         {\Gamma {\ensuremath{\vdash}}\varphi \vee \psi}
      {\Gamma {\ensuremath{\vdash}}\varphi \vee \psi}                                                                                                                                                                   $
    $                                                                            
  