# Do models of Cartesian closed logic physically exist?

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?)

• The answer is in your second paragraph: they do not physically exist. Also, what would it mean that a "logic" physically exists? Commented Mar 10, 2023 at 18:48
• @Frank: By "logic" I specifically mean syntax, which is already symbolic. Commented Mar 10, 2023 at 20:40
• The only way I can understand the question, "Does a logic physically exist?" would be to take it to mean, "Can we design and build a computing device that implements this logic in a direct way?" Most computers are classical computers. But we can also build quantum computers and analog computers. So all of these 'exist'. I'm not sure whether anyone has built a relevant computer. Commented Mar 10, 2023 at 20:41
• @Bumble: Ah, logics are not their models. A logic, or type theory, is syntax which describes a possible world; a model, or semantics, is a system whose behavior is (partially) described by the logic. Your typical CPU is not creating/destroying energy as it computes; it linearly transforms electricity to heat in a way which allows any permutation of logic gates -- including ones which happen to manipulate symbols according to the rules of any logic. We choose logic gates which constrain the possible permutations. Commented Mar 12, 2023 at 15:13