Hi Bryan:

there is a lot of related work with respect to what we discussed this morning.
Please see what I write at the very end.

This gives a lot more insight into what the mathematical challenges
could be.

Please add references to this work to the proposal. Suggestions for references are below
but you might foind better ones.

-- Karl

From: http://planetmath.org/?op=getobj&from=objects&name=GameTheoreticalQuantifier

This concept can be generalized to the game-theoretical quantifiers. This concept comes from interpreting a formula as a game between a ``Prover'' and ``Refuter.'' A theorem is provable whenever the Prover has a winning strategy; at each and  the Refuter chooses which side they will play (so the Prover must be prepared to win on either) while each  is a choice for the Prover. At a  not, the players switch roles. Then  or represents a choice for the Refuter and  for the Prover.


From:
http://en.wikipedia.org/wiki/Game_semantics

Classical logic

The simplest application of game semantics is to propositional logic. Each formula of this language is interpreted as a game between two players, known as the "Verifier" and the "Falsifier". The Verifier is given "ownership" of all the disjunctions in the formula, and the Falsifier is likewise given ownership of all the conjunctions. Each move of the game consists of allowing the owner of the dominant connective to pick one of its branches; play will then continue in that subformula, with whichever player controls its dominant connective making the next move. Play ends when a primitive proposition has been so chosen by the two players; at this point the Verifier is deemed the winner if the resulting proposition is true, and the Falsifier is deemed the winner if it is false. The original formula will be considered true precisely when the Verifier has a winning strategy, while it will be false whenever the Falsifier has the winning strategy.

If the formula contains negations or implications, other, more complicated, techniques may be used. For example, a negation should be true if the thing negated is false, so it must have the effect of interchanging the roles of the two players.

More generally, game semantics may be applied to predicate logic; the new rules allow a dominant quantifier to be removed by its "owner" (the Verifier for existential quantifiers and the Falsifier for universal quantifiers) and its bound variable replaced at all occurrences by an object of the owner's choosing, drawn from the domain of quantification. Note that a single counterexample falsifies a universally quantified statement, and a single example suffices to verify an existentially quantified one.

See also:
http://www.cis.upenn.edu/~giorgi/cl.html
Computability Logic

Reference this 2009 paper from Springer Verlag:
http://arxiv.org/PS_cache/cs/pdf/0507/0507045v3.pdf

This was about why in the beginning was Semantics. 
Now a few words about why Semantics was Game
Semantics. For CL, game is not just a game. It is a foundational mathematical concept on which a powerful
enough logic (=semantics) should be based. This is so because, as noted, CL sees logic as a “real-life
navigational tool”, and it is games that appear to offer the most comprehensive, coherent, natural, adequate
and convenient mathematical models for the very essence of all “navigational” activities of agents: their
interactions with the surrounding world. An agent and its environment translate into game-theoretic terms
as two players; their actions as moves; situations arising in the course of interaction as positions; and success
or failure as wins or losses.
It is natural to require that the interaction strategies of the party that we have referred to as an “agent” be
limited to algorithmic ones, allowing us to henceforth call that player a machine.

Also reference:
http://arxiv.org/abs/cs.LO/0404023

i@article{DBLP:journals/corr/cs-LO-0404023,
  author    = {Giorgi Japaridze},
    title     = {Propositional computability logic I},
      journal   = {CoRR},
        volume    = {cs.LO/0404023},
	  year      = {2004},
	    ee        = {http://arxiv.org/abs/cs.LO/0404023},
	      bibsource = {DBLP, http://dblp.uni-trier.de}
	      }

In the same sense as classical logic is a formal theory of truth, the recently initiated approach called computability logic is a formal theory of computability. It understands (interactive) computational problems as games played by a machine against the environment, their computability as existence of a machine that always wins the game, logical operators as operations on computational problems, and validity of a logical formula as being a scheme of "always computable" problems. 

The approach initiated recently in [7] called computability logic is a formal theory of computability in the
same sense as classical logic is a formal theory of truth. It understands (interactive) computational problems
as games played by a machine against the environment, their computability as existence of a machine that
always wins the game, logical operators as operations on computational problems, and validity of a logical
formula as being a scheme of “always computable” problems. With the meaning of computational resources
being dual/symmetric to that of computational problems (what is a problem for the machine is a resource
for the environment, and vice versa), computability logic is, at the same time, a logic of computational
resources.

As this was mentioned, technically we understand interactive problems as games, or dialogues, between
two agents/players: machine and environment, symbolically named as . and ¡Ñ, respectively. Machine, as
its name suggests, is specified as a mechanical device with fully determined, algorithmic behavior, while
the behavior of the environment, that represents a capricious user or the blind forces of nature, is allowed
to be arbitrary. ¡°Observable actions¡± by these two agents translate into game-theoretic terms as their
moves, ¡°interaction histories¡± as runs, i.e. sequences of moves, ¡°possible outputs¡± as legal runs, and ¡°right
outputs¡± as successful, or winning runs. The machine is considered to solve a given problem/game if it
wins it (ensures that a right/successful output/run is generated) on every possible input no matter how the
environment behaves.
===========================
What is different in SCG:
We don't play games against the arbitrary environment but against other machines.
We are not interested to use games to define computability (as in computability logic)
but to judge the quality of a machine compared to other machines.
The machines are compared with respect to resource consumption and 
quality of the solutions achieved.

While in computability theory the second player represents the "blind forces of nature",
in SCG the second player is a machine that most obey the rules of the artifical market.