Applet Help

Language help

The applet consists of three areas:

  • The input area at the top is the area where one enters a proposition. Move your mouse to this area and click. A blinking cursor will appear. Try entering some sentence of the formal language. When you have finished typing your proposition, either hit the Return key or click Accept. If your input was in error, you can restore the last content of the input area by clicking Reject. A small part of the input area provides for selecting the notation: Peano-Russell (Infix), strict, or Polish. Strict notation is the same as Peano-Russell notation except that it does not omit any brackets.
  • The big white area in the middle of the applet is the graphical output area. Here the applet will show the syntax tree of your proposition, its alpha graph or its Begriffsschrift graph as well as any evaluation.
  • The area at the bottom of the applet consists of many clickable buttons. By clicking any of them you tell the applet what to do. At this time, there are the following buttons:
  • Tree: The syntactical structure of the proposition entered is shown in the large graphical area. This is the default.
  • Alpha graph: The proposition is shown as a Peirce-style alpha graph. This function is only available if the selected logical system (see further below) supports the necessary syntactical operations.
  • Frege: shows the notation as presented by G. Frege in his book "Begriffsschrift".
  • DNF: shows the disjunctive normal form (DNF) of the proposition entered
  • step towards DNF
  • animated DNF: slowly constructs the DNF displaying every step of its operation.
  • CNF: shows the conjunctive normal form (CNF) of the proposition entered
  • step towards CNF
  • animated CNF: slowly constructs the CNF displaying every step of its operation
  • eliminate conditionals: constructs an equivalent proposition that doesn't contain any conditionals
  • atomic negations: constructs an equivalent proposition where only propositional variables are negated
  • optimize: performs some cheap syntactical optimizations.
  • user-defined: opens a window where the user may assign truth-values to all propositional variables occurring in the proposition. After closing the window, the user is shown the evaluation of the whole proposition and its sub-expressions
  • counter-example: the applet shows a counter-example to the proposition, i.e. an evaluation that falsifies the proposition
  • satisfy: the applet shows an evaluation under which the proposition happens to be true
  • first evaluation: shows the first evaluation
  • next evaluation: shows the next evaluation
  • animated evaluation: slowly shows the evaluation of the proposition and its sub-expressions under every possible assignment of truth-values to propositional variables occurring in the proposition
  • reset: resets the evaluation last shown One button, normally labeled classic logic, has a special meaning: Here you can select the logical system you want to use. Besides classic logic, the applet supports several well-known non-classic, multi-valued systems and even an infinite-valued system. Note that not every button is available in every system. For example, the button truth table will be inaccessible if you choose an infinite-valued system.