This paper provides a semantic analysis of admissible rules and associated completeness conditions for arbitrary deductive systems, using the framework of abstract algebraic logic. Algebraizability is not assumed, so the meaning and significance of the principal notions vary with the level of the Leibniz hierarchy at which they are presented. As a case study of the resulting theory, the nonalgebraizable fragments of relevance logic are considered.

A principal type-scheme of a -term is the most general type-scheme for the term. The converse principal type-scheme theorem (J.R. Hindley, The principal typescheme of an object in combinatory logic, Trans. Amer. Math. Soc. 146 (1969) 29–60) states that every type-scheme of a combinatory term is a principal type-scheme of some combinatory term.This paper shows a simple proof for the theorem in -calculus, by constructing an algorithm which transforms a type assignment to a -term into a principal type assignment to (...) another -term that has the type as its principal type-scheme. The clearness of the algorithm is due to the characterization theorem of principal type-assignment figures. The algorithm is applicable to BCIW--terms as well. Thus a uniform proof is presented for the converse principal type-scheme theorem for general -terms and BCIW--terms. (shrink)