Existenzquantors

Existenzquantors, or Existenzquantoren in German terminology, refer to the existential quantifier in formal logic. The existential quantifier asserts that there exists at least one element in the domain that satisfies a given predicate. It is typically written as ∃x φ(x) and binds the variable x within the formula.

Semantics and role: In a model M with domain D, M satisfies ∃x φ(x) if there is some d in D such that M ⊨ φ(d). The existential quantifier is dual to the universal quantifier, since ∀x φ(x) is equivalent to ¬∃x ¬φ(x). Together, they form the basic means of expressing quantified statements about objects in a domain.

Proof rules and usage: Existential introduction allows deriving ∃x φ(x) from a specific instance φ(t) for a term t. Existential elimination, or ∃-elimination, permits deriving a conclusion ψ from ∃x φ(x) by assuming φ(x) for a fresh variable and showing that ψ follows independently of the particular witness chosen. These rules underpin many natural deduction and sequent-calculus systems.

Variations and extensions: Quantification can be bounded, as in ∃x ∈ A φ(x), to restrict the domain to a subset A. In modal logic, existential quantification interacts with modality, yielding notions such as existence in some possible world. In type theory and constructive logic, existential quantification corresponds to the existence of a witness, often represented by a dependent pair or sigma type. Some frameworks also connect the existential quantifier to witness extraction via epsilon terms or choice principles.

History and terminology: The term Existenzquantor is standard in German-language logic for the existential quantifier. In English, the symbol ∃ is described as the existential quantifier, with its dual ∀ used for universal statements.