In this paper, A new formal framework for Stringology is proposed, which consists of a three-sorted logical theory $latex S$ designed to capture the combinatorial reasoning about finite strings. We propose a language $latex L_S$ for expressing assertions about strings, and study in detail two sets of formulas $latex \Sigma_0^B$, a set of formulas decidable in polytime, and $latex \Sigma_1^B$, a set of formulas with the property that those provable in $latex S$ yield polytime algorithms.