vix.ing · top · new · best · stats · spec

Abstraction and Application in Adjunction

2001/11/06 by Kosta Došen, K. Dosen, Dosen, K.
Computer Science · Mathematics · #18A15 #18A40 #18D15 #Advanced Algebra and Logic #Category Theory (math.CT) #FOS: Mathematics #Logic (math.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #math.CT #math.LO #msc:18A15 #msc:18A40 #msc:18D15

paper · pdf · doi:10.48550/arxiv.math/0111061

15 pages

arxiv created 2001/11/06 · openalex publication_date 2001/11/06 · arxiv updated 2009/11/30 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

Abstract

The postulates of comprehension and extensionality in set theory are based on an inversion principle connecting set-theoretic abstraction and the property of having a member. An exactly analogous inversion principle connects functional abstraction and application to an argument in the postulates of the lambda calculus. Such an inversion principle arises also in two adjoint situations involving a cartesian closed category and its polynomial extension. Composing these two adjunctions, which stem from the deduction theorem of logic, produces the adjunction connecting product and exponentiation, i.e. conjunction and implication.

Related