🚀 go-pugleaf

     Actually, there are now several interesting type-free,
consistent, non-trivial set theories.  Gilmore's NaDSet (Journal
of Symbolic Logic 1986) is joined by the "map theory" by ??
(someone from Germany, sorry I've forgotten the name) in the
latest issue of Theoretical Computer Science, and a set theory
by Fairouz Kamareddine in Volume 1 Issue 1 of the new Journal of
Logic, Language and Information.

     Interestingly, the TCS writer and Kamareddine seem not to
have known about each other's work or Gilmore's, though they
refer to Aczel's papers on non-well-founded set theory, which in
turn refer to Gilmore's earlier work.

     All three papers refer to (and, basically, refute) Scott's
1975 paper "Combinators and Classes", which bemoaned the lack of
type-free set theories and implied that set theory was not a
suitable basis for theoretical computer science.  Any of the
three set theories looks like it would work OK as a basis.  (I
prefer Gilmore's for sentimental reasons and because it's simpler.)

     I wouldn't consider NF and its extensions to be really
"type-free" because they sneak type theory ideas in the back
door with the stratification condition.

--Jamie.
  jamie@cs.sfu.ca
"Every \item command in item_list must have an optional argument." LaTeX pg.168