This machine (version 0.01, 06/99) has been made by © Jan Jaspars in honor of Johan van Benthem at the occasion of his 50th birthday.
Instruction can be found at the bottom of this page.

     
     
1 2 << worlds>> 3 4












       












  
                 

 


Instructions

Make a model, specify a formula and let the machine do the evaluation!

Creating Models

A model can be made by clicking the buttons on the upper righthand part of the 'dashboard'. The management of possible worlds is divided into four different columns (four worlds is the maximum). Click +x in column number x and world x appears on the screen (model), click -x in column x and world x disappears again.

Every world contains the evaluation of two propostional variables p and q. The machine takes those propositions to be false, but they can be made true by the user by clicking p and/or q, respectively. This is made visible on the screen by changing colors of the variables: green = true, red = false.

A world y can be made accessible from a world x by clicking >y in column x. Tired of creating worlds? Let the machine do it for you. A model can be generated by clicking random model. Unhappy with the chosen model? Click clear model, and repeat.

Partial random generation is also possible. If you have a set of worlds in your model, then you can let the machine decide on the truth-value assignments by clicking the upper random button. The second randombutton (yellow background) picks an arbitrary accessibility configuration. Clearing the accessibility is also possible.

Writing formulas Specifying a formula can be done by the buttons in the lowest part. The formula appears step by step on the lower longer screen. A faster way of writing a formula is to specify in the text window by using your keyboard: B = box, D = diamond, & = conjunction, v = disjunction, - = negation, > = implication, = = equivalence. Put the formula on the display by clicking PUT. Evaluation of the formula can then be accomplished by clicking ENT. A small flashing light at every world's horizont appears. The color indicates the truth-value at the given world: green = true, red = false.

Modifying formulas and models A formula can be replaced by clicking CLR and filling in a new formula. Backward deletion step by step is possible by clicking DEL.
A model can be modified by adding worlds, choosing new truth-value assignments for p and q or a new accessibility relation. Remember that after modifications, a new evaluation takes another click on ENT.