Inspired by Fagin's result that NP = ∑11, we have developed a partial framework to investigate expressibility inside ∑11 so as to have a finer look into NP. The framework uses interesting combinatorics derived from second-order Ehrenfeucht-Fraïssé games and the notion of game types. Some of the results that have been proven within this framework are: (1) for any k, divisibility by k is not expressible by a ∑11 sentence where (1.i) each second-order variable has arity at most 2, (1.ii) the first-order part has at most 2 first-order variables, and (1.iii) the first-order part has quantifier depth at most 3, (2) adding one more first-order variable makes the same problem expressible, and (3) inside this last logic the parameter k creates a proper hierarchy with varying the number of second-order variables.

Ehrenfeucht-Fraïssé games, divisibility, expressibility, first-order, second-order