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?
4
-
2$\begingroup$ 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. $\endgroup$– JakeOct 27, 2014 at 1:28
-
3$\begingroup$ 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. $\endgroup$– Andrej BauerOct 27, 2014 at 7:34
-
1$\begingroup$ this seems like a similar query A lambda calculus with arbitrary set primitives $\endgroup$– vznOct 29, 2014 at 15:19
-
$\begingroup$ maybe some leads in survey Lambda-Calculus and Functional Programming / 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." $\endgroup$– vznOct 29, 2014 at 15:24
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
1
There is a really interesting approach to a set theory-like foundational system that I am rather fond of: Grue's Map Theory. 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.
-
$\begingroup$ This sounds to be a great approach. I have lots of reading to do before I can ask my next question. Thank you! $\endgroup$– JoeDOct 30, 2014 at 18:01