2 ms·

> All formalisations of non-classical logic operate in the framework of first-order logic, in the sense that the informal meta-language in which the non-classic

by fmap 8y ago

> All formalisations of non-classical logic operate in the framework of first-order logic, in the sense that the informal meta-language in which the non-classical logics are explained in is traditional first-order logic What gave you this idea? It is frequently useful to work over different base logics to obtain models of non-classical logics. E.g., when you work in categorical logic you usually work over an intuitionistic logic which can then be interpreted in an arbitrary topos. This gives you the ability to internalize any constructions you do "on the outside". There is a large community of mathematicians fixated on classical first-order logic, but this is just because of tradition. For models of classical first-order set theory it just doesn't make much of a difference. This is not true of "all formalizations of non-classical logic".

YorkshireSeason 8y ago
> work over an intuitionistic logic Whoops, yes, you are right. That said, a lot of the development of category theory that I'm aware of, is taking place with set theory. Certainly the two books [1, 2] that I learnt category theory from do. But that was a while back, and it might be the case that this is different now, I have not kept up with this research direction. For example is there a full, unrestricted formalisation of category theory in HoTT? [1] J. Adamek, H. Herrlich, G. E. Strecker, Abstract and Concrete Categories: The Joy of Cats. [2] S. Mac Lane, Categories for the Working Mathematician.
- fmap 8y ago
  Textbooks are usually supposed to be accessible to a wide audience so it makes sense when discussing foundations to start from a (hopefully) familiar set theory. It's usually a trade-off, since you end up repeating yourself when it comes to "internalized" constructions. "Sketches of an Elephant" is a good example of a textbook that pretty much presents everything twice. Once in an ambient set theory and once internally. What I meant specifically is work such as the following: Internal Universes in Models of Homotopy Type Theory - https://arxiv.org/abs/1801.07664 which explicitly works in an extensional type theory with some axioms to simplify and generalize a complicated model construction. > For example is there a full, unrestricted formalisation of category theory in HoTT? You can formalize category theory in HoTT as presented in the book. This has some advantages over a presentation in extensional type theory or set theory (being able to work up-to equivalence) and some disadvantages (universes in categories have to be constructed explicitly, since the ambient universe is not truncated). In my opinion, it's not the case that one is strictly superior - in the end it always depends on what you want to do.

by fmap 8y ago

YorkshireSeason 8y ago

> work over an intuitionistic logic Whoops, yes, you are right. That said, a lot of the development of category theory that I'm aware of, is taking place with set theory. Certainly the two books [1, 2] that I learnt category theory from do. But that was a while back, and it might be the case that this is different now, I have not kept up with this research direction. For example is there a full, unrestricted formalisation of category theory in HoTT? [1] J. Adamek, H. Herrlich, G. E. Strecker, Abstract and Concrete Categories: The Joy of Cats. [2] S. Mac Lane, Categories for the Working Mathematician.

fmap 8y ago
Textbooks are usually supposed to be accessible to a wide audience so it makes sense when discussing foundations to start from a (hopefully) familiar set theory. It's usually a trade-off, since you end up repeating yourself when it comes to "internalized" constructions. "Sketches of an Elephant" is a good example of a textbook that pretty much presents everything twice. Once in an ambient set theory and once internally. What I meant specifically is work such as the following: Internal Universes in Models of Homotopy Type Theory - https://arxiv.org/abs/1801.07664 which explicitly works in an extensional type theory with some axioms to simplify and generalize a complicated model construction. > For example is there a full, unrestricted formalisation of category theory in HoTT? You can formalize category theory in HoTT as presented in the book. This has some advantages over a presentation in extensional type theory or set theory (being able to work up-to equivalence) and some disadvantages (universes in categories have to be constructed explicitly, since the ambient universe is not truncated). In my opinion, it's not the case that one is strictly superior - in the end it always depends on what you want to do.