William Elliot wrote:
Since your draft isn't posted here, but there for your convenience, my
comments can not be put under your statements where they will be best
understood. Some tables weren't clear and you didn't define theorem.
For better scrutiny, post here where I can make comments instead of there
where comments aren't possible.
Theorems
These are expressions that are tautologies or truth-functionally true,
meaning that they are evaluated as T for every assignment of truth
values to the variables. Many systems employ the rule of necessitation,
in which if P is a theorem of the logic, []P can be introduced into a
proof. This can also be used here, because according to the truth
tables, []P is true for every tautology.
This is only a preliminary list: Other theorems will be added in future
versions. Also, a bare list without interpretation or commentary isn't
very interesting. More will be added later.
General theorems
These apply to propositions in general.
1} P == ~ ~P
Double negation
2} P == P v P
Idempotent law for v
3} P == P & P
Idempotent law for &
4} (P v Q) == (Q v P)
Commutative law for v
5} (P & Q) == (Q & P)
Commutative law for &
6} ((P v Q) v R) == (P v (Q v R))
Associative law for v
7} ((P & Q) & R) == (P & (Q & R))
Associative law for &
8} ((P v (Q & R) == ((P & Q) v (P & R))
Distributive law for v
9} ((P & (Q v R)) == ((P v Q) & (P v R))
Distributive law for &
10} ~(P v Q) == ~P & ~Q
de Morgan's law for v
11} ~(P & Q) == ~P v ~Q
de Morgan's law for &
12} P => P
13} (P => Q) == (~Q => ~P)
Contrapositive rule
14} (P & (P => Q)) => Q
Modus ponens
15} ((P => Q) & (Q => R)) => (Q => R)
Transitive rule of the strict conditional
16} ((P => Q) & (Q => P)) == (P == Q)
Strict biconditional equivalence
17} (P == P)
Reflexive law of equivalence
18} (P == Q) == (~P == ~Q)
Negation law of equivalence
19} (P == Q) => (Q == P)
Symmetric law of equivalence
20} ((P == Q) & (Q == R)) => (P == R)
Transitive law of equivalence
Modal theorems
21} []P => P
22} P => <>P
23} ~[]P == <>~P
24} ~<>P == []~P
25} [][]P == []P
26} <>[]P == []P
27} []<>P == <>P
28} <><>P == <>P
29} [](P v Q) == ([]P v []Q)
30} <>(P v Q) == (<>P v <>Q)
31} [](P & Q) == ([]P & []Q)
32} <>(P & Q) == (<>P & <>Q)
Other theorems
33} !P == !~P
34} ?P == ?~P
35} ~!P == ?P
36} ~?P == !P
37} ![]P
38} !<>P
39} !?P
40} !!P
41} []P v ~[]P
42}<>P v ~<>P
43} !P v ?P
44} <>(P v ~P)
45} ~[](P & ~P)
46} (P v ~P) == ~(P & ~P)
47} !P == []P v []~P
48} ?P == <>P & <>~P
49} ?P == ( P == ~P)
50} ?P == ?(P v ~P)
51} ?P == ?(P & ~P)