§1.2 How to use the program ``Tarski''

Installing the program ``Tarski''. Download the source file from http://www.di.unito.it/~stefano/Mathematica-TarskiGames.nb. You need Mathematica interpreter of Wolfram co. to install it. Open the file, select the title: ``A program implementing ...'', then press Shift+Enter and wait a few seconds.

Calling the program ``Tarski''. The program is started by executing (i.e., by copying into a free location, then pressing Shift+Enter):

    Tarski[Formula, Arg1, Arg2, ... ]

What ``Tarski'' does. You can play a Tarski game for a given formula, drawing each position in tree form.

Input form for formulas. Variables, terms, and atomic formulas are written between "...", for instance: "x", y", "x<y". Compound formulas are written using the operators: Conj[A,B], Disj[A,B], Impl[A,B], Neg[A], Un["x",A], Ex["x",A], denoting A∧B, A∨B, A→B, ¬A, ∀x.A, ∃x.A. For instance, ∀x.∃y.(x<y) becomes Un["x",Ex["y","x<y"]]. If F is in input form, you can recover the usual syntax for F executing Lin[F].

An example. Copy in a new location, then execute (by Shif+Enter) all the following expressions:

    (* A formula in input form *)
    F20 = Disj[Conj["A","B"],Disj[Conj["A",Neg["B"]],Conj[Neg["A"],"B"]]];

    (* The same formula in the usual syntax: (A∧B)∨((A∧¬B)∨(¬A∧B)) *)
    Lin[F20]

    (* Calling the program ``Tarski'' *)
    Tarski[F20];

Graphic Parameters. An extra argument can be a strings: par1, par2, par3=n, ..., where par1, par2, par3, ... are graphic parameters. If a parameter is not assigned, it is taken with the previous value. Some graphic parameters are: FontSize=... (say: 12,14,18, ..), for Font size; TreeWidth=... (in pixels), for the width of the tree-like picture of the play. LevelHeight=... (height in pixels of each level of the tree-like picture).
An example. Copy in a new location, then execute (by Shif+Enter):

    Tarski[F20,"FontSize=14,TreeWidth=500, LevelHeight=35"]

How the play runs. ``Tarski'' asks the player who should move next for a move. The player can answer with the following moves:
  1.``Left'' or``Right'', for selecting the left- or right-hand side of a judgement of the form: t.A∧B, t.A∨B, t.A⇒B, or: f.A∧B, f.A∨B, f.A⇒B;  
  2.``Negation'', to select the only subjudgement of a negation t.¬A or f.¬A;
  3. ``Atom'' for the only subformula of an atom t.a or f.a (the subformula is: t.T or f.T if a is true, it is: t.F or f.F, if is a is false);
  4. t (a closed term of the language) for selecting the instance t.A[t/x] or f.A[t/x] of a quantification t.∀x.A, t.∃x.A, or f.∀x.A, f.∃x.A.
The current node can be an atomic formula A whose truth value is open (because there are free variables, or undefined constants). In this case, the program asks the player moving next for the truth value of A. The player should provide it in a consistent way.

Saved plays. An argument can be also a saved play, in matrix form,for instance:

In[356]:=

The matrix includes moves and the truth assignment for the atom B. Saved played in matrix form are available whenever a play ends. We can delete any number of lines at the end, save just an initial part of the play, then re-play only the initial part. For instance, copy in a new location,then execute (Shif+Enter) all expressions below:

    
    
    Tarski[F20,"FontSize=14,TreeWidth=500, LevelHeight=35", savedplay]

Created by Mathematica  (October 17, 2006)