Is used by the following modules:
We only need the logical disjunction ("or") and the negation ("not"). The other operands will be defined by them. (It would be possible to use only one operator: "sheffer's or" or "sheffer's and".) At first we note an abbreviation that defines the implication:
1 Abbreviation
(@F0 Þ @F1) º (Ø@F0 Ú @F1) (impl)
This means that we could transform a part formula that matches the pattern on the left side into the right side and we could transform a part formula that matches the pattern on the right side into the formula on the left side.
The logical conjunction ("and") could be defined with de Morgan:
2 Abbreviation
(@F0 Ù @F1) º Ø(Ø@F0 Ú Ø@F1) (and)
This is still an abbreviation.
The logical equivalence is defined as usual:
3 Abbreviation
(@F1 Û @F2) º ((@F1 Þ @F2) Ù (@F2 Þ @F1)) (equi)
Now we come to the first axiom of propositional calculus. This axiom enables us to get rid of an unnecessary disjunction:
4 Axiom
((P Ú P) Þ P) (axiom1)
This expresses the "idempotence" of the disjunction.
Axiom of weakening:
5 Axiom
(P Þ (P Ú Q)) (axiom2)
If a proposition is true, any alternative may be added without making it false.
The commutativity of the disjunction is expressed with the third axiom:
6 Axiom
((P Ú Q) Þ (Q Ú P)) (axiom3)
The last axiom is:
7 Axiom
((P Þ Q) Þ ((A Ú P) Þ (A Ú Q))) (axiom4)