Near-equational and equational systems of logic for partial functions. II
WILLIAM LANE CRAIG · Journal of Symbolic Logic · 1989
For the reader's convenience, we begin Part II by restating the rules for constructing Sq derivations given in §2: We let R be the set of 14 rules for Sq, R* the set of pure *-rules in R, R≃ the set of pure ≃-rules in R, and R− the set R ∩ − {Exs≃}. The closure of any F ⊆ Sq under R will be denoted by csRF, and the direct image of F under Cut*, for example, by Cut*(F).