BOUNDED SET THEORY: Home Page

Bounded Set Theory (BST) is a weak version of the ordinary set theory. Its main feature is paying main attention to using bounded quantification (as in the ordinary everyday mathematical practice) and other analogous bounded constructs. The language of this set theory, called DELTA, allows to define both set-theoretic (bounded) formulas and operations. The main universe of sets for BST consists of hereditarily-finite sets and is called HF. However, the universe for Zermelo-Frenkel set theory does as well.

Moreover, it is considered also so called antifounded version of HF, called HFA, which satisfies finite version of Aczel's Antifoundation Axiom. Antifounded sets are also called hypersets. This correlates very happily with the concept of HyperText used for creating World-Wide Web (WWW)-pages with hyperlincs between them. Antifounded version of BST is called BSTA. There exists corresponding version of the language DELTA.

This language may be naturally interpreted as query language for nested databases with very arbitrary and flexible structure. Such kind of databases may be considered also as unstructured or semistructured ones. For the antifounded case this nested structure may be also cyclic. (Some cycles in the membership relation are possible.) We meet this kind of cyclic structure in the World-Wide Web. Therefore it seems most natural to interpret DELTA in this antifounded case as query language to WWW or to Web-like data bases (WDB), i.e. to databases possibly distributed between many computers organized as a set of ``pages'' like those in WWW which contain references to other pages. These references correspond to the ordinary set-theoretic membership relation between any set and its elements.

A key result demonstrating the expressive power of DELTA says that definability in DELTA exactly corresponds to computability over HFA (or over WWW or WDB) in Polynomial Time.

Also some version of DELTA corresponds to LOGSPACE-computability.

Here are some publications on BST available by WWW. Cf. also information on Computer Logic Laboratory where BST is worked out.

Here is a brief introduction to BST in its connection to WWW.

We also have a simple experimental implementation of BST on LISP with some illustrating examples.

An implementation of BST on Java as a query language to the real Web is in progress.


The work on BST is supported by RBRF (project 96-01-01717) and by INTAS (project 93-0972)

This page is constructed by Vladimir Sazonov (sazonov@logic.botik.ru).