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.