undefined | Better HN

0 pointssoist2y ago0 comments

The logic of toposes is higher order intuitionistic logic. The logic of higher toposes is presumed to be intensional dependent type theory. The best introduction to these logics is probably the homotopy type theory book.

0 comments

3 comments · 1 top-level

auggierose2y ago· 2 in thread

I cannot understand the homotopy type theory book. It just makes no sense to me, sorry.

> The logic of toposes is higher order intuitionistic logic.

Yes, I have read that a lot. Eventually, I would like to understand how toposes form a model of higher-order intuitionistic logic (which is what "The logic of toposes is higher order intuitionistic logic" probably means?). But first, I would like to understand what a topos is in first-order logic terms. You know, baby steps.

soistOP2y ago

The category of sets is a topos and can be expressed/presented with first order classical logic but the general logic of toposes is intuitionistic and non-classical. There is no single topos with a single logic, each topos has its own logic and the common thread is that they're non-classical and higher order.

auggierose2y ago

So are you saying that "T is a topos" cannot be expressed via first-order classical logic? Unlike something such as "G is a group", or "T is a topology" or "C is a category"?

1 more reply

j / k navigate · click thread line to collapse