The statements that describe valid input are known as preconditions and the conditions that the output should satisfy when the program has run are known as postconditions.
Universal quantification, which tells us that a predicate is true for every element under consideration,
Existential quantification, which tells us that there is one or more element under consideration for which the predicate is true.
DEFINITION 1
The universal quantification of P (x) is the statement “P (x) for all values of x in the domain.”
The notation ∀xP (x) denotes the universal quantification of P (x). Here ∀ is called the universal quantifier.
We read ∀xP (x) as “for all xP (x)” or “for every xP (x).”
An element for which P (x) is false is called a counterexample of ∀xP (x).
DEFINITION 2
The existential quantification of P (x) is the proposition “There exists an element x in the domain such that P (x).”
We use the notation ∃xP (x) for the existential quantification of P (x). Here ∃ is called the existential quantifier.
Binding Variables When a quantifier is used on the variable x, we say that this occurrence of the variable is bound.
An occurrence of a variable that is not bound by a quantifier or set equal to a particular value is said to be free.
All the variables that occur in a propositional function must be bound or set equal to a particular value to turn it into a proposition.
This can be done using a combination of universal quantifiers, existential quantifiers, and value assignments.
The part of a logical expression to which a quantifier is applied is called the scope of this quantifier. Consequently,
a variable is free if it is outside the scope of all quantifiers in the formula that specify this variable.
The uniqueness quantifier, denoted by ∃! or ∃1.
The notation ∃!xP (x) [or ∃1xP (x)] states “There exists a unique x such that P (x) is true.”
Other phrases for uniqueness quantification include “there is exactly one” and “there is one and only one.”
For instance, ∃!x(x − 1 = 0), where the domain is the set of real numbers, states that there is a unique real number x such that x − 1 = 0.
This is a true statement, as x = 1 is the unique real number such that x − 1 = 0.
Quantifiers with Restricted Domains
An abbreviated notation is often used to restrict the domain of a quantifier.
In this nota-tion, a condition a variable must satisfy is included after the quantifier.
Precedence of Quantifiers The quantifiers ∀ and ∃ have higher precedence than all logical operators from propositional calculus.
For example, ∀xP (x) ∨ Q(x) is the disjunction of ∀xP (x) and Q(x). In other words, it means (∀xP (x)) ∨ Q(x) rather than ∀x(P (x) ∨ Q(x)).
DEFINITION 3
Statements involving predicates and quantifiers are logically equivalent if and only if
they have the same truth value no matter which predicates are substituted into these
statements and which domain of discourse is used for the variables in these propositional functions.
We use the notation S ≡ T to indicate that two statements S and T involving predicates and quantifiers are logically equivalent.
原文：https://www.cnblogs.com/minost/p/10964381.html