


          Choice of logic

               You can choose logic by clicking on any of the  entries
          in  the  "logic:"  list.   This you can combine additionally
          with selecting any of the possible orders from the  "order:"
          list. The defaults are the FD logic and the distributed lat-
          tice order.

               The FD logic is defined by the following set of  axioms
          and rules:

                  FD Axioms:  1.  A -> A
                              2.  (A & B) -> A
                              3.  (A & B) -> B
                              4.  A -> (A v B)
                              5.  B -> (A v B)
                              6.  ~~A -> A
                              7.  F -> A
                              8.  A -> T

                  Rules:  1.       A -> B,  A  ==>  B
                          2.            A,  B  ==>  A & B
                          3.  A -> B,  B -> C  ==>  A -> C
                          4.  A -> B,  B -> A  ==>  (C -> A) -> (C -> B)
                          5.  A -> B,  B -> A  ==>  (B -> C) -> (A -> C)
                          6.  A -> B,  A -> C  ==>  A -> (B & C)
                          7.  A -> C,  B -> C  ==>  (A v B) -> C
                          8.          A -> ~B  ==>  B -> ~A
                          9.                A  ==>  t -> A
                         10.           t -> A  ==>  A
                         11.    A -> (B -> C)  ==>  (A o B) -> C
                         12.     (A o B) -> C  ==>  A -> (B -> C)


               Logics B, DW, and TW are defined by the following:

                  B  Axioms 1 - 8 as for FD.
                            9.   ((A -> B) & (A -> C)) -> (A -> (B & C))
                           10.   ((A -> C) & (B -> C)) -> ((A v B) -> C)

                     Rules 1 - 2, 8 - 12 as for FD.
                     Rules 6 and 7 replaced by the above axioms.
                     Rules 3 - 5 replaced by:

                           4'.   A -> B  ==>  (C -> A) -> (C -> B)
                           5'.   A -> B  ==>  (B -> C) -> (A -> C)

                  DW is B with rule 8 replaced by the axiom form:

                     Axiom 11.   (A -> ~B) -> (B -> ~A)

                  TW is DW with rules 4' and 5' replaced by the axiom forms:

                     Axiom 12.   (A -> B) -> ((C -> A) -> (C -> B))
                           13.   (A -> B) -> ((B -> C) -> (A -> C))


               Finally, the stronger logics EW, C, T, E, R, CK, and S4
          are defined by:

                  Axioms for the stronger logics are as follows:

                      EW  is  TW   plus   ((A -> A) -> B) -> B

                       C  is  TW   plus   A -> ((A -> B) -> B)

                       T  is  TW   plus   (A -> (A -> B)) -> (A -> B)

                                   and    (A -> ~A) -> ~A

                       E  is  T    plus   ((A -> A) -> B) -> B

                       R  is  C    plus   (A -> (A -> B)) -> (A -> B)

                      CK  is  C    plus   A -> (B -> A)

                      S4  is  E    plus   A -> (B -> B)


               Axiomatisations of fragments of these logics result  by
          selecting  the axioms and rules which explicitly mention the
          appropriate connectives.
