4 ms·

Question about a claim in the article: "If classical logic is based on set theory, intuitionistic logic is based on category theory and its related theories."

Question about a claim in the article: "If classical logic is based on set theory, intuitionistic logic is based on category theory and its related theories." I'm no expert, but as I understood it, category theory can be used to construct a semantics for certain constructive logics, such as type theory, but to claim that intuitionistic logic is "based on" category theory seems off. A logic can exist all by itself, regardless of which theory is used to give semantics for it. Right?

Koshkin 5y ago
Well, “classical logic is based on set theory” seems off too… In fact, a theory can always be formulated using a minimum number of axioms, so none requires some other theory as its base. For example, the system of real numbers can be built starting from the natural numbers, but what this achieves is, this just gives a “proof of existence” of the reals, i.e of consistency of the definition of the reals as a complete ordered field.
foldr 5y ago
Yes, this seems completely off to me too. It’s perhaps worth noting in this connection that intuitionistic logics predate anything that could reasonably be called “category theory”.
boris_m 5y ago
Author here. Yes. Texts says "If classical logic is based on set theory", that is I am comparing the relations to set theory and category theory to that between classical logic and intuitionistic logic. I will try to fix the ambiguity.
- boris_m 5y ago
  Corrected the sentence: "If we view classical logic as based on set theory, then intuitionistic logic would be based on category theory and its related theories." And regarding the fact that CT is not "needed" for algebraic logic what I say is "category theory and its related theories." where I consider orders related to categories.
Ericson2314 5y ago
Orthodox Set theory is a "standard library" for classical logic. It just so happens that the people who like one tend to like the other, and so explorations of the semantics of classical logic (mostly, model theory) use Set theory. The Tarski-style algebrization of logic which is "logics as orders" stuff from this article is an alternative to that one can do without category theory. Heyting algebra vs boolean algebra is sufficient to distinguish classical and intuitionistic logic. Category theory is this not necessary for intuitionism, but is nicer, because the point is to compute things. Otherwise we just speak abstractly of what can be computed, which is like a pessimist compromise between realism and idealism. So Logic : order :: type theory : category Roughly, and the right side makes intuitionism a lot more exciting and applicable.

Koshkin 5y ago

Well, “classical logic is based on set theory” seems off too… In fact, a theory can always be formulated using a minimum number of axioms, so none requires some other theory as its base. For example, the system of real numbers can be built starting from the natural numbers, but what this achieves is, this just gives a “proof of existence” of the reals, i.e of consistency of the definition of the reals as a complete ordered field.

foldr 5y ago

Yes, this seems completely off to me too. It’s perhaps worth noting in this connection that intuitionistic logics predate anything that could reasonably be called “category theory”.

boris_m 5y ago

Author here. Yes. Texts says "If classical logic is based on set theory", that is I am comparing the relations to set theory and category theory to that between classical logic and intuitionistic logic. I will try to fix the ambiguity.

boris_m 5y ago
Corrected the sentence: "If we view classical logic as based on set theory, then intuitionistic logic would be based on category theory and its related theories." And regarding the fact that CT is not "needed" for algebraic logic what I say is "category theory and its related theories." where I consider orders related to categories.

Ericson2314 5y ago

Orthodox Set theory is a "standard library" for classical logic. It just so happens that the people who like one tend to like the other, and so explorations of the semantics of classical logic (mostly, model theory) use Set theory. The Tarski-style algebrization of logic which is "logics as orders" stuff from this article is an alternative to that one can do without category theory. Heyting algebra vs boolean algebra is sufficient to distinguish classical and intuitionistic logic. Category theory is this not necessary for intuitionism, but is nicer, because the point is to compute things. Otherwise we just speak abstractly of what can be computed, which is like a pessimist compromise between realism and idealism. So Logic : order :: type theory : category Roughly, and the right side makes intuitionism a lot more exciting and applicable.