Vol. 16 No. 2, © The Author, 2006. Published by Oxford University Press. All rights reserved.
Original Articles |
An Independence Result for Intuitionistic Bounded Arithmetic
Department of Mathematics, Shahid Beheshti University, Evin, Tehran, Iran, and Institute for Studies in Theoretical Physics and Mathematics (IPM), P.O. Box 19395-5746, Tehran, Iran. Email: ezmoniri{at}ipm.ir
It is shown that the intuitionistic theory of polynomial induction on positive
1b (coNP) formulas does not prove the sentence ¬¬
x, y
z
y(x
|y|
x = |z|). This implies the unprovability of the scheme ¬¬PIND(
1b+) in the mentioned theory. However, this theory contains the sentence
x, y¬¬
z
y(x
|y|
x = |z|). The above independence result is proved by constructing an
-chain of submodels of a countable model of S2 +
3 + ¬exp such that none of the worlds in the chain satisfies the sentence, and interpreting the chain as a Kripke model.
Keywords: Bounded arithmetic, intuitionistic logic, Kripke model, NP, polynomial hierarchy, polynomial induction
Received 2 December 2004.