Axioms and Theorems

The definition of an axiom or theorem in Russell is similar and follows the pattern of Assertion :

axiom ax-1 (ph : wff, ps : wff)  {
    prop 1 : wff = |- ( ph → ( ps → ph ) ) ;;
}
axiom ax-mp (ph : wff, ps : wff)  {  
    hyp 1 : wff = |- ph ;;
    hyp 2 : wff = |- ( ph → ps ) ;;
    -----------------------
    prop 1 : wff = |- ps ;;
}
theorem syl (ph : wff, ps : wff, ch : wff)  {
    hyp 1 : wff = |- ( ph → ps ) ;;
    hyp 2 : wff = |- ( ps → ch ) ;;
    -----------------------
    prop 1 : wff = |- ( ph → ch ) ;;
}

In the example there are two axioms of Hilbert-style propositional calculus and modus-ponens inference rule and syllogism theorem. Inference rules are marked with the same keyword axiom because substantially both - axioms and inference rules - are of axiomatic nature. Structurally, all assertions has following parts:

• a (possibly empty) list of premises, entitled with hyp keyword
• in case when there are premises - a horizontal bar -------------, which separates premises from propositions
• a (non empty) list of propositions, entitled with prop keyword

Each expression from premises and propositions lists has a type - it is placed right after the colon after the index of an entity, and a body, which lies between |- and ;; keywords. This expression must satisfy the grammar of its type. For example from above, all formulas satisfy the grammar of propositional calculus.

Note If there are several propositions in assertion, they are understood as a conjunction, not a disjunction.