15
$\begingroup$

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

$\endgroup$
  • 2
    $\begingroup$ 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. $\endgroup$ – Kaveh Apr 5 '16 at 10:08
  • 2
    $\begingroup$ 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." $\endgroup$ – Martin Berger Apr 6 '16 at 11:47
  • $\begingroup$ @MartinBerger I think for purposes of this question, axiom schemes count as "higher-order reasoning techniques" $\endgroup$ – fread2281 Apr 30 '17 at 5:51
  • $\begingroup$ @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. $\endgroup$ – Martin Berger Apr 30 '17 at 11:23
6
$\begingroup$

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 Q0, which is generally considered to be the theory basis of modern higher-order provers. (See the introduction to the HOL logic for example.)

For Q0 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]."

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.