.nr PO 1i
.ND
.SH
Choice of logic
.PP
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 lattice order.
.PP
The FD logic is defined by the following set of axioms and rules:
.DS
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)
.DE
.PP
Logics B, DW, and TW are defined by the following:
.DS
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))
.DE
.PP
Finally, the stronger logics EW, C, T, E, R, CK, and S4 are defined by:
.DS
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)
.DE
.PP
Axiomatisations of fragments of these logics result by
selecting the axioms and rules which explicitly mention
the appropriate connectives.