Я хотел бы разобраться, в чем смысл матлогики, зачем она нужна. Для меня этот предмет очень сложный, в первую очередь из-за того, что я не понимаю цели основных построений. Я первоначально думал, что матлогика нужна для большей строгости в рассуждениях в любой другой области математики. Но сейчас я этот вариант откинул. В самом деле, я вполне нормально себя чувствую, рассуждая обычным человеческим образом. Почему я должен в своих рассуждениях опираться на какой-то там язык первого порядка с какими-то аксиомами? Почему, например, язык не второго порядка? Или бесконечного порядка?
Вот мне, например, нравится сюжет про булевы функции, полные булевы базисы, нормальные формы, полиномы Жегалкина. Во-первых, сами объекты очень естественные, а во-вторых приятно, когда результаты из абстрактной алгебры находят конкретное применение к этим вещам. Но логика то тут при чем? Вроде бы самые обычные объекты дискретной математики, которые могли бы быть в одной книжке наряду с какими-нибудь перестановками, производящими функциями, факториалами и т.д.
Если бы матлогика была бы только о строгости математических доказательств, я бы наверное вообще не открывал бы ее даже. Проблема в том, что у меня есть
подозрение, что матлогика совсем о другом. Пример: Теорема Мальцева: Если квазиуниверсальная формула

истинна на подсистемах

, локально покрывающих алгебраическую систему

, то

истинна и на

. Я понимаю так, что эта теорема дает очень сильное достаточное условие истинности для огромного количества утверждений. Но здесь и речи нету ни о какой строгости математических рассуждений. Как было в обычной алгебре? Мы брали какой-то объект (например, группа), определяли для него какие-то понятия (например, подгруппа, смежный класс, нормальная подгруппа) и далее находили связи между этими понятиями (множества смежных классов по нормальной подгруппе совпадают). А здесь получается намного круче. Мы берем некоторый набор средств (формулы и термы из какой-то формальной системы), который как-то связан с нашим представлением об объектах целой предметной области (например, теории групп). Этот набор средств в некотором смысле хорош. Например, он обладает рекурсивной природой. А значит к нему можно применять индукцию по построению формул. Т.е. мы как бы работаем не в самой предметной области, а "над" ней. Получаем какие-то результаты о наших формальных конструкциях (формулах формальной теории) и интерпретируем их с точки зрения интересующей нас предметной области (теории групп). Так что ли?
Отдельно хотел бы узнать про роль матлогики в каких-нибудь обычных разделах математики типа матанализа. Я где-то здесь, на форуме видел про то, что в

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

зависят от таких эфемерных сущностей как большие кардиналы. Допустим, я вообще не знаю, что такое

и мыслю в рамках канторовской теории множеств. Получается, что я могу наткнуться на какие-то обычные вещи из матанализа, которые без матлогики никак не решаются?
В общем, помогите разобраться, о чем матлогика и что от нее стоит ожидать?