for questions or link request: module admin

Axioms of Propositional Calculus

name: propaxiom, module version: 1.00.00, rule version: 1.00.00, orignal: propaxiom, author of this module: Michael Meyling

Description

This module includes the axioms of propositional calculus. These axioms (together with some rules) allow the deduction of all theorems of propositional calculus. To learn about possible conclusions click through the following `.. used by..' list.
This 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:

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)


8. Rule Declaration
      modus ponens     (rule1)

For an explanation see Modus Ponens


9. Rule Declaration
      add axiom     (rule2)

For an explanation see Add Axiom


10. Rule Declaration
      add sentence     (rule3)

For an explanation see Add Sentence


11. Rule Declaration
      replace proposition variable     (rule4)

For an explanation see Replace Proposition Variable


12. Rule Declaration
      use abbreviation     (rule5)

For an explanation see Use Abbreviation


13. Rule Declaration
      reverse abbreviation     (rule6)

For an explanation see Reverse Abbreviation

This module is used by the following modules: