I'm imagining some kind of sliding-block puzzle game, with each block as a symbol or logical operator. You start off with some axioms and then have to go through and construct proofs for progressively more complex first-order logic expressions.

Or maybe a game that does for syllogisms what Manufactoria does for Turing Machines. (Memetic hazard warning!)

This could be promising...