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.