Semi decision procedures for Peano arithmetic? Is there an efficient semi-decision procedure (i.e. an algorithm that sometimes works and sometimes not) for -at least- elementary problems in peano arithmetic? 
I am not talking about weak fragments of Peano arithmetic such as Presburger arithmetic, which have very little expresive power, but of Peano arithmetic itself.
In particular, I am seeking a theory in which you could define what is a prime number and design a semi decidable algorithm too. 
The only example I is near to  what I'm thinking is this
http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.117.2911&rep=rep1&type=pdf.
 A: You might be interested in "generic-case," as opposed to worst-case complexity results.
The earliest-that-I'm-aware-of variant is average case complexity; see for example "Matrix transformation is complete for the average case" (http://research.microsoft.com/en-us/um/people/gurevich/opera/97.pdf), in which Blass and Gurevich show that the Bounded Product Problem for $PSL_2(\mathbb{Z})$ has average-case polynomial complexity, even though it is NP-complete in the worst case.
This proved tricky to study, and so versions based on asymptotic density (generic and strong-generic computability) were introduced in "Generic- case complexity, decision problems in group theory and random walks" (http://www.sciencedirect.com/science/article/pii/S0021869303001674). A number of "infeasible," or even outright incomputable, problems turn out to be simple in the strongly generic sense: e.g., the word problem for Boon's original example of a group with undecidable word problem is strongly generically linear-time decidable!
The point is, if you have an algorithm $A$ solving a problem $P$ "most of the time" in time $f(n)$, we can truncate $A$ to $A_f$ by stopping $A$ after $f(n)$ steps; this gives an efficient (well, $f$-time) algorithm for $P$ which works "most" of the time.
Off the top of my head, I can't recall results specifically about problems from number theory, but I'm sure there are some; I'll add them once I find them. Note, however, that these problems which are phrased in terms of group theory etc. are really problems about realtions on natural numbers, so do (even if not explicitly) correspond to subtheories of PA.

This has also been studied in pure computability theory, that is, without regard to feasibility: see e.g. http://www.math.uiuc.edu/~jockusch/lastGC.pdf. Also see http://arxiv.org/pdf/1406.2982.pdf for some more esoteric aspects.
