Lambda the Ultimate

Well, I'm not quite glad with the terminology.

ANY is not constructed in any way but primitive, just like {}.

From a mathematical point of view it is rather unsophisticated and one doesn't have to go through the history of Russel paradox avoidance and language surgery. It is not entirely necessary to fit it into an outdated research program.

Usually one doesn't talk about constructing new sets from {} using the union operator

A = {} ∪ {a,b,c,...}

because {} is just the union identity and doesn't add anything to our understanding of A.

It makes sense however to construct new sets from ANY using subtraction

B = ANY - {a,b,c,...}

Talking about characters and such stuff has motivational purposes because I can't see right now another use case.

I'd rather compare this with that non-standard analysis. In NSA a new symbol ϵ is introduced as a positive number that is smaller than any positive real. Even if one rejects this meaning as nonsensical it provides a good base for our intuition.

OK... well I'm still not sure quite what you're asking, or how much you already know.

If you just want to write a language which includes such a construct, you should find it easy.

It seemed you were concerned about ZF and paradoxes though.

If you want a simpler formalism to base this kind of semantics on there are of course Lattices, Boolean algebras, etc. Mathematicians have been talking about a Top object in these contexts for a long while. You don't need a whole Set theory to model them in, far from it, nor anything like the kind of cleverness required to introduce non-standard analysis.

there's virtually no reason I can think of base programming language semantics on the ZF formulation of set theory. ... Constructive theories are a much more natural fit when talking about computation

I can see why you'd not like ZF, as it doesn't embed an easy to work with model of computation. But as for reasons to work with a set based formalism rather than some constructive type theory:

1. The law of the excluded middle. It works, and things proven by contradiction tend to be true. There are occasionally things that are easier proved by contradiction.

2. Types as sets. It seems very appealing to be able to reason about "x:T" as a simple boolean proposition rather than having this as a special syntactic form.

3. Natural subtyping. Related to the previous, it's nice to be able to reason about subtypes (particularly refinement types) "for free".

4. Intuitive denotations. Maybe it's my math background, but the semantic underpinnings of a set based approach seem more intuitive. For this reason, the correctness of ZF seems more intuitive. If CIC didn't have a consistency proof grounded in set theory, I'm not sure I'd feel comfortable believing it.

I can see how to develop a nice programming language starting from a set-based formalism, but I confess I'm not an expert on constructive logic or the calculus of constructions. Maybe those are all foolish reasons not to like constructive type theories?

There are intuitionalistic and classical set theories, as well as intuitionalistic and classical Higher Order Logics. Neither classical nor constructive logics have monopolies on useful models of computation.

The canonical example is adding call/cc to the simply typed lambda calculus. This creates an axiomatization of classical logic from constructive logic.

The cool thing in this area is Laurent's LLP, which harmoniously integrates classical and constructive logic into a cohesive whole. And of course, everybody seems to be buzzing about Call-By-Push-Value these days...

I can sympathize. Due to some of the same background, I'm much more comfortable with (hyper-)sets than HOL, and for what little it's actually saying, I am more comfortable with HOL than any abstract kind of category theory. Although I am often amused by light-hearted trash-talking of category theory, I am actually rather agnostic about the differences at this point. I don't know enough to competently judge, and I am more interested in going deeper into HOL than ZF.

(Hmm... there is a humor page out there to the effect of 25 generic questions to derail a math talk or ask afterwards to hide the fact you didn't understand anything, but I can't seem to find it.)

