Editing Universal quantification (section)

== Properties ==

<!-- ''We need a list of algebraic properties of universal quantification, such as distributivity over conjunction, and so on. Also rules of inference.'' -->

=== Negation ===
The negation of a universally quantified function is obtained by changing the universal quantifier into an [[existential quantifier]] and negating the quantified formula. That is, 
:<math>\lnot \forall x\; P(x)\quad\text {is equivalent to}\quad \exists x\;\lnot P(x) </math>
where <math>\lnot</math> denotes [[negation]].

For example, if {{math|''P''(''x'')}} is the [[propositional function]] "{{math|''x''}} is married", then, for the [[set (mathematics)|set]] {{mvar|X}} of all living human beings, the universal quantification
<blockquote>Given any living person {{math|''x''}}, that person is married</blockquote>
is written
:<math>\forall x \in X\, P(x)</math>

This statement is false. Truthfully, it is stated that
<blockquote>It is not the case that, given any living person {{mvar|''x''}}, that person is married</blockquote>
or, symbolically:
:<math>\lnot\ \forall x \in X\, P(x)</math>.

If the function {{math|''P''(''x'')}} is not true for ''every'' element of {{mvar|X}}, then there must be at least one element for which the statement is false. That is, the negation of <math>\forall x \in X\, P(x)</math> is logically equivalent to "There exists a living person {{math|''x''}} who is not married", or:
:<math>\exists x \in X\, \lnot P(x)</math>

It is erroneous to confuse "all persons are not married" (i.e. "there exists no person who is married") with "not all persons are married" (i.e. "there exists a person who is not married"):
:<math>\lnot\ \exists x \in X\, P(x) \equiv\ \forall x \in X\, \lnot P(x) \not\equiv\ \lnot\ \forall x\in X\, P(x) \equiv\ \exists x \in X\, \lnot P(x)</math>

=== Other connectives ===
The universal (and existential) quantifier moves unchanged across the [[logical connective]]s [[logical conjunction|∧]], [[logical disjunction|∨]], [[material conditional|→]], and [[converse nonimplication|↚]], as long as the other operand is not affected;<ref>that is, if the variable <math>y</math> does not occur free in the formula <math>P(x)</math> in the equivalences below</ref> that is:

:<math>\begin{align}
P(x) \land (\exists{y}{\in}\mathbf{Y}\, Q(y)) &\equiv\ \exists{y}{\in}\mathbf{Y}\, (P(x) \land Q(y)) \\
P(x) \lor  (\exists{y}{\in}\mathbf{Y}\, Q(y)) &\equiv\ \exists{y}{\in}\mathbf{Y}\, (P(x) \lor Q(y)),& \text{provided that } \mathbf{Y}\neq \emptyset \\
P(x) \to   (\exists{y}{\in}\mathbf{Y}\, Q(y)) &\equiv\ \exists{y}{\in}\mathbf{Y}\, (P(x) \to Q(y)),& \text{provided that } \mathbf{Y}\neq \emptyset \\
P(x) \nleftarrow (\exists{y}{\in}\mathbf{Y}\, Q(y)) &\equiv\ \exists{y}{\in}\mathbf{Y}\, (P(x) \nleftarrow Q(y)) \\
P(x) \land (\forall{y}{\in}\mathbf{Y}\, Q(y)) &\equiv\ \forall{y}{\in}\mathbf{Y}\, (P(x) \land Q(y)),& \text{provided that } \mathbf{Y}\neq \emptyset \\
P(x) \lor  (\forall{y}{\in}\mathbf{Y}\, Q(y)) &\equiv\ \forall{y}{\in}\mathbf{Y}\, (P(x) \lor Q(y)) \\
P(x) \to   (\forall{y}{\in}\mathbf{Y}\, Q(y)) &\equiv\ \forall{y}{\in}\mathbf{Y}\, (P(x) \to Q(y)) \\
P(x) \nleftarrow (\forall{y}{\in}\mathbf{Y}\, Q(y)) &\equiv\ \forall{y}{\in}\mathbf{Y}\, (P(x) \nleftarrow Q(y)),& \text{provided that } \mathbf{Y}\neq \emptyset
\end{align}</math>

