We shall address the issues of modelling or formalising game theoretic properties like Nash Equilibrium, Finite Improvement Property, Weak Acyclicity of various game forms in various kinds of logic. We shall investigate the _expressive powers_ offered by each logic, the _model checking_ theorems and also a _completeness_ proof of a decidable logic variant. We hope that this investigation would have an impact on the formalisation of game theory and its allied areas like computational social choice theory.