Чуть меньше оффтоп — вам строго говоря не нужна прям теория множеств, чтобы определить булеву алгебру на {0, 1}. В частности, чтобы поработать с {0, 1} вам не надо отвечать частным случаем какого более абстрактного объекта является {0, 1}, какие такие вообще объекты бывают, как они себя ведут, итд.

Я пытаюсь составить какую-то последовательность внятную или набор последовательностей в голове — последовательностей построения формальных теорий в математике. И я так думал, что в одной из таких последовательностей аксиоматические теории множеств идут за логиками первого и второго порядка, а правила вывода вообще из метатеории даются. А есть, возможно, какой-то способ начать с теории множеств и построить логику на ней?

В общем, меня эти паровозы путают. Кто из чего и что строит..

Такой последовательности нет — это самый простой ответ.

Вообще ни одной? Или только последней?)

В том виде о котором вы ведёте речь, если я вас правильно понял, то вообще ни одной. Вы ищите что-то вроде гильбертовской программы. А так каждое доказательство в математике это пример последовательности построения формальной теории. С чего-то начинаете, дальше выводите. С чего именно начинаете целиком зависит от того, в каком поле работаете.

А правила вывода?

Они ведь не определяются полем работы

Ну как сказать. Если только вы не работаете в традиции алгоритмических доказательств, вы вряд ли прямо выводите согласно четко заявленным правилам внутри доказательной системы. Подавляющее большинство математических доказательств не являются formal proofs. Вообще изучение всех этих proof calculus составляет самостоятельную область математики, а не даёт какую-то характеристику математики в целом. Естественно есть определённые связи между формальной теорией доказательств и доказательствами, но там всё не так просто, что вот мол мы установили последовательность как это делается. Там очень много тонкостей, насколько формальные системы доказательств работают и для чего, каких свойств они доказуемо не могут иметь, и так далее. Это целая отдельная специальная область, которую не стоит даже пытаться объяснять в пределах чата — но вам выше указания дали как раз в эту сторону. Если я правильно понимаю, что вы в это всё только вкатываетесь и для вас вновинку была идея представления логики функциями над {0, 1}, то проще всего сказать, что предполагаемая вами картина, что мы можем от и до красиво представить всю схему математики — не имеет места.

посмотрите первые две главы шульмановского труда

это собрано с мастера https://github.com/mikeshulman/catlog

он кстати еще работает над некоторыми главами насколько я знаю, т.е. книга не заброшена

Для меня в новинку скорее то, что иерархичность рассыпается, хотя раньше она казалась очевидной)

Спасибо, выглядит очень многообещающе

Для получения категорной семантики в смысле пруф-теоретической нужно всего лишь...

1. Взять аксиомы и правила вывода нужной логики;

2. Перевести всё в правила вывода в исчислении секвенций;

3. Syntactic consequence и горизонтальная линия будет стрелочкой, коннективы — аджойнтами, с кванторами посложнее, но там можно посмотреть ncatlab для необобщённых кванторов, например: https://ncatlab.org/nlab/show/existential+quantifier#categorical_semantics

выглядит как сигма и пи-типы

но насколько я понял, сигма-тип это не совсем то же самое, что квантор существования