Краткое руководство по теории топосов в 1200 страницах.

Да. Щас чуть точнее.

Два тома в одном файле.

Но читать её не рекомендую, там слишком МНОГО всего.

В алгебраической семантике нет никаких конструкций в стиле Тарского.

А кто seven sketches in composability читал? Я чего-то подзабил и думаю стоит ли возвращаться.

Про пучки и топосы я рекомендую книжку Мак Лейна и Мёрдика.

О, шикарная монография. Но это скорее справочник

Всё правильно, к "Слону" и стоит обращаться, как к справочнику.
Как книжка, по которой надо изучать топосы, она очень плохая (нихера не понятно).
Вот книжка Мак Лейна и Мёрдика, как раз, довольно хороша.

Тебе не кажется, что ты очень привязываешься к исторически-сформировавшимся делениям? Конечно теория топосов наследует инструменты теории моделей, но топос это скорее алгебраическое (и немного топологическое) явление

Модельная семантика работает так: есть метаязык, есть предметный язык. Предметный язык задаём рекурсивно в псевдограмматической нотации. Потом мы определяем фрейм в терминах множеств / топосов. Это о том, какие семантические понятия будут участвовать в используемой логике. Например, там будут возможные миры. Присоединяем к фрейму функцию валюации, это будет модель. Задаём отношения выполнения по Т-конвенции. Там используется терминология семантического вывода, что он выполняется для формулы тогда и только тогда, когда. Так строим для всех форм формул, затем рекурсивно для каждой формулы проходимся по этому -- в этом идея. Семантический вывод может быть "индексирован", например, по тем же самым возможным мирам. Это ограничивает то, где именно относительно фрейма мы что-то там вывели. Потом мы пишем, при каких условиях формула будет считаться логически валидной. Это тоже рекурсивно. Всё, модельная семантика готова.

Топологическая семантика существует отдельно, и она входит в ряды альтернативных.

Не вполне классический взгляд на теорию категорий.
В целом, неплохо и полезно. Примеры есть хорошие.

Вот здесь есть короткое введение в альтернативные семантики. У меня было где-то подробнее, но не важно.

В общем-то сразу видно, что это такое.

Ну это примитивно.
Модальная логика, это гораздо больше, чем булевы алгебры с операторами.
Квантали хоть бы ;-) Да или хоть локали-фреймы...

Ну вот алгебраическая семантика — это вот это вот. Мы говорим о классах каких-то там алгебр и вместо всех семантических понятий используем эти классы алгебр.

Сейчас ради полноты заскриню две другие альтернативные семантики в этом введении.