Constructive Second Order Weak Arithmetic with Extracting Polynomial Time Algorithms
by
Anatoly Beltiukov
Udmurt State University

A weak intuitionistic second order arithmetic is considered with a special restriction for the induction scheme:

A(0) & for all x (A(x)  = >  A(x+1))  = >   for all x A(x).

It means that A(x) in this scheme may not contain some specified combinations of quantifiers and logical connectives. The theory does not contain operations of addition and multiplication. It is allowed to use only corresponding predicates. It is proved that extracting the realizations from the proofs of the theory leads to algorithms, that are computable within a time that is bounded by a polynomial of the first order values. For example, the realization of a proved formula of the form

for all n  for all f ( for all y (f(y) < n)  = >   exists x A(n, f, x))

contains an algorithm that computes a required value of x using n and f (as an oracle) within a time that is bounded by a polynomial of n.

Date received: March 15, 2002