N的推理规则(续一 →消去律 若「(a→),「a, →引入律 若「U{a}FB, 则厂a→ (→+)N ( ✜ ) → : Γ ` (α → β), Γ ` α, Γ ` β. (→ −) → : Γ ∪ {α} ` β, Γ ` α → β. (→ +) 8