[FOM] Computational set thery

[Klaus Ebbe Grue]

Having followed "Computational set thery" I cannot resist making an announcement and then injecting some comments to the discussion.



Announcement

You can find a preliminary version of Chantal Berline and Klaus Grue: "A synthetic axiomatization of Map Theory" at http://www.diku.dk/~grue/papers/synthetic/

The paper has been submitted to Theoretical Computer Science and has been through one round of review.

What it is: Map Theory (MT) is type free lambda-calculus plus Hilberts epsilon operator. Like one of the reviewers said: "If we want to do computation in Map Theory then we can use the lambda-calculus.  If we want to do something uncomputable, like calculate an existential quantifier, we can do that too, using Epsilon."

The notions of sets and set membership are definable in MT, wellformed formulas of ZFC are expressible in MT, and all axioms and inference rules of ZFC are provable in MT. In consequence, all theorems of ZFC are provable in MT.

MT is provably consistent in ZFC plus the assumption that there exists a strongly inaccessible ordinal.

MT can be used for programming in the sense that you can download a compiler for the Lox programming language from www.lox.la and start hacking. The Lox programming language is Map Theory minus the epsilon operator plus some syntax for typing programs using a standard keyboard.

The paper on MT from 1992 had complex axioms and a complex model. A simpler model was published in 1997. The "synthetic" MT has simple axioms (I would say) and a simple model. The first version of the synthetic MT paper dates back to 1996, so it has taken i little while to simplify MT.



Comment injection:

Henk> Set theory is a very awkward theory to represent computations.

Arnon> Henk - this is simply not true. It is true that computational issues
Arnon> have not been a factor at the development of set theory and its
Arnon> use as the foundations of math - but this is does not
Arnon> mean that this is impossible in principle ...

I formally agree with Arnon but actually agree with Henk: Programming in ZFC is not impossible but indeed awkward. At least that was the motivation for making MT in the first place. Programming in MT minus epsilon is straightforward and making a compiler for MT minus epsilon can be used as a student project (making something like a compiler for the Lox language is a bit more than a student project).

Harvey> Can't we simply prove outright that all formalisms, including ZFC
Harvey> with abbreviation power, represent large computations awkwardly?

If you can accept MT as non-awkward, then MT is a counterexample to that conjecture.

Harvey> The standard way that people get convinced that an
Harvey> alternative foundation is sound, at least in the
Harvey> sense that it is internally consistent, is to interpret
Harvey> it in set theory, or a fragment of set theory. Does
Harvey> anybody object to this continued practice?

At least I do not object to that. I would rather consider ZFC to be the "gold standard" that anyone should compare to. If you make a foundation and you cannot simulate ZFC in it: forget it. If you make a foundation and cannot prove consistency in ZFC plus something: forget it. At least those were the guiding criteria for the development of MT.

Scott> there is only one satisfactory way of avoiding the
Scott> paradoxes: namely, the use of some form of the
Scott> theory of types...

I do not agree. The alternative is to use, well, kappa-Scott semantics. The Scott semantics most people know is the case where kappa is omega (the smallest infinite ordinal). But Scott was aware of kappa-Scott semantics (for regular ordinals kappa) from the beginning and wrote about them in German lecture notes which are probably lost now.

In MT I would say that e.g. Russells paradox is avoided in a satisfactory way. Russell applies the fixed point operator to the negation operator to get a truth value which equals its own negation. You can ask any computer to apply the fixed point operator to negation, and the computer will respond by looping indefinitely. And you can apply the fixed point operator to negation in MT, and you will get "bottom" where bottom is the minimal element of the kappa-Scott domain which models MT. I personally find that perfectly satisfactory.

In synthetic MT one can define a predicate psi(x) for which psi(x)=true iff x is "wellfounded". For wellfounded x you have nice properties like Tertium Non Datur (TND) and things like that. And bottom is not wellfounded, so you cannot call upon TND to get a paradox. Wellfounded x correspond to the sets of ZFC.

Cheers,
Klaus

PS: For an introduction to MT, I think Sections 1--4 of http://www.diku.dk/~grue/papers/synthetic/ is the best I can offer at present.