Границы выразимости

☀️ Логика первого и второго порядка: почему мы выбираем меньше?
Мы уже знакомы с кванторами (∀ и ∃), которые пробегают по элементам множества. Это логика первого порядка. Но что, если мы захотим сказать что-то о самих свойствах или множествах элементов?
Математическое ядро:
В логике первого порядка мы можем сказать: «Для каждого числа x существует число y, такое что y = x + 1». Мы квантифицируем по элементам (числам).
В логике второго порядка мы можем сказать: «Для каждого свойства P, если P(0) и P(n) влечет P(n+1), то P верно для всех чисел». Здесь мы квантифицируем по самим свойствам (множествам).
Логика второго порядка гораздо мощнее. В ней можно однозначно описать натуральные числа (с точностью до изоморфизма), чего нельзя сделать в первом порядке.
Зачем это нужно?
Так почему же математики используют в основном логику первого порядка? Ответ дал Гёдель. Его теорема о полноте работает только для первого порядка. Логика второго порядка слишком богата: в ней нет полного и эффективного механизма доказательств. Мы жертвуем выразительностью ради возможности строго доказывать теоремы.