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)