 The language we defined above is second-order because the last clause in the definition of the formulas sanctions both quantified formulas of the form \(\forall x\phi\) and of the form \(\forall F\phi\). In what follows, we employ the standard definitions of the following formulas: