![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
ADJOINTNESS IN FOUNDATIONS
May. 13th, 2020 11:01 pmhttp://www.tac.mta.ca/tac/reprints/articles/16/tr16.pdf
ADJOINTNESS IN FOUNDATIONS
F. WILLIAM LAWVERE
One of the aims of this paper is to give evidence for the universality of the concept of adjointness, which was first isolated and named in the conceptual sphere of category theory, but which also seems to pervade logic. Specifically, we describe in section III the notion of cartesian closed category, which appears to be the appropriate abstract structure for making explicit the known analogy (sometimes exploited in proof theory) between the theory of functionality and propositional logic. The structure of a cartesian closed category is entirely given by adjointness, as is the structure of a “hyperdoctrine”, which includes quantification as well. Precisely analogous “quantifiers” occur in realms of mathematics normally considered far removed from the province of logic or proof theory.
ADJOINTNESS IN FOUNDATIONS
F. WILLIAM LAWVERE
One of the aims of this paper is to give evidence for the universality of the concept of adjointness, which was first isolated and named in the conceptual sphere of category theory, but which also seems to pervade logic. Specifically, we describe in section III the notion of cartesian closed category, which appears to be the appropriate abstract structure for making explicit the known analogy (sometimes exploited in proof theory) between the theory of functionality and propositional logic. The structure of a cartesian closed category is entirely given by adjointness, as is the structure of a “hyperdoctrine”, which includes quantification as well. Precisely analogous “quantifiers” occur in realms of mathematics normally considered far removed from the province of logic or proof theory.
