Stack Exchange network consists of 183 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.
@provocateur Are you familiar with Curry-Howard? The idea of propositions as types comes from that. It's untypable in the simply typed lambda calculus (and some extensions that essentially introduce other "logical connectives" than ->). It's typable in other systems. I don't know about other's making the claim, I guess I didn't even consider it to be a claim and more of an observation. I'll put up an explanation a little later, although we're going to need to use $\beta$ reduction...
@provocateur The type of the Y combinator is the diagonalization lemma, the combinator Y itself is the proof of the lemma. That's not really a claim, that's the interpretation of the Curry-Howard isomorphism... What I'm claiming is about what Goedel might have meant and showing the relationship to type theory in case it's of interest.
