for questions or link request: module admin

Axioms, Definitions and Rules of Propositional Calculus

name: lukaxiom, module version: 1.00.00, rule version: 1.00.00, original: lukaxiom, authors of this module: Franz Fritsche, Michael Meyling

Description

This module includes the axioms of propositional calculus due to Lukasiewicz and Tarski. These axioms, together with some definitions and rules of derivations, allow the deduction of all valid formulas of propositional logic.
The primitive logical symbols are implication ('→') and negation ('¬'). The other operands will be defined by them.
This file is part of the project `Hilbert II' see project homepage.

Content

1. Axiom
      P → (Q → P)     (axiom1)


2. Axiom
      (P → (Q → A)) → ((P → Q) → (P → A))     (axiom2)


3. Axiom
      (¬Q → ¬P) → (P → Q)     (axiom3)


4. Abbreviation
      @F1 ∨ @F2 ≡ ¬@F1 → @F2     (or)

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.


5. Abbreviation
      @F1 ∧ @F2 ≡ ¬(¬@F1 ∨ ¬@F2)     (and)


6. Abbreviation
      @F1 ↔ @F2 ≡ (@F1 → @F2) ∧ (@F2 → @F1)     (equi)


7. Rule Declaration
      modus ponens     (rule1)

For an explanation see Modus Ponens or Modus Ponens (o)


8. Rule Declaration
      add axiom     (rule2)

For an explanation see Add Axiom or Add Axiom (o)


9. Rule Declaration
      add sentence     (rule3)

For an explanation see Add Proposition or Add Proposition (o)


10. Rule Declaration
      replace proposition variable     (rule4)

For an explanation see Replace Proposition Variable or Replace Proposition Variable (o)


11. Rule Declaration
      use abbreviation     (rule5)

For an explanation see Use Abbreviation or Use Abbreviation (o)


12. Rule Declaration
      reverse abbreviation     (rule6)

For an explanation see Reverse Abbreviation or Reverse Abbreviation (o)

Cross References

This document is used by the following documents: