User loginNavigation 
A lambda calculus with arbitrary set primitivesFor various reasons, I am looking for (or looking to develop) a lambda calculus and a semantics that I can use to structure settheoretic calculations. In other words, I want to be able to write things like (setfilter p A), which returns the subset of A for which p is true, even when A is uncountable. I don't need to write setfilter in this lambda calculus, but I want to include it as a primitive operation (along with membership, cartesian product, etc.), and wellfounded sets as primitive values. My main question: am I going to run into foundational problems, specifically with the ZF axioms? Has someone already tried this and written about it? I'm not concerned with whether the sets or set operations are computable. I'm not concerned with mathematical foundations, except for the possibility that they might pose difficulties. Having types isn't necessary, and neither is having every lambda denote a settheoretic function. It doesn't matter whether any given set can be expressed in a finite or even countable number of symbols. I don't need to use only a minimal collection of primitives. (In fact, I'd be nice if I could import them on a whim.) I want to use the syntax and structure of the lambda calculus, especially lambda abstraction, to express calculations that a particular group of applied mathematicians is interested in. After that, I can consider what subclass of these calculations is computable  but limiting the language to computable calculations right away feels like premature optimization. It seems easy to do. I'm asking because I found a subtlety in a related lambda calculus + semantics, and there might be more. If someone has found them already, I'd like to know. (The subtlety, which I half expected, came up when trying to interpret (lambda x in A . e) as a settheoretic function; i.e. as the set of points in its graph. The simple rule I wrote requires unrestricted comprehension when an enclosing lambda is applied to itself. Denotational semantics provides a solution, but I don't want that kind of complexity. I also decided I didn't need to interpret certain lambda forms as settheoretic functions, either, if it would make things simpler.) By Neil Toronto at 20100624 23:32  LtU Forum  previous forum topic  next forum topic  other blogs  5130 reads

Browse archivesActive forum topics 
Recent comments
3 days 19 hours ago
1 week 4 days ago
2 weeks 3 hours ago
2 weeks 3 hours ago
2 weeks 3 hours ago
2 weeks 4 hours ago
2 weeks 4 hours ago
2 weeks 6 hours ago
2 weeks 10 hours ago
2 weeks 12 hours ago