9/5/2026
Introduction
With a reasonable complex formula, it is not enough to know (or guess) that it is true (or false) in an Interpretation. One should also know the reasons why it is true (or false) or, alternatively, just what the assertion of the truth (or falsity) of the formula commits you to. The idea is that a view as to the truth-status of a compound formula has repercussions for views about the truth-status of the formula's constituents (and vice-versa). As a (simple) example, if you think that F(a)&F(b) is true you should think that F(a) is true and that F(b) is true (for then, and only then, is F(a)&F(b) true).
This insight lies behind the top-down approach of Game Theoretic Semantics (GTS) which is primarily from Leon Henkin, and Jaakko Hintikka, (valuable here for us are Jon Barwise and John Etchemendy, The Language of First-Order Logic, including Tarski’ s World 3.0, John Sowa on Model Theory Semantics, and Wilfrid Hodges and Jouko Väänänen. Logic and Games). The present work is closest to the Barwise and Etchemendy text (indeed there is a software book on this site on their Tarski's World).
The software widget will debate with you about these matters. The widget has two buttons: Endorse Deny. They work as follows. You use them when you have formed a view as to whether a selected formula (or list of formulas) is true (or is false), and you wish to argue the point with the widget. In the ordinary way you probably would not wish to do this, but if you disagree with the program about the truth value of a formula (or list of formulas) then tracing through the game will pinpoint the error (your error). There is also value in this if you would like to know what the formula means in the sense of what it commits you to.
A caution
One point that you might see: you can be right for the wrong reasons. You may believe a formula to be true, and perhaps it is true. But yet when you reason with the program, the computer beats you. This means that that the grounds for your belief are unsound. In another context, the philosopher John Stuart Mill argues in his essay On Liberty that freedom of speech is valuable because it encourages people to defend the views that they have, and this means that folks's views have some rational basis (as opposed to being guesses or parroted from the media or some 'authorities'). Winning this game requires you to place your semantical views on a sound basis.
The game
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 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
Worked examples
Two real traces from the software. The interpretation is: Universe = {a,b}, F = {a}, G = {b}. The software will use 'You' for the User and 'I' for itself.
F(a)→G(b), Deny — the formula is actually true, so denying it is a losing opening move.
F(a)≡G(b), Endorse — the program is forced to deny a conditional; the very next rule then applies to the User, not the program again.
When the widget is playing a game it puts in an arrow head '>' to indicate where it will write its reply to (and that the game is still in progress)-- when the game is over it removes this. (It is wise not to type in extra '>'s of your own. )
The program writes earlier instantiations made within a game even though these are perhaps not relevant to the current formula. For example, say we have a drawing containing an a which has both the properties F and G and consider a game for ∃x(F(x)&∃yG(y)) which you endorse
You endorsed ∃x(F(x)&∃yG(y))
You should endorse (F(x)&∃yG(y))[?/x]
for a ? that you choose.
and as the second move you endorse (F(x)&∃yG(y))[a/x] which leads to
You endorsed (F(x)&∃yG(y))[a/x]
I denied ∃yG(y)[a/x]
You should endorse G(y)[?/y,a/x]
for a ? that you choose. >
notice that the formula (∃y)G(y) does not even contain x; why then does the program tell you I denied ∃yG(y[)a/x] ? the reason is just to remind us that at the earlier stage, with the more complex formula, the instantiation a/x was chosen. These lists of instantiations are read with the oldest on the right and the newest on the left; a similar game can be played for ∃x(F(x)&∃xG(x)) and it would proceed
∃x(F(x)&∃xG(x))
You endorsed ∃x(F(x)&∃xG(x))
You should endorse (F(x)&∃xG(x)[?/x]
for a ? that you choose.
choosing a/x
You endorsed (F(x)&∃xG(x))[a/x]
I denied ∃xG(x)[a/x]
You should endorse G(x)[?/x,a/x]
for a ? that you choose. >
this tells us that the program wishes to know your present choice as an instantiation for x (reminding us that the last time an x was instantiated a was used to do it).
Cheating
If the program tells you to endorse (or deny) a formula, you have to do exactly that. If the program tells you to endorse a formula and you deny that formula, you are violating the rules! Actually, the widget may even wag a finger at you for doing that.
A Shortcut
When entering instantiations during the game, merely replace the question mark within the square brackets with your choice, then select and endorse the formula with its instantiations. For example, if the program writes
You should endorse G(x)[?/x,a/x]
for a ? that you choose. >
do not bother to rewrite the whole formula, or copy and paste it-- just replace the first question mark with your choice, b say, and select and endorse.