kick, albeit something quite a bit less than full second-order logic.

&gt; Therefore my preference is to remain first order until it can be
&gt; demonstrated that critical requirements can not be satisfied without
&gt; moving from that. You have said that these situations should not
&gt; occur, or can be overcome, and I will buy that until the contrary is
&gt; proved.  (see how trusting I am!)

Or naive! :-)  Overall, yes, there seems little need to go beyond
first-order, though the additional expressive p