This paper is divided into two parts. Part I provides a resumé of the evolution of the notion of predicativity. Part II describes our own work on the subject.

Part I

§1. Conceptions of sets. Statements about sets lie at the heart of most modern attempts to systematize all (or, at least, all known) mathematics. Technical and philosophical discussions concerning such systematizations and the underlying conceptions have thus occupied a considerable portion of the literature on the foundations of mathematics.

Let LIC be the implicational fragment of Dummett's LC, axiomatised by Bull in [1] by adding the axiom (L) CCCpqrCCCqprr to positive implication. The system which Bull in [2] calls OIC, i.e. positive implication plus (0) CCCCpqqrCCCpqrr, is contained in LIC (it is thesis 34 in [1], p. 193); but it does not contain it, as the following matrix (due to Bull)

verifies OIC but not (L) (CCC342CCC4322 = 2). Nor is (L) deducible in OIC supplemented by intuitionist axioms for negation, since the latter are all verified by the above matrix with Cp5 for Np.

I shall refer to the implicational fragment of intuitionist logic, and its extension with the further axiom

CCCCpqqrCCCpqrr

as IIC and OIC, respectively. The purpose of this paper is to apply a result due to Garrett Birkhoff to the extensions of IIC, and to the extensions of OIC in particular. The main result obtained is that every extension of OIC is characterised by finite models.