A deductive system is structurally complete if its admissible inference rules are derivable. For several important systems, like modal logic S5, failure of structural completeness is caused only by the underivability of passive rules, i.e. rules that can not be applied to theorems of the system. Neglecting passive rules leads to the notion of almost structural completeness, that means, derivablity of admissible non-passive rules. Almost structural completeness for quasivarieties and varieties of general algebras is investigated here by purely algebraic means. The results apply to all algebraizable deductive systems.
Firstly, various characterizations of almost structurally complete quasivarieties are presented. Two of them are general: expressed with finitely presented algebras, and with subdirectly irreducible algebras. One is restricted to quasivarieties with finite model property and equationally definable principal relative congruences, where the condition is verifiable on finite subdirectly irreducible algebras.
Secondly, examples of almost structurally complete varieties are provided Particular emphasis is put on varieties of closure algebras, that are known to constitute adequate semantics for normal extensions of S4 modal logic. A certain infinite family of such almost structurally complete, but not structurally complete, varieties is constructed. Every variety from this family has a finitely presented unifiable algebra which does not embed into any free algebra for this variety. Hence unification in it is not unitary. This shows that almost structural completeness is strictly weaker than projective unification for varieties of closure algebras.
Yet another proof of Goedel's completeness theorem for first-order classical logic
给出了一阶经典逻辑关于直觉序列的Genzten演绎规则的极小集合（特别是缺失的截规则）的完备性的Henkin式证明.可满足性定理坚持对推导规则的保留，认为它需要比完备性定理更弱的假设，缺少的要求恰好是规则~ p --> p，这从经典的角度暗示了直觉主义的动机。一个裸露的治疗标准，基本的一阶语法不知何故更多的代数味道比平常也给。
Completeness and interpolation for intuitionistic infinitary predicate logic, in connection to finitizing the class of representable Heyting polyadic algebras
