The Friedman/Flagg paper

The Friedman/Flagg paper

[categories]

Date: Mon, 26 Jan 1998 19:16:12 -0500 (EST)
From: Peter Freyd <pjf@saul.cis.upenn.edu>

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