Postscript: To clarify, I was mostly disagreeing with citylight's assertion that ZF wasn't a good choice for modelling semantics, and Matt's suggestion that the law of the excluded middle was an inherent advantage of set theory. The rest of Matt's post seemed alright, although I'm indifferent whether or not CIC's consistency proof in terms of ZF actually means that much to me, as only God can know that ZF is consistent. (Although I do believe in ZF, so it's a good sign.)

I'm also amused by light-hearted trash-talking of set theory, by the way. :-)

You missed the truly heavyweight reason to choose set theory: theories based on ZF have by far the strongest consequence relations, and by far the strongest consistency strengths (in terms of the Gödelian hierarchy). This means that if you use a ZF-based theory to reason about a programing —all things to do with the quality of the construction of your semantics being equal— you will be able to prove more things about the PL than in a weaker theory, say CIC.

Of course, you shouldn't think that finding the axioms of a theory intuitive provides much in the way of reason to think the theory consistent. Given a formal theory that sits high up in the hierarchy of consistency strengths, it follows we should have less confidence in its consistency that theories sitting lower down. And indeed, the most widely circulated reasons given for believing in the consistency of ZF are rather handwavy.

I'd guess that the semantic underpinnings of a set based approach seem more intuitive, not because they are well grounded, but because set theory can be used to reason about its own models in a way that unleashes its inferential power on its own semantics.

Postscript: As a biographical aside, I learnt axiomatic set theory long before I discovered structural proof theory.

[Ok, edited first paragraph: Initially posted somehow thinking CIC referred to simple calculus of constructions].

Why do you say CIC is weaker than ZFC? My understanding is that CIC and ZFC are essentially the same consistency strength - one can model the other if you're willing to just postulate bigger sets in ZFC or more universes in CIC.

Of course, you shouldn't think that finding the axioms of a theory intuitive provides much in the way of reason to think the theory consistent. Given a formal theory that sits high up in the hierarchy of consistency strengths, it follows we should have less confidence in its consistency that theories sitting lower down.

My point was that I have more a priori confidence in ZFC based on natural intuitions. If the only reason we trust the consistency of some formal system is because we have a ZFC proof of it's consistency, then I see ZFC as more foundational.

The paper you refer to (Werner 1997), provides a family of axioms to add to CIC that allow, essentially, a chain of extensions of CIC that can do something along the lines of classical set theoretic introspection on theories below them. You need the first such extension to interpret ZFC, the second to interpret ZFC plus the existence of an inaccessible cardinal, etc. CIC does not interpret ZFC. The paper provides bounds on consistency strength, but does not explicitly talk about them. Good call, btw, I enjoyed reading that paper.

I don't believe in `natural' intuitions in higher-order logic. If we really understood set theory, then we would be able to construct `natural' large cardinal axioms that could settle the continuum hypothesis. To be more explicit, except for the redundant axioms, ZFC is very much more than the sum of its parts:Fraenkel's comprehension axiom is very easily interpreted in a weak set theory that admits constructive models, but when put in combination with ZC has very radical and difficult to fathom implications for the structure of set theory.

If we can construct a model for a theory in ZFC, this provides a powerful sanity check for that theory. And since there is no particular reason to doubt the consistency of ZFC, then there is no particular reason to doubt the consistency of one's theory. But this does not provide the kind of well grounded consistency argument that justifies deep confidence in a theory, the way that, say, Gentzen's consistency proof for arithmetic is grounded in elementary combinatorial intuitions.

I should add that I do believe in the consistency of ZFC, but my reasons are rather intricate, and they justify a belief that is of a somewhat hypothetical nature.

The paper you refer to (Werner 1997)...

I had forgotten about needing to add a functional axiom of choice to CIC to do the ZFC encoding, but that makes good sense. The main take away I have from the paper is summarized in the abstract: "both hierarchies of logical formalisms interleave w.r.t. expressive power and thus are essentially equivalent."

If we really understood set theory, then we would be able to construct `natural' large cardinal axioms that could settle the continuum hypothesis.

Isn't that like saying that if we really understood the natural numbers, we could give an answer to the Goldbach conjecture?

I think Godel's result casts serious doubt on our being able to find a simple finitary proof of ZFC's consistency in the way that we have a simple proof for arithmetic. This seems reasonable to me though, as the objects ZFC is meant to model are not finitary.

If you can make the leap to accepting subsets of the naturals as objects, getting to higher cardinals shouldn't be a problem, and then you have an intuitive "model" of a fragment of ZFC. All of the "counterintuitive" results about set theory that I've come across (e.g. Löwenheim–Skolem) really aren't that counterintuitive once you've wrapped your head around them.

Somehow this discussion doesn't feel very LtUish...

"both hierarchies of logical formalisms interleave w.r.t. expressive power and thus are essentially equivalent."
Sure, but there is a big difference between CIC and its extensions: CIC is a constructive theory, in a somewhat strange sense, and its extensions are not. The behaviour of the hierarchy really doesn't tell us anything new about CIC: we already knew that it had models in ZFC.

Isn't that like saying that if we really understood the natural numbers, we could give an answer to the Goldbach conjecture?

In one sense yes, in another sense no. Our failure to prove the Goldbach conjecture shows how little we understand the distribution of the prime numbers, and that is a sense that we don't understand the natural numbers. But this is not a complaint about our axiomatisations: if Goldbach's conjecture is false, then the weakest theories of arithmetic suffice to show it, whilst Harvey Friedman informally polled a number of mathematicians, all of whom had some confidence that the conjecture could be settled within existing theories of arithmetic.

The Continuum Hypothesis is a different story. Wrestling with it goes back to Cantor's failed proof of it, right at the beginning of set theory, before Zermelo's first axiomatisation. The embedding of arithmetic in set theory is perfectly clear, but the embedding of analysis is trickier: can the continuum usefully be described using an uncountable set of cardinality lessthan the set of real numbers? There is no fact of the matter in those set theories we understand best, nor are there good candidates for LCAs that settle the matter.

I think Godel's result casts serious doubt on our being able to find a simple finitary proof of ZFC's consistency in the way that we have a simple proof for arithmetic.
"Finitary" is a distraction: we can't even prove first-order logic consistent with finitary methods. I disagree with your claim even if we raise the bar to mean combinatorial, since the result casts exactly the same doubt on relatively weak theories, such as Peano Arithmetic, that do have combinatorial consistency proofs. The results described at Wikipedia's Ordinal Analysis page give a glimmer of inslight into the problem: we can't find combinatorial bases for theories with more than the weakest second-order comprehension axioms.

then you have an intuitive "model" of a fragment of ZFC.
I'll try another tack on intuitive: intuitive is nice, because it means you can work with a theory. ZFC is intuitive, and I like how easy it is to find intuitive models for it and its many intuitive large cardinal axioms —besides the many LCAs I don't find intuitive— but this cornucopia of intuition does not provide me with one iota of confidence in the consistency of ZF set theory, just as it does not with the intuitive nature of Frege's inconsistent theory of the Grundgesetze.

Intuitiveness is an internal property of a theory. Confidence in the consistency of the theory needs to come from outside the theory.

Löwenheim–Skolem
It makes clear the important difference between what theories about uncountable structures purport to define, and what they actually do define. So ZFC aims to describe, among many other things, the uncountable set of functions Nat -> Nat, but only succeeds in describing the countable subset of functions that it can prove total.

Somehow this discussion doesn't feel very LtUish...

As the discussion drifts more to feelings and intuition, I concur. We can wind this down...

... and that is a sense that we don't understand the natural numbers. But this is not a complaint about our axiomatisations: ...

The former is the sense I meant, but of course Godel's incompleteness result provides an example of axioms for arithmetic failing in your other sense. I don't think there's anything we're disagreeing about here.

I disagree with your claim even if we raise the bar to mean combinatorial, since the result casts exactly the same doubt on relatively weak theories, such as Peano Arithmetic, that do have combinatorial consistency proofs.

Such a combinatorial consistency proof of the consistency of ZFC could not be formalized in ZFC, right?

Intuitiveness is an internal property of a theory. Confidence in the consistency of the theory needs to come from outside the theory.

This is the crux of our disagreement, but it may just be terminological. I'm not talking about intuitiveness as in, "wow, this iPod interface is intuitive" - I'm talking about intuitive correctness. For example, the Peano Arithmetic is consistent. And this fact is intuitively obvious, in the absence of any combinatorial consistency proof, because the theory is modeled by natural numbers. Every axiom and every inference rule correctly describes the naturals and the naturals exist, QED. While the infinite sets that are to model ZFC are not as concrete as the natural numbers, I think the intuitive correctness is still there.

[Edit: "Grundgesetze" isn't the system I thought it was, but AFAICT it suffers the standard problem with naive impredicativity of not considering that there may be non-termination of recursion in the valuation function for supposed boolean predicate expressions.]

[Löwenheim–Skolem...] So ZFC aims to describe, among many other things, the uncountable set of functions Nat -> Nat, but only succeeds in describing the countable subset of functions that it can prove total.

I don't like the way you've phrased this. ZFC successfully describes the uncountable set of the functions Nat->Nat, but it doesn't describe them completely and there are other different structures that it also describes.

Update: Private mail sent. Apologies as well if this was too off topic. I've also made a few edits for clarity.

There are two points that suggest a misunderstanding that I think are best taken to email, and one point, regarding intuitive correctness that is interesting enough to be conducted with some visibility, where I will summarise my view on my weblog, sooner or later.

I agree entirely with Ehud's point about clogging up the forum with conversations of interest to few, and apologise for having done just that.

I'd guess that the semantic underpinnings of a set based approach seem more intuitive, not because they are well grounded, but because set theory can be used to reason about its own models in a way that unleashes its inferential power on its own semantics.

Also, I'm not sure what you mean by this. ZFC seems very well grounded to me. Would you deny that it makes sense to consider an object such as "all subsets of the Natural numbers?" Or do you think that some axiom or inference rule doesn't capture our intuition of how such objects should behave?

Finally, I don't see what's special about the self-referential power of ZFC as compared to CIC, which can implement and prove things about an evaluator for itself (in a higher universe).

I'll try to find something in your biographical aside to argue against in another post :).

Also, I'm not sure what you mean by this. ZFC seems very well grounded to me.

Just to point out a potential communication error: it was not stated that set-based approach is not well grounded. Rather, it was stated that the benefits (regarding intuition) of set-based approach have cause based in something other than it being or not being well grounded (i.e. independent of it being well grounded).

... Can't say I agree one way or another. I suspect that what is 'intuitive' to us depends mostly upon our prior exposure and efforts to achieve those critical 'aha!' moments. I suspect that, for the uninitiated, simple ideas like recursion are often far more difficult to grok than more complex ideas constructed of simple parts we already understand (e.g. iteration).

Set theory is in some ways more complex than, say, Category theory. How many people here really grok Category theory? Is it less intuitive, or do we simply have less exposure? Related to that attack on the biographical aside you're putting off: Charles may find set approaches 'more intuitive' only because he learned them earlier and more thoroughly... though I suspect he stated this as a disclaimer.

Just to point out a potential communication error: it was not stated that set-based approach is not well grounded.

Thanks. You're right - I read too much into that.

Regarding intuition, I can't say much about what others should find intuitive or even what influenced my own intuition. I don't think I've seen an attempt to justify the existence of interesting categories based solely on intuitive first principles. Do you know of one?

I don't think I've seen an attempt to justify the existence of interesting categories based solely on intuitive first principles. Do you know of one?

I do not. On the other hand, I haven't a clue how "interesting category" might be defined, and I do not count myself among those who fully grok category theory. I have some difficulty getting my head around the various morphisms and topologies. The extent of my understanding is more limited to inductive and coinductive structure, folds and unfolds... the sort of minor take away from category theory traditionally applied in PLT.

Would you deny that it makes sense to consider an object such as "all subsets of the Natural numbers?"

No, but then again the mathematical structure is fantastically complex. Consider the Löwenheim–Skolem theorem: this tells us that every first- order theory has countable models, and so if a first-order theory is complete with respect to an uncountable structure, then that structure is uncountable in a degenerate way, such as in case for the set of all subsets of the natural numbers.

It is easy to trip over when one tries to grasp such complexity. Martin-Löf's intensional type theory without universes can reason about the type Nat -> {0,1}, in its unambitious way.

Or do you think that some axiom or inference rule doesn't capture our intuition of how such objects should behave?

Well, there are good intuitions, and there are bad intuitions, and it's not always easy to tell which are which. If I were to be flippant, I would point you to our financial crisis.

But more seriously, it's not that we can't have confidence in a small intuition in isolation, it is more that —to echo a point I made in my other point— we find it hard to keep track of what happens to intuitions in combination. And often what we write down when we try to formalise our ideas goes beyond our original intuition: this rather seems to be the case with both Frege's Axiom V, and Martin-Löf's original type theory.