This html file is part of the project "Principia Mathematica II" see project homepage.
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:
Abbreviation 1
(@0 Þ @1) º (Ø@0 Ú @1)
(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:
Abbreviation 2
(@0 Ù @1) º Ø(Ø@0 Ú Ø@1) (and)
This is still an abbreviation.
The logical equivalence is defined as usual:
Abbreviation 3
(@1 Û @2) º ((@1 Þ @2) Ù (@2 Þ @1)) (equi)
Now we come to the first axiom of propositional calculus. This axiom enables us to get rid of an unnecessary disjunction:
Axiom 4
((P Ú P) Þ
P) (axiom1)
This expresses the "idempotence" of the disjunction.
Axiom of weakening:
Axiom 5
(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:
Axiom 6
((P Ú Q) Þ (Q Ú P)) (axiom3)
The last axiom is:
Axiom 7
((P Þ Q) Þ ((A Ú P) Þ (A Ú Q))) (axiom4)