Cartesian closed logics, also known as simple type theories or simply-typed lambda calculi, are ubiquitous; we use sentential logic (WP, nLab) all the time in philosophy and law, and doxastic logic to reason about beliefs and social constructions. Surely, the models of these logics, known as Cartesian closed categories or CCCs (WP, nLab) exist; computer scientists and other mathematicians rely on them daily.
However, quantum information cannot be duplicated or deleted. This is in stark contrast to classical information: a computer can duplicate or delete a file, a lawyer can restate or drop an argument, a book can be copied or rot. Indeed, when it comes to physics, we usually want to talk about some sort of linear logic (WP, nLab) which conserves information: quantum logic (WP, nLab), stoichiometry, etc.
So, CCCs exist, but do they physically exist? Or do we merely interpret certain arrangements of physical symbols as models of Cartesian closed logic? (Or a third horn, perhaps?)
