Quantifier

see predicate

Universal Quantifier

equiv boolean > conjunction-reduce

definition \(\forall P = \land\ P\)

note \(\forall S\ x.\ P\ x\) means \(\land\ (S \to P)\)

Existential Quantifier

equiv boolean > disjunction-reduce

definition \(\exists P = \lor\ P\)

note \(\exists S\ x.\ P\ x\) means \(\lor\ (S \land P)\)

Uniqueness Quantifier

definition \(\exists! P = \exists P\ x.\ \forall P\ y.\ x = y\)

note the universal < quantifier and existential < quantifier are fundamental and work well together because they're duals. the uniqueness < quantifier, on the other hand, is a whole different thing because it either assumes or defines a equivalence < relation. it can be a useful shorthand, but it's in no way fundamental