В математической логике схема аксиом (множественное число: схемы аксиом или схемы аксиом ) обобщает понятие аксиомы .
Схема аксиомы — это формула на метаязыке аксиоматической системы , в которой появляется одна или несколько схематических переменных . Эти переменные, которые являются металингвистическими конструкциями, обозначают любой термин или подформулу системы, которые могут или не могут быть необходимы для удовлетворения определенных условий. Часто такие условия требуют, чтобы определенные переменные были свободными или чтобы определенные переменные не появлялись в подформуле или термине [ требуется ссылка ] .
Учитывая, что число возможных подформул или терминов, которые могут быть вставлены вместо схематической переменной, бесконечно, схема аксиом обозначает бесконечный класс или набор аксиом. Этот набор часто может быть определен рекурсивно . Теория, которая может быть аксиоматизирована без схем, называется конечно аксиоматизируемой .
Два хорошо известных примера схем аксиом:
Чеслав Рылль-Нардзевский доказал, что арифметика Пеано не может быть конечно аксиоматизирована, а Ричард Монтегю доказал, что ZFC не может быть конечно аксиоматизирована. [1] Следовательно, схемы аксиом не могут быть устранены из этих теорий. Это также касается довольно многих других аксиоматических теорий в математике, философии, лингвистике и т. д.
Все теоремы ZFC являются также теоремами теории множеств фон Неймана–Бернайса–Гёделя , но последняя может быть конечно аксиоматизирована. Теория множеств Новые основания может быть конечно аксиоматизирована через понятие стратификации .
Схемные переменные в логике первого порядка обычно тривиально исключаются в логике второго порядка , поскольку схематическая переменная часто является заполнителем для любого свойства или отношения по индивидам теории. Это касается схем индукции и замены, упомянутых выше. Логика высшего порядка позволяет квантифицированным переменным ранжироваться по всем возможным свойствам или отношениям.