# How to determine whether a proof requires “higher-order reasoning techniques”?

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

• What you are asking is essentially deciding if a given formula is provable (in your weaker system) which is in general undecidable even for a simple theory like Q. But provability is actually not very useful because a stronger theory can shorten proofs of a theorem a lot. Deciding if a theorem has a short proof is NP-complete. I doubt there is a good heuristic. – Kaveh Apr 5 '16 at 10:08
• Peano arithmetic has induction, and Peano arithmetic is first-order (i.e. quantifies only over individuals). Same for ZFC. To quote Martin Davis: "higher-order logics are just notational variants of set theories formalized in first-order logic, the question of the use of higher-order formalisms in mechanical theorem-proving is simply a matter of whether or not such formalisms suggest useful algorithms." – Martin Berger Apr 6 '16 at 11:47
• @MartinBerger I think for purposes of this question, axiom schemes count as "higher-order reasoning techniques" – fread2281 Apr 30 '17 at 5:51
• @fread2281 It is helpful to be careful with terminology. There are set-theories that have a finite axiomatisation (e.g Neumann–Bernays–Gödel set theory which is a conservative extension of ZFC). In contrast the axiom schemata of ZFC cannot be expressed by a finite number of axioms. I think but I'm not sure right now that the axiom schemes do not need the full power of set theory or higher-order logic. – Martin Berger Apr 30 '17 at 11:23