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.