epros, я похоже совсем чуть-чуть в свертке ошибся. Там не совсем любая формула
. Надо, чтобы она не содержала
в качестве свободной, как я понял.
Да, я в курсе, просто не стал заострять на этом внимание, как на не относящемся к делу.
Дело в том, что в исчислении предикатов есть правило для замены утвержения о конкретном
утверждением о "существовании такого
, что...". В исчислении предикатов второго порядка есть аналогичное правило и для предикатной переменной (
). С помощью этого правила как раз выводится это утверждение. Если при выводе формула, в которой производится замена, будет содержать свободную предикатную переменную
, то эта переменная тоже заменится и ничего интересного не получится. А вот если не будет содержать, то выведется это самое утверждение - "аксиома свёртки".
Так что да, это утверждение - общезначимое, но только для
, не содержащих свободной переменной
.
В той статье Википедии про арифметику второго порядка, которую Вы цитируете, есть некоторая некорректность, заключающаяся в том, что они пытаются описать аксиоматику теории отдельно от того, что уже есть в логике. На самом же деле арифметика второго порядка - это та же арифметика первого порядка, только в логике второго порядка.
А так, ну даже если мы забудем про это доп. условие. Формула, грубо говоря, сможет определить пустое множество. Я как-то не очень понимаю, почему это запрещено.
Это дополнительное условие никак не помешает вывести утверждение о существовании пустого множества.
И как-то больно круто выглядит, что она общезначимая...
Ну, дык, это логика второго порядка. Вот она такая.