<p>There is a really interesting approach to a set theory-like foundational system that I am rather fond of: Grue's <a href="http://www.diku.dk/~grue/">Map Theory</a>. The basic idea is to take the (untyped!) $\lambda$-calculus as a base foundation, and to represent a set $S$ as a term $f$ such that</p>

<p>$$ S=\{f(x)\mid x\in\Phi\}$$
where $\Phi$ represents the <em>well founded functions</em> ($x\neq\bot$ in the Scott semantics). It doesn't look like there is any proof assistant based on it though, so I have no idea how it would work in practice.</p>

CC BY-SA 3.0
2014-10-30T18:01:00.197Z
This sounds to be a great approach. I have lots of reading to do before I can ask my next question. Thank you!
JoeD
CC BY-SA 3.0
2014-10-27T18:07:01.043Z
2014-10-27T18:07:01.043Z
cody
<p>I am planning to implement in software a set theory language, based on a binary function, which in set theory is the so called adjunction operation: $f(x, y) = x \cup$ {y}. Therefore, a presentation of set theory in terms of lambda-calculus will really help. Are there such presentations or attempts to do it?   </p>

CC BY-SA 3.0
2014-10-27T01:28:25.840Z
If you look at denotational semantics they do this sort of thing all the time; or rather they use lambda terms where they mean set theoretic functions. This might not be what you are looking for however. 

It is also important to know what kind of set theory you are looking for. Lambda calculus is limited to the computable  but set theory in general is not. The set of lambda terms is countable so you can't possible define the set of reals with lambda calculus. So depending on your set theory lambda calculus may just not be powerful enough. Martin Lof type theory might offer an alternative.
Jake
CC BY-SA 3.0
2014-10-27T07:34:00.307Z
You are looking for Church's type theory, and what you're planning sounds like a toy version of the HOL proof assistant, which is based on Church's type theory. And this isn't research-level.
Andrej Bauer
CC BY-SA 3.0
2014-10-29T15:19:24.643Z
this seems like a similar query [A lambda calculus with arbitrary set primitives](http://lambda-the-ultimate.org/node/3992)
vzn
CC BY-SA 3.0
2014-10-29T15:24:29.727Z
maybe some leads in survey [Lambda-Calculus and Functional
Programming](http://people.uleth.ca/~jonathan.seldin/Article.pdf) / Seldin. eg see p26 "For some logicians, the interpreting of logic and set theory in combinatory logic or lambda-calculus was much less important than interpreting the type-free lambda-calculus in set theory."
vzn
<reference-request><lambda-calculus><set-theory>
Are there presentations of set theory in terms of lambda-calculus?
JoeD
# Are there presentations of set theory in terms of lambda-calculus?

(Asked by: username_0 on 2014-10-26)

I am planning to implement in software a set theory language, based on a binary function, which in set theory is the so called adjunction operation: $f(x, y) = x \cup$ {y}. Therefore, a presentation of set theory in terms of lambda-calculus will really help. Are there such presentations or attempts to do it?

**Tags:** reference-request, lambda-calculus, set-theory

> **Comments:**
> **username_1**: If you look at denotational semantics they do this sort of thing all the time; or rather they use lambda terms where they mean set theoretic functions. This might not be what you are looking for however.   It is also important to know what kind of set theory you are looking for. Lambda calculus is limited to the computable  but set theory in general is not. The set of lambda terms is countable so you can't possible define the set of reals with lambda calculus. So depending on your set theory lambda calculus may just not be powerful enough. Martin Lof type theory might offer an alternative.  
> **username_2**: You are looking for Church's type theory, and what you're planning sounds like a toy version of the HOL proof assistant, which is based on Church's type theory. And this isn't research-level.  
> **username_3**: this seems like a similar query [A lambda calculus with arbitrary set primitives](http://lambda-the-ultimate.org/node/3992)  
> **username_3**: maybe some leads in survey [Lambda-Calculus and Functional Programming](http://people.uleth.ca/~jonathan.seldin/Article.pdf) / Seldin. eg see p26 "For some logicians, the interpreting of logic and set theory in combinatory logic or lambda-calculus was much less important than interpreting the type-free lambda-calculus in set theory."  

---

## 1 answers

### Answer by username_4 on 2014-10-27. Score: 7

There is a really interesting approach to a set theory-like foundational system that I am rather fond of: Grue's [Map Theory](http://www.diku.dk/~grue/). The basic idea is to take the (untyped!) $\lambda$-calculus as a base foundation, and to represent a set $S$ as a term $f$ such that

$$ S=\{f(x)\mid x\in\Phi\}$$
where $\Phi$ represents the *well founded functions* ($x\neq\bot$ in the Scott semantics). It doesn't look like there is any proof assistant based on it though, so I have no idea how it would work in practice.

> **Comments:**
> **username_0**: This sounds to be a great approach. I have lots of reading to do before I can ask my next question. Thank you!  

---

