Suppose I have a specification of a problem consisting of axioms and a goal (i.e. the associated proof problem is whether the goal is satisfiable given all the axioms). Let us also assume that the problem does not contain any inconsistencies/contradictions among the axioms. Is there a way to determine in advance (i.e. without first constructing a full proof) that proving the problem will require "higher-order reasoning"?
By "higher-order reasoning", I mean applying proof steps which require higher-order logic to be written down. A typical example for "higher-order reasoning" would be induction: Writing down an induction scheme in principle requires using higher-order logic.
One can specify the proof problem "Is addition on two natural numbers commutative?" using first-order logic (i.e. define natural number via constructors zero/succ along with standard axioms, together with axioms that recursively define a "plus" function). Proving this problem requires induction on the structure of either the first or the second argument of "plus" (depending on the exact definition of "plus"). Could I have known this before attempting to prove it, e.g. by analyzing the nature of the input problem...? (Of course, this is just a simple example for illustration purposes - in reality, this would be interesting for more difficult proof problems than commutativity of plus.)
Some more context:
In my research, I frequently try to apply automated first-order theorem provers like Vampire, eprover etc. to solve proof problems (or parts of proof problems), some of which may require higher-order reasoning. Often, provers require quite some time to come up with a proof (provided there is a proof which only requires first-order reasoning techniques). Of course, trying to apply a first-order theorem prover to a problem that requires higher-order reasoning typically results in a timeout.
Therefore, I have been wondering whether there are any methods/techniques which can tell me in advance whether a proof problem will require higher-order reasoning techniques (meaning "don't waste time trying to hand it to a first-order theorem prover") or not, at least maybe for particular input problems.
I looked in the literature for an answer to my question and asked some fellow researchers from the area of theorem proving about that - but so far, I didn't receive any good answers. My expectation would be that there is some research on that topic from people who try to combine interactive theorem proving and automated theorem proving (Coq community? Isabelle community (Sledgehammer)?) - but so far, I could not find anything.
I guess that in general, the problem I outlined here is undecidable (is it?). But maybe there are good answers for refined versions of the problem...?