Теорема об неопределимости предикатов в алгебре с некоторыми отношениями выдерживающей некоторые автоморфизмы, но не являющиеся автоморфизмами предикатов

Где FV – множество всех свободных переменных формулы А, а a1/v1 есть результат подстановки a1 вместо v1 в А.

Система аксиом арифметики Пеано.

S9 – принцип мат индукции

Аксиома индукции в системе Пеано.

Вывод коммутативности и ассоциативности сложения в системе Пеано.