An Independence Result for Intuitionistic Bounded Arithmetic

摘要

It is shown that the intuitionistic theory of polynomial induction on positive Π_1~b (coNP) formulas does not prove the sentence - any x, y exist z ≤ y(x ≤ |y| → x = |z|). This implies the unprovability of the scheme - PIND(Σ_1~(b+)) in the mentioned theory. However, this theory contains the sentence any x, y - exist z ≤ y(x ≤ |y| → x = |z|). The above independence result is proved by constructing an ω-chain of submodels of a countable model of S_2 + Ω_3 + - exp such that none of the worlds in the chain satisfies the sentence, and interpreting the chain as a Kripke model.