Аксіомна схема

У математичній логіці, аксіомна схема (схема аксіом) узагальнює поняття аксіоми.

Аксіома являє собою формулу у мові аксіоматичної системи, у якій присутні одна або більше схематичних змінних. Ці змінні, являючи собою метамовні конструкти, заміщують будь-які терми або підформули системи.

Враховуючи, що число можливих підформул або термів, що можуть бути поставлені замість схематичної змінної є зліченно нескінченною, аксіомна схема виконує роль зліченно нескінченної множини аксіом. Ця множина може бути зазвичай визначена рекурсивно. Теорія, що може бути аксіоматизована без схем, називається скінченно аксіоматизовуваною. Теорії, що можуть бути скінченно аксіоматизованими, розглядаються як дещо быльш математично елегантні, навіть якщо вони менш практичні для дедуктивної роботи.

Два добре відомих приклада аксіомних схем є:

• Схема індукції, що є складовою аксіом Пеано для арифметики натуральних чисел;
• Аксіомна схема заміщення, що є складовою стандартної ZFC аксіоматизації теорії множин.

Було доведено (уперше Річардом Монтегю), що ці схеми не можуть бути усунені. Тому арифметика Пеано і ZFC не можуть бути скінченно аксіоматизованими. Це також має місце для кількох інших аксіоматичних теорій у математиці, філософії, лінгвістиці тощо.

Всі теореми ZFC є також теоремами теорії множин фон Нойманна-Бернайса-Гьоделя, проте остання, quite surprisingly, скінченно аксіоматизовувана. Теорія множин Нові Основи може бути скінченно аксіоматизована, але тільки з деякою втратою елегантності.

Схематичні змінні у логіці першого порядку зазвичай усуваються тривіально у логіці другого порядку, оскільки схематична змінна часто стоїть на місці довільної властивості або відношення над індивідами теорії. Це має місце зі схемами Індукції та Заміщення, згаданих вище. Логіка вищих порядків дозволяє квантифікованим змінним приймати значення усіх можливих властивостей та відношень.