Conversely, for the logical connectives [[Sheffer stroke|↑]], [[Logical NOR|↓]], [[Material nonimplication|↛]], and [[converse implication|←]], the quantifiers flip:

:<math>\begin{align}
P(x) \uparrow (\exists{y}{\in}\mathbf{Y}\, Q(y)) & \equiv\ \forall{y}{\in}\mathbf{Y}\, (P(x) \uparrow Q(y)) \\
P(x) \downarrow  (\exists{y}{\in}\mathbf{Y}\, Q(y)) & \equiv\ \forall{y}{\in}\mathbf{Y}\, (P(x) \downarrow Q(y)),& \text{provided that } \mathbf{Y}\neq \emptyset \\
P(x) \nrightarrow (\exists{y}{\in}\mathbf{Y}\, Q(y)) & \equiv\ \forall{y}{\in}\mathbf{Y}\, (P(x) \nrightarrow Q(y)),& \text{provided that } \mathbf{Y}\neq \emptyset \\
P(x) \gets (\exists{y}{\in}\mathbf{Y}\, Q(y)) & \equiv\ \forall{y}{\in}\mathbf{Y}\, (P(x) \gets Q(y)) \\
P(x) \uparrow (\forall{y}{\in}\mathbf{Y}\, Q(y)) & \equiv\ \exists{y}{\in}\mathbf{Y}\, (P(x) \uparrow Q(y)),& \text{provided that } \mathbf{Y}\neq \emptyset \\
P(x) \downarrow  (\forall{y}{\in}\mathbf{Y}\, Q(y)) & \equiv\ \exists{y}{\in}\mathbf{Y}\, (P(x) \downarrow Q(y)) \\
P(x) \nrightarrow (\forall{y}{\in}\mathbf{Y}\, Q(y)) & \equiv\ \exists{y}{\in}\mathbf{Y}\, (P(x) \nrightarrow Q(y)) \\
P(x) \gets (\forall{y}{\in}\mathbf{Y}\, Q(y)) & \equiv\ \exists{y}{\in}\mathbf{Y}\, (P(x) \gets Q(y)),& \text{provided that } \mathbf{Y}\neq \emptyset \\
\end{align}</math>
<!-- What about:
*[[logical biconditional|Biconditional (if and only if) (xnor)]] (<math>\leftrightarrow</math>, <math>\equiv</math>, or <math>=</math>)
*[[Exclusive or|Exclusive disjunction (xor)]] (<math>\not\leftrightarrow</math>)
-->

=== Rules of inference ===

A [[rule of inference]] is a rule justifying a logical step from hypothesis to conclusion.  There are several rules of inference which utilize the universal quantifier.

''[[Universal instantiation]]'' concludes that, if the propositional function is known to be universally true, then it must be true for any arbitrary element of the universe of discourse.  Symbolically, this is represented as

:<math> \forall{x}{\in}\mathbf{X}\, P(x) \to P(c)</math>

where ''c'' is a completely arbitrary element of the universe of discourse.

''[[Universal generalization]]'' concludes the propositional function must be universally true if it is true for any arbitrary element of the universe of discourse.  Symbolically, for an arbitrary ''c'',

:<math> P(c) \to\ \forall{x}{\in}\mathbf{X}\, P(x).</math>

The element&nbsp;''c'' must be completely arbitrary; else, the logic does not follow: if ''c'' is not arbitrary, and is instead a specific element of the universe of discourse, then P(''c'') only implies an existential quantification of the propositional function.
<!-- ''Discuss universally quantified types in [[type theory]].'' -->

=== The empty set ===

By convention, the formula <math>\forall{x}{\in}\emptyset \, P(x)</math> is always true, regardless of the formula ''P''(''x''); see [[vacuous truth]].