Pseudo-decision procedures for first order arithmetic

Question

I was reading this paper http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.117.2911&rep=rep1&type=pdf in which the author describes an algorithm, based on Groebner basis, whose input is a proposition in Peano arithmetic that satisfies a specific quantifier structure, and the output is True or False. If the output is true, then the proposition must be true. However, sometimes the output is false but the proposition is true, so the algorithm is not a decision procedure for Peano arithmetic -I already know that such an algorithm cannot exist, by Matiyasevich theorem-.

I have two questions:

1: Are there any similar results to this, i.e. an efficient pseudo-decision procedure such that if the output is true, then the proposition must be true, but we cannot say anything in the other case?

2: Is there a chance to use similar ideas to the ones in the paper so that we can overcome the limitations on the quantifier structure of the input propositions, and ask things like "There are many infinitely many prime numbers"?

Answer 1

I don't know anything about (2), but let me try to address (1):

Given a decision problem $P$, let's say a Turing machine $\Phi$ is a pseudo-solver for $P$ if for every $n$, $\Phi(n)$ halts implies $P(n)\iff\Phi(n)=1$. (Note that the algorithm you describe can be thought of as a pseudo-solver, by replacing "outputs "FALSE"" with "goes into an endless loop.") Now, as The Masked Avenger says, the Turing machine which never halts is of course a pseudo-solver for every problem, so that's not really what we're interested in.

That is, we might want to ask:

For which decision problems is there a pseudo-solver $\Phi$ such that (1) $\Phi$ runs efficiently, and (2) $\Phi$ halts frequently?

For example, look at algorithms which halt on a set of asymptotic density 1 - this yields generic computability. We could also allow pseudo-solvers to make (rare) errors - demanding correct halting on a set of density 1 yields coarse computability - or look at other variations; see http://arxiv.org/pdf/1406.2982.pdf for a survey of these.

Lots of decision problems which are complex (or unsolvable) according to the usual model are generically/coarsely/similarly computable in very efficient time - for example, the word problem for Boon's original example of a group with undecidable word problem is generically decidable in linear time.

Answer 2

1) A positive result: Mathematica's FindInstance provides a good pseudo-decision procedure for most existential or universal questions, e.g. $$\mathtt{FindInstance[ x^2 - 3y^2 == 1 \ \&\& \ 10 < x < 100,\{x,y\}, Integers]}.$$ It can accept inputs of nested quantifiers also.

2) A negative result: The theory $I\Delta_0$, which proves the totality of all polynomial-growth functions, is not known to prove the infinitude of primes. At least, no one has found such a proof since 1988, when Paris, Wilkie and Woods proved the infinitude of primes from $I\Delta_0 + $ "the function $x \rightarrow x^{\log_2(x)}$ is total".

So, extrapolating unrigorously, any algorithm now for deciding the infinitude of primes probably can also decide the totality of some non-polynomial-growth functions, and probably isn't efficient in the usual polynomial-time sense. Good algorithms may only be able to decide simpler results.