Kvantor

Kvantor is a term used in mathematical logic to refer to quantifiers, the operators that specify the scope of a variable within a logical formula. The word is a transliteration of the Russian квантор and appears in various languages as a name for the logical concept, though the standard English term is quantifier.

The two primary quantifiers are the universal quantifier, written ∀, and the existential quantifier, written ∃. A statement such as ∀x (x ∈ X → P(x)) asserts that P holds for every element of X; ∃x ∈ X P(x) asserts that there exists at least one element of X for which P holds. Logical equivalences include ¬∃x P(x) ≡ ∀x ¬P(x) and ¬∀x P(x) ≡ ∃x ¬P(x).

Quantifiers are fundamental in predicate logic, model theory, and formal semantics. They also appear in computer science and databases in forms such as SQL’s EXISTS and FOR ALL-like constructs, and in automated theorem proving and formal verification. Quantifier elimination is a technique for simplifying logical formulas in certain theories.

Etymology and usage notes: the term derives from Latin quantus meaning “how much” and related roots; in many languages, квантор (Russian) or quantor are used as direct translations of quantifier. The term often appears in textbooks and translations to refer to the same concept.