Proofs

Proofs in Russell are essentially a list of steps, which are equipped with the references to the appropriate assertions and premises. So, the example of proof of syl theorem:

proof of syl {
    step 1 : wff = thm a1i (hyp 2) |- ( ph → ( ps → ch ) ) ;;
    step 2 : wff = thm mpd (hyp 1, step 1) |- ( ph → ch ) ;;
    qed prop 1 = step 2 ;;
}

Each line of a proof is an expression (equipped with it's type - after the : token), the reference like thm mpd - reference to the theorem mpd, the list of references to the previously proved steps and premises like (hyp 1, step 1). The body of expression is between |- and ;; tokens. In the end of a proof there must be a string like qed prop 1 = step 2 ;; which states, that the first proposition of the proved theorem coincides with the step 2 of the proof. In case, when there are several proofs of the same assertion, it is possible to add a name to the proof between proof and of tokens.

Sometimes it is necessary to declare an inner variable in a proof: a variable, which doesn't occur in the statement of a theorem. Then such variable is declared inside a proof:

proof of dfbi1gb {
    var ch : wff, th : wff;;
    step 1 : wff = axm df-bi () |- ¬ ( ( ( ph ↔ ps ) → ¬ ( ( ph → ps ) → ¬ ( ps → ph ) ) ) → ¬ ( ¬ ( ( ph → ps ) → ¬ ( ps → ph ) ) → ( ph ↔ ps ) ) ) ;;
    step 2 : wff = axm ax-1 () |- ( ch → ( th → ch ) ) ;;
    ....
    step 17 : wff = axm ax-mp (step 1, step 16) |- ( ( ph ↔ ps ) ↔ ¬ ( ( ph → ps ) → ¬ ( ps → ph ) ) ) ;;
    qed prop 1 = step 17 ;;
}