Game-theoretical Semantics: The Henkin-Hintikka Game

The Henkin-Hintikka Game: Endorse-Deny

[6/6/2008 10 Software Under development]

This contains a Java applet, so it will be slow loading and likely it will ask you about security.

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 Fa∧Fb is true you should think that Fa is true and that Fb is true (for then, and only then, is Fa∧Fb  true).

This insight lies behind the top-down approach of Model Theory Semantics (see, for example, John Sowa on Model Theory Semantics).

The applet will debate with you about these matters. The applet 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 applet.  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).

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 parrotted from the media or some 'authorities'). This game requires you to place your semantical views on a sound basis.

The software will reason with you in accordance with the following rules.  The way these rules are displayed on this page is as follows.  What you do (or what it actually does) is at the top, then underneath is what you (or it) should do next; sometimes underneath there is a choice in which case at least one of the two should be done. 'You' is you; and 'I' is the program. You play the game with the program by endorsing (or denying) a selection to start with; then you have to select and endorse (or deny) in accordance with what you should do.


When the applet 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)(Fx∧(∃y)Gy) which you endorse

You endorsed (∃x)(Fx∧(∃y)Gy)

You should endorse (Fx∧(∃y)Gy)[?/x]

for a ? that you choose.

and as the second move you endorse (Fx∧(∃y)Gy)[a/x] which leads to

You endorsed (Fx∧(∃y)Gy)[a/x]

I denied (∃y)Gy[a/x]

You should endorse Gy[?/y,a/x]

for a ? that you choose. >

notice that the formula (∃y)Gy does not even contain x; why then does the program tell you I denied (∃y)Gy[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)(Fx∧(∃x)Gx) and it would proceed


You endorsed (∃x)(Fx∧(∃x)Gx)

You should endorse (Fx∧(∃x)Gx)[?/x]

for a ? that you choose.

choosing a/x

You endorsed (Fx∧(∃x)Gx)[a/x]

I denied (∃x)Gx[a/x]

You should endorse Gx[?/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).


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!

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 Gx[?/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.

Endorse Applet

Your browser is not displaying the Deriver applet. Try downloading Deriver itself by clicking on the link elsewhere on the page.


There are a few formulas in the applet for you to try. But you can go further either by typing your own ones in or by editing the drawing (and thus changing the interpretation-- have a look at documentation on the drawing panel).