∃x φ(x) is true in a structure iff there exists at least one object a in the domain for which φ(a) is true. The existential quantifier is the logical analog of disjunction over all objects. The dual relationship ¬∀x φ ≡ ∃x ¬φ is central.
From your work on quantifier basics, you know that quantifiers bind variables and range them over a domain. Now let's build precise intuition for what the existential quantifier actually *computes*. The formula ∃x φ(x) is true in a structure exactly when you can find at least one witness — one specific object a in the domain — such that φ(a) holds. This is analogous to disjunction: if the domain is {a₁, a₂, a₃}, then ∃x φ(x) is equivalent to φ(a₁) ∨ φ(a₂) ∨ φ(a₃). For finite domains this is just a big OR. For infinite domains, you can't write it out explicitly, but the semantics is the same: there exists *some* witness, though you may not need to name it.
The key distinction between the existential and universal quantifiers is what *refutes* them. To prove ∃x φ(x) is *false*, you must show that φ(a) is false for *every* a in the domain — no exceptions. To prove ∀x φ(x) is *false*, you only need one counterexample. This asymmetry is captured in the dual law: ¬∃x φ(x) ≡ ∀x ¬φ(x) and ¬∀x φ(x) ≡ ∃x ¬φ(x). Negation pushes through the quantifier and flips it. This is the quantifier analog of De Morgan's laws for AND and OR: ¬(A ∨ B) ≡ ¬A ∧ ¬B. In fact, the analogy is exact: ∃ corresponds to ∨ and ∀ corresponds to ∧.
Scope is where students most often go wrong. In ∃x (φ(x) ∧ ψ(x)), the variable x is bound throughout the parenthesized formula — the same witness must satisfy both φ and ψ. But in (∃x φ(x)) ∧ (∃x ψ(x)), the two occurrences of x are *independently* bound; the witness for the first existential need not be the same as for the second. The parentheses determine which part of the formula the quantifier governs. A variable that appears in a formula without a governing quantifier is free — it acts like a parameter whose value must be supplied from outside the formula.
In a structure (a domain D together with interpretations for the predicate and function symbols), evaluating ∃x φ(x) requires searching D for a witness. When D is infinite, there may be infinitely many witnesses or none — but you only need one to make the statement true. This semantic picture — formulas evaluated against structures — is the foundation for the model-theoretic perspective you'll develop further. When you later study quantifier elimination, you'll be asking: can every formula involving ∃ be rewritten as an equivalent formula without ∃? That property (quantifier elimination) turns out to make certain theories decidable and is the key to understanding why theories like the theory of algebraically closed fields are so well-behaved.