JOINING RULE: If x and y are theorems, then < x∧y> is a theorem. SEPARATION RULE: If < x∧y> is a theorem, then both x and y are theorems. DOUBLE-TILDE RULE: The string '~~' can be deleted from any theorem can also be inserted into any theorem, provided that the result string is itself well-formed. FANTASY RULE: If y can be derived when x is assumed to be a theorem then < x⊃y> is a theorem. CARRY-OVER RULE: Inside a fantasy, any theorem from the "reality" c level higher can be brought in and used. RULE OF DETACHMENT: If x and < x⊃y> are both theorems, then y is a theorem. CONTRAPOSITIVE RULE: <x⊃y> and <~y⊃~x> are interchangeable DE MORGAN'S RULE: <~x∧~y> and ~< x∨y> are interchangeable. SWITCHEROO RULE: <x∨y> and <~x⊃y> are interchangeable