 Given a logical deduction system \(H\) and an arbitrary set of formulas \(X\), a formula \(a\) is deducible in \(H\) from \(X\) if there is a finite sequence of formulas any one of which belongs to \(X\) or is an axiom of \(H\) or is obtained from previous formulas in the sequence by one of the inference rules of \(H\). Such a sequence is a deduction (or proof) in \(H\) of \(a\) with premises or hypotheses in \(X\). Let \(Cn(X)\) be the set of formulas deducible in \(H\) from the formulas in \(X\) taken as premises or hypothesis. This set is called the set of consequences of \(X\) (relative to the logical deduction system \(H\)). \(Cn\) is then an operation that is applied to sets of formulas to obtain new sets of formulas. It has the following properties: For every set of formulas \(X\)