MODULE (
  HEADER (
    SPEC (
      NAME ("lukaxiom"),
      VERSION ("1.00.00"),
      VERSION ("1.00.00"),
      LOCATIONS (
        LOCATION ("http://www.qedeq.org/0_00_53")
      )
    ),
    HEADLINE ("Axioms, Definitions and Rules of Propositional Calculus"),
    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. \par The primitive logical symbols are implication ('$\rightarrow$') and negation ('$\neg$'). The other operands will be defined by them. \par This file is part of the project `Hilbert II' see \href{http://www.qedeq.org/}{project homepage}."
    ),
    EMAIL ("module@qedeq.org"),
    AUTHORS (
      AUTHOR ("Franz Fritsche",EMAIL ("ff@qedeq.org")),
      AUTHOR ("Michael Meyling", EMAIL ("mime@qedeq.org"))
    )
  ),
  USEDBY (
    SPEC (
      NAME ("luktheo1"),
      VERSION ("1.00.00"),
      VERSION ("1.00.00"),
      LOCATIONS (
        LOCATION (".")
      )
    )
  ),
  PARAGRAPHS (
    PARAGRAPH (
      LABEL ("axiom1"),
      AXIOM (
        IMPL(PROP(1), IMPL(PROP(2), PROP(1)))
      )
    ),
    PARAGRAPH (
      LABEL ("axiom2"),
      AXIOM (
        IMPL(IMPL(PROP(1), IMPL(PROP(2), PROP(3))), IMPL(IMPL(PROP(1), PROP(2)), IMPL(PROP(1), PROP(3))))
      )
    ),
    PARAGRAPH (
      LABEL ("axiom3"),
      AXIOM (
        IMPL(IMPL(NOT(PROP(2)), NOT(PROP(1))), IMPL(PROP(1), PROP(2)))
      )
    ),
    PARAGRAPH (
      LABEL ("or"),
      ABBREVIATION (
        OR(FPATTERN(1), FPATTERN(2)),
        IMPL(NOT(FPATTERN(1)), FPATTERN(2))
      ),
      "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."
    ),
    PARAGRAPH (
      LABEL ("and"),
      ABBREVIATION (
        AND(FPATTERN(1), FPATTERN(2)),
        NOT(OR(NOT(FPATTERN(1)), NOT(FPATTERN(2))))
      )
    ),
    PARAGRAPH (
      LABEL ("equi"),
      ABBREVIATION (
        EQUI(FPATTERN(1), FPATTERN(2)),
        AND(IMPL(FPATTERN(1), FPATTERN(2)), IMPL(FPATTERN(2), FPATTERN(1)))
      )
    ),
    PARAGRAPH (
      LABEL ("rule1"),
      DECLARERULE (
        "MODUSPONENS", 
        "modus ponens"
      ),
      "For an explanation see \href{http://www.qedeq.org/0_00_53/rules_1.00.00.html#modusponens}{Modus Ponens} or \href{http://www.qedeq.org/0_00_53/rules_1.00.00.o.html#modusponens}{Modus Ponens (o)}"
    ),
    PARAGRAPH (
      LABEL ("rule2"),
      DECLARERULE (
        "ADDAXIOM", 
        "add axiom"
      ),
      "For an explanation see \href{http://www.qedeq.org/0_00_53/rules_1.00.00.html#addaxiom}{Add Axiom} or \href{http://www.qedeq.org/0_00_53/rules_1.00.00.o.html#addaxiom}{Add Axiom (o)}"
    ),
    PARAGRAPH (
      LABEL ("rule3"),
      DECLARERULE (
        "ADDSENTENCE", 
        "add sentence"
      ),
      "For an explanation see \href{http://www.qedeq.org/0_00_53/rules_1.00.00.html#addproposition}{Add Proposition} or \href{http://www.qedeq.org/0_00_53/rules_1.00.00.o.html#addproposition}{Add Proposition (o)}"
    ),
    PARAGRAPH (
      LABEL ("rule4"),
      DECLARERULE (
        "REPLACEPROP", 
        "replace proposition variable"
      ),
      "For an explanation see \href{http://www.qedeq.org/0_00_53/rules_1.00.00.html#replaceprop}{Replace Proposition Variable} or \href{http://www.qedeq.org/0_00_53/rules_1.00.00.o.html#replaceprop}{Replace Proposition Variable (o)}"
    ),
    PARAGRAPH (
      LABEL ("rule5"),
      DECLARERULE (
        "USEABBREVIATION", 
        "use abbreviation"
      ),
      "For an explanation see \href{http://www.qedeq.org/0_00_53/rules_1.00.00.html#useabbreviation}{Use Abbreviation} or \href{http://www.qedeq.org/0_00_53/rules_1.00.00.o.html#useabbreviation}{Use Abbreviation (o)}"
    ),
    PARAGRAPH (
      LABEL ("rule6"),
        DECLARERULE (
        "REVERSEABBREVIATION", 
        "reverse abbreviation"
      ),
      "For an explanation see \href{http://www.qedeq.org/0_00_53/rules_1.00.00.html#reverseabbreviation}{Reverse Abbreviation} or \href{http://www.qedeq.org/0_00_53/rules_1.00.00.o.html#reverseabbreviation}{Reverse Abbreviation (o)}"
    )
  )
)