8/30/2026
Every logical connective or quantifier reduces to a move in a two-player game: someone puts forward a formula, and at each step either they or their interlocutor commits to a simpler one by endorsing or denying it.
The game is a game of moves. As it proceeds, only one person is able to make the next move (the Holder). After a move is made, often, but not always, the next move goes to the Opponent. If so, the opponent then becomes the holder and the former holder becomes the opponent. Sometimes the rules require the holder to make two moves in a sequence. Then, it is also possible for the same or a different rule to compel the holder to make yet further moves. The upshot is that usually whose move it is switches between the two parties after just one move. But it is possible for the holder to make any number of moves in a row.
When the game starts, the User has first move and is the Holder. The first mover can choose the Endorse or Deny the formula under consideration.
If the formula is atomic i.e. without any connectives e.g. F(a), and an Endore Deny choice has been made, the game ends at that point. If the formula is true (e.g. F(a) is true) and the Holder has endorsed it or if the formula is false (e.g. F(a) is false) and the Holder has denied it, the Holder wins. Otherwise the Holder loses and the Opponent wins.
If the formula is not atomic, a rule will apply, and which rule that is will be depend on the the main connective of the formula and the Endorse Deny choice. We will explain the rule pairs one by one.
Now for the Rules. Below, every branch is labelled Holder (whoever currently owns the claim on the table) or Opponent (whoever doesn't). The Holder is always either the User or the program, but it can change as the game runs.
Negation
Flips the polarity: no branch, no handoff — the Holder stays the Holder.
Endorses
Denies
Time runs from top to bottom in these diagrams. So, if the Holder Endorses ~F(a), for example, the Holder is required to Deny F(a). And were the Holder to Deny ~F(a), the Holder would be required to Endorse F(a). This pair of rules can lead to a Holder make several moves in a row. For example, the formula ~~~~~F(a), with 5 'nots' would lead to a sequence of 5 Endorse-Denies.
Conjunction
To endorse both is to survive a challenge on either — so the Opponent picks the challenge. To deny it, the Holder just needs one weak link, and picks it themself.
Endorses
Opponent becomes the new Holder.
Denies
Holder stays the Holder.
Whenever there is a branching in the diagram, a player will have a a choice to make. For example, if the Holder were to Endorse F(a)&G(b) the Opponent would have to either Deny F(a) or Deny G(b). Additionally, the Opponent would become the Holder and have to follow through on one of those denials.
Disjunction
Mirror image of &: endorsing it only takes one good witness, and the Holder gets to supply it. Denying it means refuting every option, so the Opponent picks which one to test.
Endorses
Holder stays the Holder.
Denies
Opponent becomes the new Holder.
Sometimes, when there is a choice of one thing or another (or another...) and one successful choice is made, logicians call a successful choice a 'witness'. (One can almost use that terminology in everyday speech. For example, 'one of the football team Melchester Rovers can run 50 yards in 6 seconds, witness Roy Race'.)
Conditional
Same shape as ∨ (A→B is A denied, or B). Endorsing it, the Holder picks their ground; denying it, the Opponent does.
Endorses
Holder stays the Holder.
Denies
Opponent becomes the new Holder.
Biconditional
Unpacked as two conditionals (A→B and B→A) and treated exactly like Conjunction over them.
Endorses
Opponent becomes the new Holder — then the Conditional rule above applies to them.
Denies
Holder stays the Holder.
Universal Quantifier
Like a big Conjunction across the whole Universe — the Opponent picks the individual that tests the claim.
Endorses
Denies
The notation <formula>[i/v] means the 'the formula with i substituted for free occurrences of the free variable v throughout' or, briefly, 'the formula with i for v'. For example, F(x)[a/x] is F(a).
Existential Quantifier
Like a big Disjunction across the whole Universe — mirror image of ∀: the Holder picks the witness.
Endorses
Denies