How to determine whether a proof requires "higher-order reasoning techniques"?

Question

The question:

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.

Example:

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...?

Answer 1

Briefly, every theorem stated in first-order logic has a first-order proof.

In his book "An Introduction to Mathematical Logic and Type Theory", Peter B. Andrews develops both first-order logic and a system of higher-order logic Q₀, which is generally considered to be the theory basis of modern higher-order provers. (See the introduction to the HOL logic for example.)

For Q₀ and similar systems, Andrews shows that the higher-order logics he describes can be considered as conservative extensions of first-order logic and writes (second edition, p. 259) that, "In summary, every first-order theorem of type theory has a first-order proof."

Given your practical concerns though, I also quote the following paragraph:

"However, some theorems of first-order logic can be proved most efficiently by using concepts which can be expressed only in higher-order logic. Examples may be found in [Andrews and Bishop, 1996] and [Boolos, 1998, Chapter 25]. Statman proved [Statman, 1978, Proposition 6.3.5] that the minimal length of a proof in first-order logic of a wff of first-order logic may be extraordinarily longer than that the minimal length of a proof of the same wff in second-order logic. A related result by Godel [Godel, 1936] is that in general 'passing to the logic of the next higher order has the effect, not only of making provable certain propositions that were not provable before, but also of making it possible to shorten, by an extraordinary amount, infinitely many of the proofs already available'. A complete proof of this may be found in [Buss, 1994]."