Consider a formula made up of only conjunctions and disjunctions and true/false. The first player tries to prove the formula and gets to move at every disjuncti

Consider a formula made up of only conjunctions and disjunctions and true/false. The first player tries to prove the formula and gets to move at every disjunction and is allowed to select which side of the disjunction to prove. The second player tries to prevent the first player from finding a proof and gets to move at every conjunction, selecting a side of the conjunction to descend to. The final state here is an atomic proposition which is either true or false and determines which player won. You derive a value function from that in the same way as you do for Go or Chess. You can extend this idea to full first-order intuitionistic logic and probably also to higher-order logics, as well as many different modal logics. There are also formulations of classical logic as a single player game, but that doesn't seem to be very useful here.