91f:03111 03E99 03B30 03F99 68Q25 Friedman, H.(1-OHS); Flagg, R. C.(1-SME) A framework for measuring the complexity of mathematical concepts. (English) Adv. in Appl. Math. 11 (1990), no. 1, 1--34. _________________________________________________________________ This paper presents a system $\scr F\sb 0(\scr B)$ that is intended to allow practical computation of the complexity of mathematical concepts. $\scr F\sb 0(\scr B)$ is an untyped theory of sets and partial functions in a first-order free logic with equality and a description operator. Its language $\scr L\sb 0(\scr B)$ contains many primitive operations, such as $n$-tuples, lambda abstraction, comprehension terms, finite set and Cartesian product formation, and definition by cases. $\scr B$ denotes a set of "descriptive forms" that are patterns according to which new constants, functions, and predicates can be defined. After a rigorous presentation of the syntax of $\scr L\sb 0(\scr B)$, standard programming language procedures yield parsing and recognition algorithms. A precise semantics for $\scr L\sb 0(\scr B)$ is given, followed by a deductive system $\scr F\sb 0(\scr B)$ that is shown to be complete by means of a Henkin-style proof. Finally, the authors introduce the notions of definition sequence, definition dag (directed acyclic graph), and definition tree. On the basis of these notions, they promise that, in a future paper, they will develop measures of complexity of definitions that will make possible practical calculation of the complexity of concepts in a large part of current mathematical practice. Reviewed by E. Mendelson