Квантор является связующим символом для формулы, с логическими значениями.
Квантор Q связывающий x с диапазоном E по формуле A, полностью пишется
Qx ∈ E, A(x)
где A(x) сокращение формулы со свободными переменными х и возможные параметрами.Иногда, область (тип или класс) ставится в качестве индекса: (QEx, A(x)), или остается неявным (установленным контекстом): (Qx, A(x)) (неважно, фиксируется ли в контексте, например, в общей теории). Два основных квантора (под которыми и другие будут определены позже) - это:
- Квантор существования ∃, который гласит "существует x, такой что..."
- Квантор общности ∀, который гласит «Для всех (или: для любого) x (в...),... ».
Их интерпретация может быть определена в ряде теоретий, где A рассматривается как функция и логические значения - в качестве объектов:
(∀x, A(x))
⇔ A = (x ↦ 1)
(∃x, A(x)) ⇔ A ≠ (x ↦ 0)
(∀x, A(x)) ⇎ (∃x, ¬A(x))
В теории множеств, (∀x∈E, A(x)) ⇔ {x∈E
| A(x)} = E. Формула (∀x,1)
всегда верна. С классами,
| (∃C x, A(x)) (∀C x, A(x)) ∀x, (C(x) |
⇔ (∃x, C(x) ∧ A(x))
⇔ ∃C∧A x, 1 ⇔ (∀x, C(x) ⇒ A(x)) ⇔ (∃C y, x=y)) |
Включение между классами
Считается, что класс A включен в класс B, когда ∀ x, A(x) ⇒ B(x). Тогда A - это подкласс B, как ∀x, A(x) ⇔ (B(x)
∧ A(x)). И наоборот, любой подкласс A включен в подкласс B, что подразумевает для любого предиката C (в случаях определенности):
(∀B
x, C(x)) ⇒ (∀A x,
C(x))
(∃A x, C(x)) ⇒ (∃B
x, C(x))
(∃C x, A(x)) ⇒ (∃C
x, B(x))
(∀C x, A(x)) ⇒ (∀C
x, B(x))
Правила доказательств для квантификаторов по унарному предикату
Экзистенциальное введение. Если у нас есть условия t′, …и доказательство (A(t) ∨ A(t′) ∨ …), тогда ∃x,A(x).
Экзистенциальное устранение. Если ∃x, A(x), то мы можем ввести новую свободную переменную z с гипотезой A(z) (последствия будут истинными, без ограничения общности).
Эти правила выражают смысл ∃ : переходя от t, … к ∃ затем из ∃ к z, это все равно что позволить z представлять одну из t, t′, … (не зная, какую именно). Они придают тот же смысл ∃C относительно его 2 вышеприведенных эквивалентных формул, минуя расширенное правило определенности для (C ∧ A) сосредоточив внимание на случае, когда C(x) является истинным и, следовательно A(x) является определенным.
В то время как ∃ появился как обозначение объекта, ∀ появляется в качестве правила вычета.
Универсальное введение. Если из всего лишь гипотезой C(x) на новой свободной переменной x мы могли вывести A(x), то ∀C x, A(x).
Универсальное устранение. Если ∀C x,A(x) и t является термом, выполняющим C(t), то A(t).
Представляя затем устранение ∀ как замену x на t в начальном доказательстве.
Отчисления могут быть сделаны этими правилами, отражающие формулы
| ((∀C x, A(x)) ∧ (∀C x, A(x) ⇒ B(x))) | ⇒ (∀C x, B(x)) |
| ((∃C x, A(x)) ∧ (∀C x, A(x) ⇒ B(x))) | ⇒ (∃C x, B(x)) |
| (∀C x, A(x)) ∧ (∃C x, B(x))) | ⇒ (∃C x, A(x) ∧ B(x)) |
| (∃A x, ∀B y, R(x,y)) | ⇒ (∀By, ∃A x, R(x,y)) |
Статус открытых кванторов в теории множеств
Теория множеств переводится в генерическую теорию путем преобразования в классах области кванторов:
(∃x∈E,
A(x)) → (∃x, x ∈ E ∧ A(x))
(∀x∈E, A(x)) → (∀x, x
∈ E ⇒ A(x))
Теория множеств допускает только квантор над множествами, с названием ограниченный квантор, в своих формулах, что для усиления будут называться ограниченными формулами (которые определяют предикат и могут быть использованы в выражении). Но его форма перехода в теории разрешает существование кванторов на любых классах (или вселенной), называемых открытыми кванторами.
Формулы с открытым кванторами в теории множеств будут называться претензиями. Их использование будет существенно ограничено декларацией истины замкнутых определенных претензий. Они сначала будут аксиомами, потом теоремами (выведены из аксиом и с разными именами в зависимости от их важности: теорема является более важной, чем предложение, может быть выведена из леммы, и легко может привести к следствию).
Открытые кванторы в претензии часто будут выражены как общие артикуляции языка (неявно используя вышеуказанные правила доказательств) между их ограниченными подформулами (написанными символами теории множеств).
Образователь множества определяется K = {x∈E| A(x)} претензиями (∀x, x∈K ⇔ (x∈E ∧ A(x))), но в 1.11 он будет пересмотрен без открытого квантора (кроме его параметров).