#Propositions As #Types • 1
• https://inquiryintoinquiry.com/2013/01/29/propositions-as-types-1/

One of my favorite mathematical tricks — it almost seems too tricky to be true — is the #PropositionsAsTypesAnalogy. And I see hints the 2-part analogy can be extended to a 3-part analogy, as follows.

\(\text{proof hint : proof : proposition :: untyped term : typed term : type}\)

See my notes on #PropositionsAsTypes for more.
• https://oeis.org/wiki/Propositions_As_Types_Analogy

#Logic #Combinators #ProofTheory #TypeTheory
#CurryHowardIsomorphism #LambdaCalculus