MIU Explorer

compact

Rules:	1	2	3	4
Rules:	xI  xIU	Mx  Mxx	xIIIy  xUy	xUUy  xy

Back up

one

step

Restart

using axiom

MI

Click a red button!

MI





MIU

,

MII

,{},{}

Path: MI

change axiom:

4

Explore the MIU-system [1] by clicking the red buttons, each of which represents the creation of a new theorem of the system by applying a rule of inference to a previously found theorem. The main features of the display are (a) the list of rules for your reference; (b) the current theorem (framed in blue); and (c) the options possible by applying all rules in all possible ways, given as a list of four lists of red buttons.

For example, starting with

"MI"

, the options are

{{"MIU"},{"MII"},{},{}}

, meaning that the result is

"MIU"

if you apply rule 1,

"MII"

if rule 2, and no results from rules 3 and 4.

You choose a path through the system, starting with the axiom and deriving a sequence of theorems. Below the current options (the possible branches to follow) is displayed the path that led to this point, including the theorems generated and the rules applied. Buttons to back up one step and to restart from the beginning and a slider to choose a different starting axiom are provided. This Demonstration is a power tool for considering the MU-puzzle [1]: is it possible to generate the theorem

"MU"

from the axiom

"MI"

?