Expressibility in Σ1

Inspired by fagin’s result that np = σ1 1 , we have developed a partial framework to investigate expressibility inside σ1 1 so as to have a finer look into np. the framework uses interesting combinatorics derived from second-order ehrenfeucht- fra¨ıss´e 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 σ1 1 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.