 Giorgi Japaridze has proposed a ‘computability logic’ for studying computation. Its syntax is first-order logic with some extra items reminiscent of linear logic. Its semantics is in terms of semantic games with some unusual features. For example it is not always determined which player makes the next move. The notion of strategy functions is no longer adequate for describing the players; instead Japaridze describes ways of reading the second player (player \(\exists\) in our notation) as a kind of computing machine. Further information is on his website.