Hostname: page-component-7b7567c8c-fvjsw Total loading time: 0 Render date: 2026-11-15T05:21:22.315Z Has data issue: false hasContentIssue false

Forcing on bounded arithmetic II

Published online by Cambridge University Press:  12 March 2014

Gaisi Takeuti
Affiliation:
Department of Mathematics, University of Illinois, Urbana, Illinois 61801, USA E-mail: takeuti@math.uiuc.edu
Masahiro Yasumoto
Affiliation:
Graduate School of Polymathematics, Nagoya University, Chikusa-Ku, Nagoya, 464-01, Japan E-mail: D42985A@nucc.cc.nagoya-u.ac.jp

Extract

Forcing method on Bounded Arithmetic was first introduced by J. B. Paris and A. Wilkie in [10]. Then in [1], [2] and [3], M. Ajtai used the method to get excellent results on the pigeon hole principle and the modulo p counting principle. The forcing method on Bounded arithmetic was further developed by P. Beame, J. Krajíček and S. Riis in [4], [7], [6], [8], [5], [12], [11], [13]. It should be noted that J. Krajíček and P. Pudlák used an idea of Boolean valued in [9] and also Boolean valued notion is efficiently used for model theoretic constructions in [7], [6], [8], [5].

In our previous paper [14], we developed a Boolean valued version of forcing on Bounded Arithmetic using Boolean algebra which is generated by polynomial size circuits from Boolean variables and discussed its relation with NP = co-NP problem and P = NP problem. Especially we proved the following theorem and related theorems as Theorems 2, 3 and 4 in Section 2.

Theorem. If M[G] is not a model of S2, then NP ≠ co-NP and therefore P ≠ NP.

However in the proof of the Theorem, we used a consequence of P = NP. More precisely we used the following as a consequence of NP = co-NP, though it is a consequence of P = NP but not a consequence of NP = co-NP.

Suppose that NP = co-NP holds. Then there exists an NP-complete predicate ∃x ≤ t(a) A(x,a) with sharply bounded A(x, a) and a sharply bounded B(y, a) such that ∃x ≤ t(a) A(x,a) ↔ ∀y ≤ s(a)B(y, a). Then there exists polynomial time computable functions f and g such that the following two sequents hold.

Information

Type
Research Article
Copyright
Copyright © Association for Symbolic Logic 1998

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

Article purchase

Temporarily unavailable