Я хотел бы разобраться, в чем смысл матлогики, зачем она нужна. Для меня этот предмет очень сложный, в первую очередь из-за того, что я не понимаю цели основных построений. Я первоначально думал, что матлогика нужна для большей строгости в рассуждениях в любой другой области математики. Но сейчас я этот вариант откинул. В самом деле, я вполне нормально себя чувствую, рассуждая обычным человеческим образом. Почему я должен в своих рассуждениях опираться на какой-то там язык первого порядка с какими-то аксиомами? Почему, например, язык не второго порядка? Или бесконечного порядка?
Вот мне, например, нравится сюжет про булевы функции, полные булевы базисы, нормальные формы, полиномы Жегалкина. Во-первых, сами объекты очень естественные, а во-вторых приятно, когда результаты из абстрактной алгебры находят конкретное применение к этим вещам. Но логика то тут при чем? Вроде бы самые обычные объекты дискретной математики, которые могли бы быть в одной книжке наряду с какими-нибудь перестановками, производящими функциями, факториалами и т.д.
Если бы матлогика была бы только о строгости математических доказательств, я бы наверное вообще не открывал бы ее даже. Проблема в том, что у меня есть
подозрение, что матлогика совсем о другом. Пример: Теорема Мальцева: Если квазиуниверсальная формула
![$\text{Ф}$ $\text{Ф}$](https://dxdy-02.korotkov.co.uk/f/d/f/7/df7cfa24f170ee9619cd1f785c7344b882.png)
истинна на подсистемах
![$A_i$ $A_i$](https://dxdy-01.korotkov.co.uk/f/4/e/b/4ebf880807deff5796460f39aea46f8082.png)
, локально покрывающих алгебраическую систему
![$A$ $A$](https://dxdy-02.korotkov.co.uk/f/5/3/d/53d147e7f3fe6e47ee05b88b166bd3f682.png)
, то
![$\text{Ф}$ $\text{Ф}$](https://dxdy-02.korotkov.co.uk/f/d/f/7/df7cfa24f170ee9619cd1f785c7344b882.png)
истинна и на
![$A$ $A$](https://dxdy-02.korotkov.co.uk/f/5/3/d/53d147e7f3fe6e47ee05b88b166bd3f682.png)
. Я понимаю так, что эта теорема дает очень сильное достаточное условие истинности для огромного количества утверждений. Но здесь и речи нету ни о какой строгости математических рассуждений. Как было в обычной алгебре? Мы брали какой-то объект (например, группа), определяли для него какие-то понятия (например, подгруппа, смежный класс, нормальная подгруппа) и далее находили связи между этими понятиями (множества смежных классов по нормальной подгруппе совпадают). А здесь получается намного круче. Мы берем некоторый набор средств (формулы и термы из какой-то формальной системы), который как-то связан с нашим представлением об объектах целой предметной области (например, теории групп). Этот набор средств в некотором смысле хорош. Например, он обладает рекурсивной природой. А значит к нему можно применять индукцию по построению формул. Т.е. мы как бы работаем не в самой предметной области, а "над" ней. Получаем какие-то результаты о наших формальных конструкциях (формулах формальной теории) и интерпретируем их с точки зрения интересующей нас предметной области (теории групп). Так что ли?
Отдельно хотел бы узнать про роль матлогики в каких-нибудь обычных разделах математики типа матанализа. Я где-то здесь, на форуме видел про то, что в
![$ZFC$ $ZFC$](https://dxdy-03.korotkov.co.uk/f/2/0/0/2008136f873069a865a4ab1c0ddc03c082.png)
неразрешим вопрос о мере, которая сигма аддитивна и относительно нее измеримо множество Витали. А якобы если добавить аксиому существования какого-то большого кардинала, то станет разрешим. Для меня это все какой-то нонсенс, что вещи из обычного
![$\mathbb{R}$ $\mathbb{R}$](https://dxdy-04.korotkov.co.uk/f/f/3/e/f3e711926cecfed3003f9ae341f3d92b82.png)
зависят от таких эфемерных сущностей как большие кардиналы. Допустим, я вообще не знаю, что такое
![$ZFC$ $ZFC$](https://dxdy-03.korotkov.co.uk/f/2/0/0/2008136f873069a865a4ab1c0ddc03c082.png)
и мыслю в рамках канторовской теории множеств. Получается, что я могу наткнуться на какие-то обычные вещи из матанализа, которые без матлогики никак не решаются?
В общем, помогите разобраться, о чем матлогика и что от нее стоит ожидать?