Bounded computation and incompleteness

Question

Is there a complete theory T over a logical language L such that bounded computation may be encoded in it? Computational questions can be framed as arithmetical ones by interpreting them over natural numbers. Let $\phi$ be a first order statement which states that $P \neq NP$ in the language of arithmetic. Then either $\phi$ belongs to Th(N) or its negation does (i.e.) it contains the answer to the P vs NP problem.

However, since Th(N) is not RE, I would like to know if computation (in particular, bounded computation) can be interpreted over some alternate structure with nicer properties (i.e. whose theory is decidable). Note that if a theory is complete, then it cannot be RE-complete (i.e.) deciding whether any $\phi$ belongs to the theory is not RE-complete, it is either recursive or RE-hard.

The context is Razborov's paper on "Unprovability of lower bounds on circuit size in certain fragments of bounded arithmetic" in which he shows that the bounded arithmetic theory $S_2^2(\alpha)$ cannot prove polynomial circuit lower bounds for SAT assuming Strong Pseudo Random Generators (SPRGs) exist. Here the statement "SAT does not have poly size circuits" can be written as a bounded sentence when interpreted over the naturals.

I want to understand if the presence of a total order is required for the interpretation of computation inside a structure. Suppose I take graphs with the minor ordering (which is a WQO), is it possible to interpret computation inside this? My only point of reference is the undecidability of First order satisfiability by reduction from the Halting Problem. In this case, we do not seem to require a successor function, just the idea of a "future" configuration with certain properties. I understand that this setting is different from interpretation inside a structure. I want to understand this difference.

Answer 1

It depends on what you mean by "encode computation". There are many papers on the topic, a good starting reference is "Metamathematics of First Order Logic" by Petr Hajek and Pavel Pudlak. Pavel defined what is called sequential theory for theories where you can encode strings (I don't see if being a computation or not means much).

P vs. NP can be studied for other structures, first order logic with order is sufficient to phrase the question whether every $\Sigma^b_1$ formula is equivalent to a quantifier-free one (and you can enrich the language to contain all operations that you want to assume to be efficient). The strings case is old (I will add reference later). It is also studied over real numbers (in the context of BSS model).

The question can be studied over structures without order, see the work on algebraic complexity like Valiant's VP vs. VNP and also GCT (for complex numbers and other fields).