How does Lambda-calculus relate to mathematical logic and set theory?

File: 1446161981378.jpg (97KB, 640x640px) Image search: [Google]

97KB, 640x640px

The typed lambda calculus with [math]\to, \times, +[/math] and bottom type is the proof theory of intuitionistic logic, and the Church encoding is a model for the Nats (like the Von Neumann naturals)
All those terms have their own Wikipedia article.

>>7719806
traditionally, through the curry howard correspondence.

I think the more intuitive one is the curry howard lambek taken not just over CCCs, but rather over topoi (at least I usually imagine semantics are possible because there is a "truth object" - some "table" of truth values G such that maps A->G correspond to subobjects of A).

I believe that adding this puts a few more restrictions on the logic and calculus (martin lof?) But I really don't care that much because I never run into expressiveness issues.

But yeah, basically, curry howard lambek says exponentiating in a cartesian closed category is lambda abstraction is a function symbol etc.

>>7719922
after googling, I'm wrong. The jump to the traditional topos semantics is non trivial. However, the CHL and exponentiation example are true.

>>7719806
That picture made me laugh more than it should have.

>>7719836
Goddamn I want to suck her clavicle so hard.

How is Lambda calculus related to computation?

>>7720044
the lambda calculus is a model of computation

>>7720049
Please elaborate. I'm dumb so I don't get in what way it is a model of computation. Doesn't computation involve algorithms?

>>7720054
It's a way computers interpret functions.

>>7720044
It's was literally the first Turing complete language.
Did you even peak at the Wikipedia article before asking or are you just fishing for information dots.

>>7720054
You don't know what a model of computation is, that's the problem