We can extend Propositional Logic by adding more statements and rules of inference to those we already have in our formal system. This extended formal system is called Predicate Logic.
Many math expressions contain identifiers which are variables that have no meaning outside of the expression. For example, in an expression like $\sum_{k=0}^n k^3$, the variable $k$ is bound to the expression in the sense that has no meaning outside the expression itself. Indeed, we can replace it with any other letter that is not declared to be a constant to obtain an expression with the exact same meaning, like $\sum_{i=0}^n i^3$.
Definition . A binding is an expression of the form $x.E$ where $x$ is any non-constant identifier and $E$ is any expression. All occurrences of $x$ in $x.E$ are said to be bound variables. All identifiers in $x.E$ other than constants or bound variable are called free variables. An operator applied to a binding is called a quantifier.
We can apply a constant operator $\lambda$ to a binding expression $x.E$ to form the expression $\lambda x.E$ called lambda expressions. Such expressions can be applied to an expression $a$ to form a new expression, $(\lambda x.E)(a)$. Another name for a lambda expression is anonymous function and they can also be written as $x\mapsto E$.
These can be evaluated to form the expression obtained by replacing all occurrences of $x$ in $E$ with $(a)$ (no free identifier in $a$ should become bound as a result of the substitution). If we give a name to an anonymous function, e.g., if we define $f$ to be $\lambda x.E$ then the expression $(\lambda x.E)(a)$ is just the usual prefix notation for function application $f(a)$. In this situation we refer to $a$ as the argument of the anonymous function application.
For example, $(x\mapsto x^3)(a)$ evaluates to $a^3$. Indeed, in many math textbooks they will write $f(x)=x^3$ instead of $f=(x \mapsto x^3)$, but the latter is usually what they mean. In this example, we have the usual evaluation of functions, e.g., $f(a)=a^3$, $f(2)=2^3$, and $f(x+1)=(x+1)^3$.
Notice that simply replacing all occurrences of $x$ in $\lambda x.E$ with another identifier that does not appear in $E$ produces a new lambda expression which evaluates to the same thing as the original lambda expression when applied to the same argument. Such lambda expressions are said to be $\alpha$-equivalent.
Predicate logic extends propositional logic by defining two additional quantifiers.
Definition . The symbols $\forall$ and $\exists$ are quantifiers. The symbol $\forall$ is called “for all”, “for every”, or “for each”. The symbol $\exists$ is called “for some” or “there exists”.
We will encounter more quantifiers beyond just these two.
Every statement of Propositional Logic is still a statement of Predicate Logic. In addition, we define the following new statements.
Definition If $x$ is any variable and $\mc{P}(x)$ any statement that results from applying a lambda expression $\mc{P}$ to $x$, then $(\forall x.\mc{P}(x))$ and $(\exists x.\mc{P}(x))$ are both statements.
We say that the scope of the quantifier in $(\forall x.W(x))$ and $(\exists x.W(x))$ is everything inside the outer parentheses. Sometimes the outer parentheses are omitted when the scope is clear from context. All occurrences of $x$ throughout the scope are said to be bound by the quantifier.
In addition to declaring global constants in our proofs we will also need to be able to introduce new identifiers into our proofs. Just like all expressions and environments, we will have one declaration that is an assumption and one that is a claim.
Definition
A let declaration is an expression of the form
Let $x_1,\ldots x_n$
be such that $W$
A for-some-declaration is an expression of the form
$W$ for some $x_1,\ldots x_n$
In both declarations $x_1,\ldots x_n$ must be new identifiers at that point in the proof, and $W$ is called the body of the declaration. The scope of each declaration starts at the declaration and continues until the end of the environment containing it.
A let-declaration is an assumption that we can name arbitrary things
that satisfy the statement $W$. If the phrase
be such that $W$ is omitted then a let-declaration is
just the assumption that $x_1,\ldots x_n$ are completely arbitrary
unspecified things with no restrictions. A for-some-declaration is a
claim that we can name arbitrary unspecified things that we know exist
and satisfy the statement $W$.
Bound variables do not have to be declared. They can be any identifier you like, as long as that identifier is not in the scope of a constant declaration or more than one binding expression that binds it.
Since a let-declaration is an assumption, it can be the premise of a special kind of if-then environment.
Definition . A let-environment is an if-then environment containing a let-declaration followed by one or more claims.
Note that a let-environment will usually not have additional assumptions after the initial let-declaration because usually we will want such assumptions to be included in the body.
Following Gentzen, we have an introduction and elimination rule for each of the two logical quantifiers.
Rules of Propositional Logic
| Name | Rule |
|---|---|
| $\forall+$ | $(\xlet s \vdash \mc{P}(s)) \vdash \forall x.\mc{P}(x)$ |
| $\forall-$ | $(\forall x.\mc{P}(x)) \vdash \mc{P}(t)$ |
| $\exists+$ | $\mc{P}(t) \vdash \exists x.\mc{P}(x)$ |
| $\exists-$ | $(\exists x.\mc{P}(x)) \vdash \mc{P}(c)\forsome x$ |
We can also list these rules in if-then rule notation that mirrors how they are used in proofs.
Definition of Quantifiers
Declare $\forall$, $\exists$ to be constants.
$\forall+$
Given
Let $s$ be arbitrary.
$\mc{P(s)}$
Conclude $\forall x.\mc{P(x)}$
$\forall-$
Given
$\forall x.\mc{P(x)}$
Conclude $\mc{P(t)}$
$\exists+$
Given
$\mc{P(t)}$
Conclude $\exists x.\mc{P(x)}$
$\exists-$
Given
$\exists x.\mc{P(x)}$
Conclude $\mc{P(c)}\forsome c$
Restrictions and Remarks:
Finally, we can complete our definition of logic by adding the rules of inference for equality. This definition was first introduced by Leibniz.
Definition of $=$
| Name | Rule |
|---|---|
| reflexivity | $x=x$ |
| substitution | $(x=y),W\vdash,W$ with one or more free occurrences of $x$ replaced by $y$ |
As usual we can also list these rules in if-then rule notation that mirrors how they are used in proofs.
Definition of equals
Declare = to be a constant.
Reflexivity
Conclude $x=x$
Substitution
Given
$x=y$
$W$
Conclude $W$ with one or more free occurrences of $x$ replaced by $y$
Restrictions and Remarks:
Prove each of the following theorems with a formal proof in our system of Natural Deduction. In all of these, $P,Q,R$ are statements (or lambda expressions that return a statement) and the variables $x,y,z$ etc. are of the same unspecified type.
distributivity $(\forall x.P(x) \xand Q(x)) \iff (\forall y.P(y)) \xand (\forall z.Q(z))$
distributivity $(\exists x.P(x) \xor Q(x)) \iff (\exists y.P(y)) \xor (\exists z.Q(z))$
distributivity $(\exists x.P(x) \implies Q(x)) \iff (\forall y.P(y)) \implies (\exists z.Q(z))$
equivalent predicates $(\forall x.P(x) \iff Q(x)) \implies ((\exists x.P(x))\implies (\exists x.Q(x)))$
commutativity $(\forall x.\forall y.P(x,y)) \implies (\forall y.\forall x.P(x,y))$
commutativity $(\exists x.\exists y.P(x,y)) \implies (\exists y.\exists x.P(x,y))$
one for all $(\exists y.\forall x.P(x,y)) \implies (\forall x.\exists y.P(x,y))$
some are the same $(\forall x.\forall y. P(x,y)) \implies \forall z. P(z,z)$
De Morgan $\neg (\exists x.P(x)) \iff (\forall x. \neg P(x))$
De Morgan $\neg (\forall x.P(x)) \iff (\exists x. \neg P(x))$
quantifier fun $\left(\forall x. P(x) \implies Q(x)\right) \xand \left(\forall x.\neg Q(x)\right) \implies \left(\forall x. \neg P(x)\right)$
more quantifier fun $(\forall x. P(x) \xor Q(x)) \xand (\exists y. \neg P(y)) \implies (\exists z. Q(z))$
less than, for example $$(\forall x. \neg P(x, x)) \xand (\forall x. \forall y. \forall z. P(x, y) \xand P(y, z) \implies P(x, z)) \implies (\forall x. \forall y. \neg (P(x, y) \xand P(y, x)))$$
excluded middle $(\forall x.P(x)) \xor (\exists x.\neg P(x))$
In the next three theorems, $P$ is a statement not containing $x$.
de-quantify $(\exists x.Q(x) \xand P) \iff (\exists x.Q(x)) \xand P$
de-quantify $(\forall x.Q(x) \xor P) \iff (\forall x.Q(x)) \xor P$
de-quantify $(\forall x.Q(x) \implies P) \iff (\exists x. Q(x)) \implies P$
symmetry of equality $x=y \implies y=x$
avoiding vacuous types $(\exists x. x=x) \xand (\forall y. P(y)) \implies \exists z. P(z)$
alternate definitions of unique existence $(\exists x,P(x)\xand \forall y.P(y)\implies y=x) \iff (\exists x.P(x) \xand \forall y.\neg(y=x) \implies \neg P(y))$
Let $L(x,y)$ be the statement “$x$ loves $y$” and the domain of
discourse of all quantified variables be the set of all people.
Write each of the following English statements using only
and, or, $\neg$, $\implies$, $\iff$,
$\forall$, $\exists$, $L$, $=$, the bound variables $x$ and $y$ and
the constants (names of people) given in the sentences. For example,
we could express “Everyone loves Bob.” as “$\forall
x.L(x,\text{Bob})$”.
Let $P(x,y)$ be the statement `$x$ is the parent of $y$’ and the domain of discourse of all quantified variables be the set of all people. What do each of the following say in English?
Given the first two statements, is the conclusion valid? If not, describe a situation where the conclusion is false. If it is, formalize the argument and give a formal proof.
Everyone fears Dracula.
Dracula only fears me.
Therefore, I *am* Dracula!
A function $f$ that maps the positive real numbers to other positive real numbers is said to be continuous (C) if and only if $$\forall \varepsilon, \forall x.\exists \delta,\forall y. \left|x-y\right|<\delta \implies \left|f(x)-f(y)\right|<\varepsilon$$ Similarly, $f$ is said to be uniformly continuous (UC) if and only if $$\forall \varepsilon,\exists \delta, \forall x.\forall y. \left|x-y\right|<\delta \implies \left|f(x)-f(y)\right|< \varepsilon$$ (all identifiers other than $f$ have type “positive real”).
Note: You can use the fact that the real numbers are closed under multiplication, that constants like, $3$, $\pi$, $\sqrt{2}$, $4/5$ are real numbers and properties of real number arithmetic, like $1+1=2$, or $x+x=2x$, justifying these with the black-box reason by arithmetic.
When writing formal proofs we quickly find that the perfect rigor they provide is quickly offset by the extreme length and tediousness of the proofs. Indeed, this aspect of formal proofs is often counter to our goal of elegant and effective exposition. So how can we retain the objective validity and rigor of a formal proof and make our proofs more elegant and expository at the same time?
One way is to use well-defined shortcuts that eliminate the tedious, obvious aspects of our proofs, while retaining the rigor and important concepts. In this book we will list some of the shortcuts that mathematicians use in order to shorten the proofs, make them more readable, and eliminate parts of the proof that are repetitive or uninteresting.
Once we have proven a theorem, we can use it as a new rule of inference. Theorems are like Rules in that they can be used as formulas by considering their free variables to be metavariables. Thus, after we prove the major results about a particular topic, we can add those theorems to the list of rules we can use to prove additional results in new topic.
The following theorems about logic are quite well-known, and can usually be used in an expository proof without proving them or even justifying them with a reason (although you should in a formal or semiformal proof).
Theorems of Logic
Theorem (double negative) $\xnot(\xnot W) \equiv W$
Theorem (excluded middle) $W\xor\xnot W$
Theorem (commutativity of or)
If $W\xor V$ then
$V\xor W$
Theorem (associativity of or)
$(W\xor V)\xor U \equiv W \xor (V \xor U)$
Theorem (ternary and)
$W\xand V \xand U \equiv W, V, U$
Theorem (alternate definition of implies) $W\implies V\equiv \xnot W \xor V$
Theorem (alternate or-)
If $W\xor V$ and
$\xnot W$ then
$V$
Theorem (alternate or-)
If $W\xor V$ and
$\xnot V$ then
$W$
Theorem (negated implication)
$\xnot (W\implies V) \equiv W, \xnot V$
Theorem (contrapositive)
If $W\implies V$ and
$\xnot V$ then
$\xnot W$
Theorem (De Morgan)
$\xnot(W \xand V) \equiv \xnot W \xor \xnot V$
Theorem (De Morgan)
$\xnot(W \xor V) \equiv \xnot W, \xnot V $
Sometimes the most elegant or compact way to state or prove a theorem is not the most useful way to use it as a rule for proving future theorems. In this case we can derive rules from the theorem itself (with proof) that may be more useful for doing proofs. For example, if we have the theorem
Theorem $\forall x.x \neq 0 \implies 0\lt x^2$
We might derive the following rule from that.
Theorem 6.6If $x \neq 0$ then $0\lt x^2$
Since we can easily prove the rule from the theorem, we say that the rule is derived rom the theorem, and can refer to it by the same name.
Similarly we can replace most of the formal symbols $\implies$, $\iff$, $\forall$, and $\exists$ in our theorem statements with English phrases and sentences as illustrated in the following table.
Some English Equivalents for Formal Symbols
| A theorem such as… | …can be expressed |
|---|---|
| Theorem: $P\implies Q$ | Theorem: If $P$ then $Q$. Theorem: Given $P$. Then $Q$. Theorem: Suppose $P$. Then $Q$. |
| Theorem: $P\iff Q$ | Theorem: $P$ if and only if $Q$. |
| Theorem: $\forall n.P(n)$ | Theorem: $P(n)$. |
| Theorem: $\forall n. P(n)\implies Q(n)$ | Theorem: If $P(n)$ then $Q(n)$. |
| Theorem: $\exists n. P(n)$ | Theorem: $P(n)$ for some $n$. |
In each case, since we have eliminated the corresponding formal symbol, we no longer need to end the proof with a $\forall+$ or $\implies+$ statement.
A similar situation arises when making rules for definitions, many of which are equivalences involving the predicate logic quantifiers. In those cases we need a separate introduction and elimination rule because only one of them requires a declaration.
Derived Rules from Definitions
| Definition Form | Introduction ($+$) Rule | Elimination ($-$) Rule |
|---|---|---|
| $x$ is $y \iff \forall z.P(z)$ | $($Let $s \vdash P(s)) \vdash x$ is $y$ | $x$ is $y\vdash P(t)$ |
| $x$ is $y \iff \exists z.P(z)$ | $P(t) \vdash x$ is $y$ | $x$ is $y\vdash P(c)$ for some $c$ |
While Leibniz definition of equality is very succinct, in practice it becomes tedious to constantly use substitution, reflexivity, symmetry and transitivity explicitly many times in our proofs to reach our desired conclusion. To deal with this, mathematicians use a convenient device called a transitive chain.
Definition . Let $\langle r_1,r_2,\ldots,r_n\rangle$ be a sequence of binary operators on a set $A$. We say such a sequence is mutually transitive if and only if for every $a,b,c\in A$, and for every $1\leq i\leq j\leq n$, $$a\,r_i\,b \xand b\,r_j\,c \implies a\,r_j\,c$$ and $$a\,r_j\,b \xand b\,r_i\,c \implies a\,r_j\,c$$
Examples of mutually transitive operator sequences on the set of integers include: $\langle = \rangle$, $\langle =, \leq\rangle$, $\langle =, < \rangle$, $\langle =, \leq, <\rangle$, $\langle >, \geq\rangle$, $\langle =, \equiv\rangle$ and $\langle =, \mid \rangle$. An example of a sequence of mutually transitive logical operators is $\langle\iff,\implies\rangle$.
Given such a sequence we can often shorten our proofs by using the transitive chain notation $$ \begin{align*} x_1\,& r_{i_1}\, x_2 \\ & r_{i_2}\, x_3 \\ & r_{i_3}\, x_4 \\ & \vdots \\ & r_{i_k}\, x_{k+1} \end{align*} $$ which is defined to be an abbreviation for $$ \begin{align*} x_1\, & r_{i_1}\, x_2 \\ x_2\, & r_{i_2}\, x_3 \\ x_3\, & r_{i_3}\, x_4 \\ & \vdots \\ x_{k}\, & r_{i_k}\, x_{k+1} \end{align*} $$
Because the operators are mutually transitive we can use this entire block as a single premise to justify that $x_1 r_\alpha x_{k+1}$ where $\alpha$ is the largest subscript among $i_1,\ldots,i_k$. As a shortcut, any such deduction can be omitted and the entire block of lines used as in its place in the proof.
Example In the following transitive chain, the sequence of operators, $\langle =,\leq,<\rangle$, is mutually transitive. $$ \begin{align*} 0&\leq (a+1)^2 \\ &= a^2+2a+1 \\ &< (a^2+2a+1)+1 \\ &= a^2+2(a+1) \end{align*} $$
Thus, we can conclude from this transitive chain that $0<a^2+2(a+1)$.
Sometimes it is convenient to have more than one notation for the same expression. We will identify the following expressions.
| This expression… | …means the same thing as |
|---|---|
| $\xnot W$ | $\xnot W$ |
| $x\neq y$ | $\xnot (x=y)$ |
| $x\notin A$ | $\xnot (x\in A)$ |
| $f$ is not continuous | not ($f$ is continuous) |
| Let $x\in A$ | Let $x$ be such that $x\in A$ |