Algebraic aspects of deduction theorems (Q1087867)

The present paper contains an analysis of closure spaces associated with those sequential logics which admit various deduction theorems. For purely algebraic reasons it is convenient to view deduction theorems in a more general form: given a sentential logic C (identified with a structural consequence operation) in a sequential language \({\mathcal S}\), a quite arbitrary set P of formulas of \({\mathcal S}\) built up with at most two distinct sentential variables p and q is called a uniform deduction theorem scheme for C if it satisfies the following condition: for every set X of formulas of \({\mathcal S}\) and for any formulas \(\alpha\) and \(\beta\), \(\beta\in C(X\cup \{\alpha \})\) iff \(P(\alpha,\beta) \subseteq C(X)\). \([P(\alpha,\beta)\) denotes the set of formulas which result by the simultaneous substitution of \(\alpha\) for p and \(\beta\) for q in all formulas in P.] The above definition encompasses many particular formulations of theorems considered in the literature to be deduction theorems. Theorem 1.3 gives necessary and sufficient conditions for a logic to have a uniform deduction theorem scheme. Then, given a sentential logic C with a uniform deduction theorem scheme, the lattices of deductive filters on the algebras \({\mathcal A}\) similar to the language of C are investigated. It is shown that the join-semilattice of finitely generated \((=compact)\) deductive filters on each algebra \({\mathcal A}\) is dually Brouwerian. The crucial result of the paper - Theorem 2.11 - states that for a very wide class of logics the converse of the above result also holds. More specifically, if C is a standard logic for which there exists a set \(\Lambda(p,q)\) of sentential formulas build up with two variables such that \(\Lambda(p,p) \subseteq C(\emptyset)\) and \(q\in C(\Lambda (p,q)\cup \{p\})\) then C has a uniform deduction theorem scheme iff for every algebra \({\mathcal A}\) similar to the language of C, the join- semilattice of compact deductive filters on \({\mathcal A}\) is dually Brouwerian.