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

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

Proof Hint ∶ Proof ∶ Proposition
∷
Untyped Term ∶ Typed Term ∶ Type

or

Proof Hint ∶ Untyped Term
∷
Proof ∶ Typed Term
∷
Proposition ∶ Type

See my working notes on the Propositions As Types Analogy —
• https://oeis.org/wiki/Propositions_As_Types_Analogy

#Mathematics #CategoryTheory #ProofTheory #TypeTheory
#Logic #Analogy #Isomorphism #PropositionalCalculus
#CombinatorCalculus #CombinatoryLogic #LambdaCalculus
#Peirce #LogicalGraphs #GraphTheory #RelationTheory

Survey of Precursors Of Category Theory
• https://inquiryintoinquiry.com/2023/04/03/survey-of-precursors-of-category-theory-3/

A few years ago I began a sketch on the “Precursors of Category Theory”, tracing the continuities of the category concept from Aristotle, to Kant and Peirce, through Hilbert and Ackermann, to contemporary mathematical practice. A Survey of resources on the topic is given below, still very rough and incomplete, but perhaps a few will find it of use.

#CategoryTheory #CombinatoryLogic #LambdaCalculus #RelationTheory
#Aristotle #Kant #Peirce #Schönfinkel #Hilbert #Ackermann #Carnap
#HaskellCurry #WilliamHoward #JoachimLambek #SaundersMacLane
#PropositionsAsTypesAnalogy #CurryHowardIsomorphism #Ulam

Propositions As Types Analogy • 1

Re: R.J. Lipton • Mathematical Tricks

One of my favorite mathematical tricks — it almost seems too tricky to be true — is the Propositions As Types Analogy.

And I see hints the 2‑part analogy can be extended to a 3‑part analogy, as follows.

See my working notes on the Propositions As Types Analogy for more information.

#Animata #CSPeirce #CombinatorCalculus #CombinatoryLogic #CurryHowardIsomorphism #GraphTheory #LambdaCalculus #Logic #LogicalGraphs #Mathematics #ProofTheory #PropositionsAsTypesAnalogy #TypeTheory