Integer Division and Second Order Weak Bounded Arithmetic

Satoru Kuroda

The theory T^{pol} is a second order theory whose Δ_{1}^{1,w} definable predicates (intuitively, provably NP ∩ co-NP predicates) are exactly those decidable in polynomial time. This theory, however, has a very poor ability in defining functions. Namely, Takeuti [Tak] proved that T^{pol} cannot define the function ⌊a/b⌋.

In the present talk, we will improve this result in the following way: let T^{pol+} be the theory T^{pol} extended by the function MSP (x, y) = ⌊x/2^{|y|}⌋. Then we have

Theorem 1 For k ∈ ω, T^{pol+} ⊢ ∀x∃y(y = ⌊x/k⌋ if and only if k is not a power of 2.

Contrary to the theorem of Takeuti, our proof is model-theoretical and makes use of the method of length initial substructures developed by Johannsen [Joh].

[CT] P. Clote and G. Takeuti. Bounded arithmetic for NC, AlogTIME, L and NL. Annals of Pure and Applied Logic. 56 (1992) 73–117.

[Joh] J. Johannsen. A remark on independence results for sharply bounded arithmetic. Mathematical Logic Quarterly. 44 (1998) 569–571.

[Tak] G. Takeuti. A second order version of S_{2}^{i} and U_{2}^{1}. JSL. 56 (1991) 1038–1063.

Address: Gumma Prefectural Women’s University, 1395-1 Kaminote, Tamamura-machi, Sawagun, Gunma, 370-1193, Japan

E-mail: satoru@@math.human.nagoya-u.ac.jp