Схема аксиом в математической логике: обобщение понятия аксиомы, формулы с переменными для бесконечного множества аксиом. Основы аксиоматических систем.
Сравнивайте с английским: нажмите на абзац — оригинал откроется в окне. Кнопка EN под абзацем показывает его прямо в тексте.
Содержание
Введение
Краткое обозначение для набора утверждений, принимаемых за истинные.
Short notation for a set of statements that are taken to be true
В математической логике схема аксиом (множественное число: схемы аксиом) обобщает понятие аксиомы.
In mathematical logic, an axiom schema (plural: axiom schemata or axiom schemas) generalizes the notion of axiom.
Формальное определение
Схема аксиомы — это формула в метаязыке аксиоматической системы, содержащая одну или несколько схематических переменных. Эти переменные, являющиеся металингвистическими конструкциями, обозначают любой терм или подформулу системы, которые могут (но не обязаны) удовлетворять определенным условиям. Зачастую эти условия требуют, чтобы определенные переменные были свободными, или чтобы определенные переменные не встречались в подформуле или терме.
An axiom schema is a formula in the metalanguage of an axiomatic system, in which one or more schematic variables appear. These variables, which are metalinguistic constructs, stand for any term or subformula of the system, which may or may not be required to satisfy certain conditions. Often, such conditions require that certain variables be free, or that certain variables not appear in the subformula or term.
Окончательная аксиоматизация
Учитывая, что число возможных подформул или термов, которые могут быть подставлены на место схематической переменной, бесконечно, схема аксиом представляет собой бесконечный класс или множество аксиом. Это множество часто можно определить рекурсивно. Теория, которая может быть аксиоматизирована без схем, называется конечно аксиоматизируемой.
Given that the number of possible subformulas or terms that can be inserted in place of a schematic variable is infinite, an axiom schema stands for an infinite class or set of axioms. This set can often be defined recursively. A theory that can be axiomatized without schemata is said to be finitely axiomatizable.
Окончательно аксиоматизированные теории
Все теоремы ZFC также являются теоремами теории множеств фон Неймана — Бернайса — Гёделя, но последняя может быть аксиоматизирована конечным числом аксиом. Теорию множеств «Новые основы» можно аксиоматизировать конечным числом аксиом посредством понятия стратификации.
All theorems of ZFC are also theorems of von Neumann–Bernays–Gödel set theory, but the latter can be finitely axiomatized. The set theory New Foundations can be finitely axiomatized through the notion of stratification.
В логике высшего порядка
Схематические переменные в логике первого порядка обычно легко устранимы в логике второго порядка, поскольку схематическая переменная часто представляет собой заполнитель для любого свойства или отношения над индивидами теории. Это справедливо для схем индукции и замены, упомянутых выше. Логика высшего порядка позволяет квантованным переменным варьировать по всем возможным свойствам или отношениям.
Schematic variables in first order logic are usually trivially eliminable in second order logic, because a schematic variable is often a placeholder for any property or relation over the individuals of the theory. This is the case with the schemata of Induction and Replacement mentioned above. Higher order logic allows quantified variables to range over all possible properties or relations.