Logic for Mathematics

PDF link: https://pdf.gaomj.cn/?file=get.php?f=logic

Contents
Contents
1.  Logical languages
2.  Propositional Consequences
3.  Deductive Calculus
4.  Nonlogical Axioms

As we all know, modern mathematics can be “embedded” into set theory. In other words, virtually all mathematical objects—such as real numbers, functions, and so on --- can be viewed as sets, and mathematical theorems can be seen as theorems about sets. For example, in set theory, the natural number $1$ can be regarded as a set, and moreover $0 \in 1$ .

A reasonable claim is that sets are the most fundamental objects in mathematics, and set theory constitutes the bedrock of modern mathematics. Axiomatic set theory has effectively resolved the various paradoxes that arose from the crise in mathematics, rendering the basis of mathematics both elegantly simple and rock‑solid. (That said, for most mathematical work, there is no need to delve into the deep structures of set theory; it suffices to treat it as a black box. Often, the naive set theory is already adequate.)

If we regard mathematics as a language, set theory provides the underlying raw material --- the most basic words and symbols. But to speak eloquently, one must also follow grammar, and mathematical logic can supply this necessary “grammar.” Clearly, logic, like set theory, is also the foundation of mathematics.

Logic lies at the intersection of mathematics, philosophy, and computer science, and it can be studied from multiple perspectives. Here we focus on the part of mathematical logic that is required for the foundations of mathematics. (To be honest, it is not advisable to plunge into contemplation of these vertiginous elaborations.)

1. Logical languages

In mathematical logic a statement consists of some logical or mathematical symbols, some variables and punctuation signs (e.g., parentheses, but for readatibility some of them may be omitted), and must have finite length. In order to obtain meaningful statements, there are some syntax rules to obey.

The simpliest statements that are syntactically correct in mathematics are those called atomic formulas, e.g., $x\in\varnothing$ and $v=v$ , in which there is neither a connective symbol like $\vee$ , $\Rightarrow$ , nor a quantifier symbol like $\forall$ . Given some atomic formulas, we can build up the well--formed formulas, or simply formulas, by using symbols $\neg$ , $\vee$ , or $\forall$ : a well--formed formula is either an atomic formula or a formula in the following forms:
\[\neg \alpha,\quad \alpha\vee \beta,\quad \forall v \, \alpha,\]where $\alpha,\beta$ are well--formed formulas.

The other symbols can be derived from them: $\alpha\wedge \beta$ means $\neg(\neg \alpha\vee \neg \beta)$ , $\alpha\to \beta$ means $\neg \alpha\vee \beta$ , $\alpha\leftrightarrow \beta$ means $\alpha\to \beta$ and $\beta\to \alpha$ , and $\exists v\, \alpha$ means $\neg(\forall v\, \neg \alpha)$ . We will see that these symbols will mean what we expect them to mean. For logicians $\rightarrow$ may be preferred instead of $\Rightarrow$ , but it is not a good candidate for mathematics as there have been too many arrows in mathematical statements. Therefore, the symbol $\to$ is used as a connective only in this chapter, while $\Rightarrow$ is used to denote implication in the rest.

Among the formulas there are some in which we will be especially interested. For example, we may prefer $\exists x\, (\varnothing\in x)$ rather than $\varnothing\in x$ --- we can hardly say anything in the latter one since what $x$ represents is indeterminate. Variables of this kind are called free variables. Informally a free variable represents totally arbitrary objects. If $x$ is in the range/scope of a quantifier, it is called a bound variable. The variable $x$ in the example $\exists x\, (\varnothing\in x)$ is a bound variable. If a formula contains no free variables, it is called a sentence. Clearly, $\exists x\, (\varnothing\in x)$ is a sentence.

In mathematics, we start from a set of axioms, some of which are purely logical. In the following we denote the set of logical axioms by the letter $\Lambda$ . Given another set $\Gamma$ of formulas, we can obtain some theorems of $\Gamma$ --- the formulas that can be obtained from $\Gamma\cup\Lambda$ by some rules of inference (applied in finitely many times).

The choice of logical axioms and rules of inference are far from unique. Different choices can result in divergent consequences. One can develop the theory with very few axioms and a number of rules of inference. Here we adopt only one rule of inference that is traditionally called modus ponens --- From the formulas $\alpha$ and $\alpha\to\beta$ , the formula $\beta$ can be inferred. It is customary to denote by
\[\frac{\alpha,\alpha\to\beta}{\beta}.\]

2. Propositional Consequences

In this section we consider the case where there is no any quantifier. We adopt the following four axioms:
\begin{gather*}
\alpha\vee \alpha\to \alpha,\quad \alpha\to \alpha\vee \beta,\\
\alpha\vee \beta\to \beta\vee \alpha,\quad (\alpha\to \beta)\to(\alpha\vee \gamma\to \beta\vee \gamma).
\end{gather*}
It is said that these come from the Russell--Bernays axiom system.

An immediate consequence is that if we can deduce $\alpha$ , then by the axiom and modus ponens we have $\alpha\vee\beta$ . If we can deduce $\beta$ , then we have $\beta\vee\alpha$ , and by the axiom $\alpha\vee\beta$ . Hence we can deduce $\alpha\vee\beta$ from either $\alpha$ or $\beta$ . This explains the interpretation of the symbol $\vee$ as "or".

We can prove some useful results for deduction.

Proposition 1. For formulas

\alpha,\beta,\gamma

, if we can deduce

\alpha\to \beta

and

\beta\to \gamma

, then

\alpha\to \gamma

By applying the axiom, we have $(\beta\to \gamma)\to[(\beta\vee \neg \alpha)\to(\gamma\vee \neg \alpha)]$ . By assumption, $\beta\to \gamma$ can be deduced, so $(\beta\vee \neg \alpha)\to(\gamma\vee \neg \alpha)$ . We defined $\alpha\to \beta$ as $\neg \alpha\vee \beta$ , so by assumption we can deduce $\neg \alpha\vee \beta$ , and therefore $\beta\vee \neg \alpha$ . As $(\beta\vee \neg \alpha)\to(\gamma\vee \neg \alpha)$ , we infer $\gamma\vee\neg \alpha$ . Then $\neg \alpha\vee \gamma$ , which is just $\alpha\to \gamma$ . $\square$

Proposition 2. For any formula

\alpha

, we can deduce

\alpha\to \alpha

By the axioms, we have both of $\alpha\vee \alpha\to \alpha$ and $\alpha\to \alpha\vee \alpha$ . By the preceding proposition, from $\alpha\to (\alpha\vee \alpha)\to \alpha$ we can deduce $\alpha\to \alpha$ . $\square$

Corollary 3. For any formula

\alpha

, we can deduce

\alpha\vee\neg \alpha

. (Note that this does not indicate that we can deduce

\alpha

\neg\alpha

Proposition 4. For any statement

\alpha

, we can deduce

\alpha\leftrightarrow\neg(\neg \alpha)

By the preceding corollary, we can deduce $\neg \alpha\vee\neg(\neg \alpha)$ , so by definition of $\to$ , $\alpha\to\neg(\neg \alpha)$ .

Therefore, $\neg \alpha\to\neg(\neg(\neg \alpha))$ . Now by the axiom, $\neg \alpha\vee \alpha\to\neg(\neg(\neg \alpha)) \vee \alpha$ . By the preceding corollary and modus ponens, we have $\neg(\neg(\neg \alpha)) \vee \alpha$ , which means $\neg(\neg \alpha) \to \alpha$ . $\square$

Proposition 5 (Contrapositive). For formulas

\alpha,\beta

, we can deduce that

(\alpha\to \beta)\leftrightarrow(\neg \beta\to\neg \alpha)

. The formula

\neg \beta\to \neg \alpha

is called the contrapositive of

\alpha\to \beta

On the one hand we have $(\neg \alpha\vee \beta)\to(\beta\vee \neg \alpha)$ and $[\beta\to\neg(\neg \beta)]\to[\beta\vee \neg \alpha\to\neg(\neg \beta)\vee \neg \alpha]$ , by the axioms. By the preceding proposition, $\beta\to \neg(\neg \beta)$ , so $\beta\vee \neg \alpha\to\neg(\neg \beta)\vee \neg \alpha$ . Hence, $(\neg \alpha\vee \beta)\to(\neg(\neg \beta)\vee \neg \alpha)$ , which is just $(\alpha\to \beta)\to (\neg \beta\to\neg \alpha)$ by definition.

On the other hand, we have $(\beta\vee\neg \alpha)\to(\neg \alpha\vee \beta)$ and $[\neg(\neg \beta)\to \beta]\to[\neg(\neg \beta)\vee\neg \alpha\to \beta\vee\neg \alpha]$ . Then, similarly, we can deduce $(\neg(\neg \beta)\vee\neg \alpha)\to (\neg \alpha\vee \beta)$ , which means $(\neg \beta\to\neg \alpha)\to (\alpha\to \beta)$ . $\square$

Proposition 6. For formulas

\alpha,\beta

, we can deduce

\alpha\wedge \beta\to \alpha

and

\alpha\wedge \beta\to \beta

We have known the result $\alpha\vee\neg \alpha$ , as well as $\neg \alpha\vee \alpha$ . By the axiom, $\neg \alpha\to(\neg \alpha\vee \neg \beta)\to(\neg \beta\vee \neg \alpha)$ and $[\neg \alpha\to(\neg \beta\vee\neg \alpha)]\to[\neg \alpha\vee \alpha\to(\neg \beta\vee\neg \alpha)\vee \alpha]$ . Therefore $(\neg \beta\vee \neg \alpha)\vee \alpha$ . It is not difficult to obtain $\neg\neg(\neg \alpha\vee \neg \beta)\vee \alpha$ , which is $\neg(\alpha\wedge \beta)\vee \alpha$ , or $\alpha\wedge \beta\to \alpha$ . The other formula can be inferred immediately. $\square$

A formula $\alpha$ is said to be contradictory if we can deduce both $\alpha$ and $\neg\alpha$ . Of course we wish our axioms do not lead to any contradictory formulas. Suppose $\alpha$ is a contradictory formula and $\beta$ is another formula. By the axiom we have $\neg \alpha\to\neg \alpha\vee \beta$ , and since we are able to deduce $\neg \alpha$ by assumption, we have $\neg \alpha\vee \beta$ , or $\alpha\to \beta$ . By assumption again, we deduce $\beta$ . Since $\beta$ is arbitrary, $\neg \beta$ can also be deduced, which means $\beta$ is also contradictory. Thus every formula is contradictory provided there exists a contradictory formula.

This indicates the possibility of the method of proof by contradiction. If we can deduce $\neg \gamma\to \alpha$ and $\neg \gamma\to \neg \alpha$ , then we can infer $\gamma$ .

Proposition 7. We can deduce

(\alpha\to \beta)\longrightarrow[(\alpha\to\neg \beta)\to \neg \alpha]

By the property of contrapositive, $(\alpha\to \beta)\to(\neg \beta\to\neg \alpha)\to(\neg \beta\vee\neg \alpha\to\neg \alpha\vee\neg \alpha)\to(\neg \beta\vee \neg \alpha\to \neg \alpha)\to(\neg \alpha\vee\neg \beta\to\neg \alpha)$ . Thus $(\alpha\to \beta)\longrightarrow[(\alpha\to\neg \beta)\to\neg \alpha]$ . $\square$

Replacing $\alpha,\beta$ by $\neg \gamma,\alpha$ , we have $(\neg \gamma\to \alpha)\longrightarrow[(\neg \gamma\to\neg \alpha)\to \neg(\neg \gamma)]$ . If both $\neg \gamma\to \alpha$ and $\neg \gamma\to\neg \alpha$ are deducible, then $(\neg \gamma\to\neg \alpha)\to \neg(\neg \gamma)$ . Then from the assumption $\neg \gamma\to\neg \alpha$ we know $\neg(\neg \gamma)$ can be deduced, so can $\gamma$ .

The following proposition is also useful.

Proposition 8 (Associativity). For formulas

\alpha,\beta,\gamma

, we can deduce

(\alpha\vee\beta)\vee\gamma\leftrightarrow\alpha\vee(\beta\vee\gamma)

Consider the deduction:
\begin{gather*}
\alpha\to\alpha\vee\beta\to(\alpha\vee\beta)\vee\gamma,\\
\alpha\vee[(\alpha\vee\beta)\vee\gamma]\to[(\alpha\vee\beta)\vee\gamma]\vee[(\alpha\vee\beta)\vee\gamma]\to(\alpha\vee\beta)\vee\gamma,\\
\beta\to\beta\vee\alpha\to\alpha\vee\beta,\quad \beta\vee\gamma\to(\alpha\vee\beta)\vee\gamma,\\
\begin{aligned}
\alpha\vee(\beta\vee\gamma)&\to(\beta\vee\gamma)\vee\alpha\to[(\alpha\vee\beta)\vee\gamma]\vee\alpha\\
&\to \alpha\vee[(\alpha\vee\beta)\vee\gamma]\to(\alpha\vee\beta)\vee\gamma.
\end{aligned}
\end{gather*}This shows $\alpha\vee(\beta\vee\gamma)\to(\alpha\vee\beta)\vee\gamma$ . We then have
\begin{align*}
&(\alpha\vee\beta)\vee\gamma\to(\beta\vee\alpha)\vee\gamma\to\gamma\vee(\beta\vee\alpha)\\
\to{}& (\gamma\vee\beta)\vee\alpha\to(\beta\vee\gamma)\vee\alpha\to\alpha\vee(\beta\vee\gamma).
\end{align*}Thus $(\alpha\vee\beta)\vee\gamma\leftrightarrow\alpha\vee(\beta\vee\gamma)$ . $\square$

As an application, we show $\alpha\wedge \beta$ if we can deduce $\alpha,\beta$ .

Proposition 9. If we can deduce

\alpha

and

\beta

, then

\alpha\wedge \beta

is deducible. Thus,

\alpha\wedge \beta

if and only if

\alpha

and

\beta

Formally, it is deducible that $\alpha\to(\beta\to\alpha\wedge\beta)$ .

Proposition 10. If we can deduce

\neg\alpha

and

\neg\beta

, then

\neg(\alpha\vee \beta)

is deducible. Similarly,

\neg(\alpha\vee \beta)

if and only if

\neg\alpha

and

\neg\beta

Formally, it is deducible that $\neg\alpha\to(\neg\beta\to\neg(\alpha\vee \beta))$ .

These two propositions can be proved easily with the associativity of $\vee$ . We shall prove $\neg\alpha\vee[\neg\beta\vee\neg(\neg\alpha\vee\neg\beta)]$ . This can be deduced by applying modus ponens on $(\neg\alpha\vee\neg\beta)\vee\neg(\neg\alpha\vee\neg\beta)$ and the associativity of $\vee$ .

For the other proposition, we have $\neg\alpha\to(\neg\beta\to\neg\alpha\wedge\neg\beta)$ and $\neg\alpha\wedge\neg\beta\to\neg(\alpha\vee \beta)$ (not difficult to prove). The desired formula follows. $\square$

Proposition 11. For formulas

\alpha,\beta,\gamma

, if we can deduce all of the following three formulas:

\alpha\vee \beta

\alpha\to \gamma

\beta\to \gamma

, then we can deduce

\gamma

This proposition if useful for proof: we have known $\alpha\vee \neg \alpha$ , so to deduce $\gamma$ we can deduce $\alpha\to \gamma$ and $\neg \alpha\to \gamma$ .

Since $\alpha\to \gamma$ , $\alpha\vee \beta\to \gamma\vee \beta$ . By assumption, we can deduce $\alpha\vee \beta$ , so $\gamma\vee \beta$ can be deduced. Since $\beta\to \gamma$ , $\beta\vee \gamma\to \gamma\vee \gamma$ , so $\gamma\vee \gamma$ , as well as $\gamma$ , can be deduced. $\square$

3. Deductive Calculus The results obtained from the previous four axioms are called tautologies. In order to deduce the formulas involving quantifiers, some extra axioms are needed.

Consider the quantifier $\forall$ . What can we deduce from the formula $\forall x\, \alpha$ ? Intuitively if $\alpha$ is a formula involving $x$ we expect $\alpha$ is deducible for any object substituted for the variable $x$ . If we denote the formula with $x$ replaced by $t$ is $\alpha^x _ t$ , then it may be an axiom that $\forall x\, \alpha\to \alpha^x _ t$ .

But there are times when caution is warranted. Consider the example $\forall x\exists y\, x\neq y$ . This sentence holds if we are considering at least two objects, but the formula in $\forall$ with $x$ replaced by $y$ is $\exists y\, y\neq y$ . This example shows we should be careful with the substituting variable.

Let $x,t$ be two variables. We say that $t$ is substitutable for $x$ in $\alpha$ if:

$\alpha$ is atomic, or
$\alpha$ is $\neg\beta$ and $t$ is substitutable for $x$ in $\beta$ , or
$\alpha$ is $(\alpha _ 1\vee\alpha _ 2)$ and $t$ is substitutable for $x$ in both $\alpha _ 1$ and $\alpha _ 2$ , or
\alpha is \forall y\, \beta and either:
1. $x$ is not free in $\alpha$ , or
2. $y$ is $t$ and $t$ is substitutable for $x$ in $\beta$ .

With this definition, we can avoid the problem in the previous example.

Next, we consider the generalization. Assume with the axioms, we can deduce from a set $\Gamma$ of formulas a formula $\alpha$ . Can we generalize it to $\forall x\, \alpha$ ? Of course in the special case $\Sigma=\{\alpha\}$ , we cannot deduce $\forall x\, \alpha$ with only modus ponens. For example $x=\varnothing$ does not imply $\forall x\, (x=\varnothing)$ . A natural restriction is to impose that $x$ does not occur free in any formula in $\Gamma$ .

Suppose $\alpha$ is deduced from $\frac{\beta,\beta\to\alpha}{\alpha}$ . If we have $\forall x\, \beta$ and $\forall x\, (\beta\to\alpha)$ , then in order to deduce $\forall x\, \alpha$ , it can be assumed that $\forall x\, (\beta\to\alpha)\longrightarrow(\forall x\, \beta\to\forall x\, \alpha)$ . With these assumptions, $\forall x\, \alpha$ can be deduced by applying modus ponens twice.

Axioms

We can state the axioms for quantifiers now. Let $\alpha,\beta$ be two formulas and $x,t,v$ be three variables. Denote the formula $\alpha$ with $x$ replaced properly by $t$ as $\alpha^x _ t$ . The following are axioms:

If $t$ is substitutable for $x$ in $\alpha$ , then $\forall x\, \alpha\to \alpha^x _ t$ .
$\forall x\, (\alpha\to \beta)\longrightarrow(\forall x\, \alpha\to\forall x\, \beta)$ .
If $x$ does not occur free in $\alpha$ , then $\alpha\to\forall x\, \alpha$ .
If the formula $\varphi$ is an axiom, then so is its generalization $\forall v\, \varphi$ .

Proposition 12. If

t

is substitutable for

x

\alpha

, then it is deducible that

\alpha _ t^x\to\exists x\, \alpha

Since $\forall x\, \neg\alpha\to\neg\alpha _ t^x$ , by the property of contrapositive we can deduce $\neg(\neg \alpha _ t^x)\to \neg(\forall x\, \neg\alpha)$ . We have known $\alpha _ t^x\to\neg(\neg\alpha _ t^x)$ and $\neg(\forall x\, \neg\alpha)$ is just $\exists x\, \alpha$ , so we can deduce the desired result. $\square$

We next prove two important theorems for our deductive system, namely the generalization theorem and deduction theorem. Informally, the generalization theorem allows us to deduce $\forall x\, \alpha$ if we can deduce $\alpha$ without any special assumptions about $x$ , for the reason that " $x$ is arbitrary". The deduction theorem allows us to deduce an implication $\gamma\to\alpha$ if we can deduce $\alpha$ from $\gamma$ , which facilitates the application of modus ponens.

Theorem 13 (Generalization theorem). If from a set

\Gamma

of formulas we can deduce a formula

\varphi

, and

x

does not occur free in any formula in

\Gamma

, then we can deduce

\forall x\, \varphi

from

\Gamma

Theorem 14 (Deduction theorem). If from a set

\Gamma

of formulas and a formula

\gamma

we can deduce

\varphi

, then we can deduce

\gamma\to\varphi

from

\Gamma

We prove these two theorems by induction principle: Suppose $S$ is a set of formulas that contains $\Gamma\cup\Lambda$ and is closed under modus ponens. Then $S$ contains the set of all theorems of $\Gamma$ . Here we say $S$ is closed under modus ponens whenever $\alpha$ and $\alpha\to\beta$ are both in $S$ then $\beta\in S$ .

Remark: We have used the notations from set theory, but how can we? For now they are used for the purpose of readatibility. When we try to prove the two theorems, we shall ensure that there is an interpretation of string manipulations.

Suppose we can deduce $\varphi$ from $\Gamma$ and $\Lambda$ . The "deduction" consists of a sequence of formulas, the last of which is $\varphi$ . For any formula in this sequence, either it is from $\Gamma$ or $\Lambda$ , or deduced from two preceding formulas in the sequence by applying modus ponens. When $\varphi$ is from $\Gamma$ or $\Lambda$ , the sequence has length one.

If $\varphi$ is a logical axiom, then its generalization $\forall x\, \varphi$ is also an axiom. If $\varphi$ comes from $\Gamma$ , since we have assumed that $x$ does not occur free in any formula in $\Gamma$ , we can deduce $\varphi\to\forall x\, \varphi$ by the axiom, and then by applying modus ponens, we can deduce $\forall x\, \varphi$ .

If $\varphi$ is deduced from modus ponens, then we consider the deduction sequence from the beginning. Denote this sequence as $(\psi _ 1,\psi _ 2,\dots,\psi _ n=\varphi)$ . Suppose the first time we apply modus ponens is $\frac{\psi,\psi\to\psi'}{\psi'}$ . Then $\psi$ and $\psi\to\psi'$ both come from $\Gamma$ or $\Lambda$ . Thus, we can deduce their generalization $\forall x\, \psi$ and $\forall x\, (\psi\to\psi')$ . By the axiom, $\forall x\, (\psi\to \psi')\longrightarrow(\forall x\, \psi\to\forall x\, \psi')$ . Hence we deduce $\forall x\, \psi'$ by applying modus ponens twice. The similar argument applies to all later application of modus ponens. Finally we can deduce $\forall x\, \varphi$ .

The generalization theorem is proved. It is this theorem that motives us to introduce the two axioms in the axiom list (the second and the third one).

The deduction theorem is essentially the converse of modus ponens. Suppose $\varphi$ is a theorem of $\Gamma\cup\{\gamma\}$ . We want to show $\gamma\to\varphi$ is a theorem of $\Gamma$ . We prove the following lemma before the deduction theorem.

Lemma 15. From

\gamma\to\psi

and

\gamma\to(\psi\to\psi')

we can deduce

\gamma\to\psi'

We start from $\gamma\to(\psi\to\psi')$ , which is just $\neg\gamma\vee(\neg\psi\vee\psi')$ . By the associativity of $\vee$ and the axiom we can deduce $\neg\gamma\vee(\neg\psi\vee\psi')\to(\neg\gamma\vee\neg\psi)\vee\psi'\to(\neg\psi\vee\neg\gamma)\vee\psi'\to\neg\psi\vee(\neg\gamma\vee\psi')$ . From modus ponens $\neg\psi\vee(\neg\gamma\vee\psi')$ , or $\psi\to(\neg\gamma\vee\psi')$ , is deduced.

Then we have $\neg\gamma\vee\psi\to\psi\vee\neg\gamma\to (\neg\gamma\vee\psi')\vee\neg\gamma$ . Since we can deduce $\gamma\to\psi$ , which is $\neg\gamma\to\psi$ , we have $(\neg\gamma\vee\psi')\vee\neg\gamma$ , and also $\neg\gamma\vee(\neg\gamma\vee\psi')$ as $(\neg\gamma\vee\psi')\vee\neg\gamma\to\neg\gamma\vee(\neg\gamma\vee\psi')$ . Thus $\gamma\to\psi'$ . The lemma is proved.

We return to the deduction theorem. If $\varphi=\gamma$ , then we can deduce $\gamma\to\varphi$ since it is a tautology. If $\varphi$ is from $\Gamma$ or a logical axiom, then we can deduce $\varphi$ from $\Gamma$ , and then deduce $\gamma\to\varphi$ since $\varphi\to(\gamma\to\varphi)$ , or $\varphi\to(\neg\gamma\vee\varphi)$ , is a tautology.

If $\varphi$ is deduced from modus ponens, then we consider the deduction sequence $(\psi _ 1,\psi _ 2,\dots,\psi _ n=\varphi)$ . Suppose the first time we apply modus ponens is $\frac{\psi,\psi\to\psi'}{\psi'}$ . Then both $\psi$ and $\psi\to\psi'$ come from $\Gamma$ or $\Lambda$ . Thus, we can deduce the implication $\gamma\to\psi$ and $\gamma\to(\psi\to\psi')$ . By the lemma, we can deduce $\gamma\to\psi'$ . The similar argument applies to all later application of modus ponens. Finally we can deduce $\gamma\to\varphi$ . $\square$

In our deductive system, we have a slightly weak version of generalization theorem but have a strong version of deduction theorem. In the generalization theorem the variable $x$ is not allowed to be a free variable in any formula in $\Gamma$ , while in the deduction theorem $\gamma$ can be any well--formed formula. For example we cannot deduce $\forall x\, P(x)$ from $P(x)$ .

Some deductive systems are able to deduce $\forall x\, P(x)$ from $P(x)$ since they have a strong version of the generalization theorem. However they cannot deduce the implication $P(x)\to\forall x\, P(x)$ by deduction theorem, since there should be more restriction on the deduction theorem: the premise $\gamma$ must be a sentence.

A quick example of generalization theorem: We have known it is deducible that $P(x)\to\exists y\, P(y)$ . By generalization theorem, we can deduce $\forall x\, (P(x)\to\exists y\, P(y))$ .

We finally end this chapter with some propositions.

Proposition 16.

\forall x\, \neg \alpha\leftrightarrow\neg(\exists x\, \alpha)

By definition, $\neg(\exists x\, \alpha)$ means $\neg(\neg(\forall x\, \neg \alpha))$ , from which we immediately know $\forall x\, \neg \alpha\leftrightarrow\neg(\exists x\, \alpha)$ . $\square$

Proposition 17.

\forall x\, (\alpha\wedge \beta)\leftrightarrow (\forall x\, \alpha)\wedge (\forall x\, \beta)

Proposition 18.

\exists x\, (\alpha\vee \beta)\leftrightarrow (\exists x\, \alpha)\vee (\exists x\, \beta)

Note that we do not have the "dual": $\forall x\, (\alpha\vee \beta)\nleftrightarrow (\forall x\, \alpha)\vee (\forall x\, \beta)$ and $\exists x\, (\alpha\wedge \beta)\nleftrightarrow (\exists x\, \alpha)\wedge (\exists x\, \beta)$ .

In order to prove $\forall x\, (\alpha\wedge \beta)\leftrightarrow (\forall x\, \alpha)\wedge (\forall x\, \beta)$ , by deduction theorem we shall show $(\forall x\, \alpha)\wedge (\forall x\, \beta)$ from $\forall x\, (\alpha\wedge \beta)$ and the converse.

Suppose $\forall x\, (\alpha\wedge \beta)$ . By the axiom we have $\forall x\, (\alpha\wedge \beta)\to(\alpha\wedge\beta)$ (note that $\varphi^x _ x$ is $\varphi$ for any formula $\varphi$ ). By modus ponens, we have $\alpha\wedge\beta$ , and then $\alpha$ and $\beta$ . Since $x$ is a bound variable in the premise, by generalization theorem we can deduce $\forall x\, \alpha$ and $\forall x\, \beta$ , and therefore $(\forall x\, \alpha)\wedge (\forall x\, \beta)$ .

Next suppose $(\forall x\, \alpha)\wedge (\forall x\, \beta)$ and try to show $\forall x\, (\alpha\wedge \beta)$ . We can deduce $\forall x\, \alpha$ and $\forall x\, \beta$ . By the axiom and modus ponens we have $\alpha$ and $\beta$ , and hence $\alpha\wedge\beta$ . Since $x$ is a bound variable in the premise, by generalization theorem we can deduce $\forall x\, (\alpha\wedge \beta)$ .

Now we prove $\exists x\, (\alpha\vee \beta)\leftrightarrow (\exists x\, \alpha)\vee (\exists x\, \beta)$ . We have known $\neg(\alpha\vee\beta)$ if and only if $\neg\alpha$ and $\neg\beta$ , and by deduction theorem $\neg(\alpha\vee\beta)\leftrightarrow\neg\alpha\wedge\neg\beta$ . By generalization theorem $\forall x\, (\neg(\alpha\vee\beta)\leftrightarrow\neg\alpha\wedge\neg\beta)$ , and by the axiom and modus ponens, $\forall x\, \neg(\alpha\vee\beta)\leftrightarrow\forall x\, (\neg\alpha\wedge\neg\beta)$ . We can apply the preceding proposition, and deduce $\forall x\, \neg(\alpha\vee\beta)\leftrightarrow(\forall x\, \neg\alpha)\wedge(\forall x\, \neg\beta)$ . By contraposition, we have $\neg\forall x\, \neg(\alpha\vee\beta)\leftrightarrow\neg[(\forall x\, \neg\alpha)\wedge(\forall x\, \neg\beta)]$ .

We have just shown $\neg(\alpha\vee\beta)\leftrightarrow\neg\alpha\wedge\neg\beta$ . Replacing $\alpha,\beta$ by $\neg\alpha,\neg\beta$ respectively, we can show $\neg\alpha\vee\neg\beta\leftrightarrow\neg(\alpha\wedge\beta)$ without too much difficulty (detail omitted). With this result, we have $\neg\forall x\, \neg(\alpha\vee\beta)\leftrightarrow\neg[(\forall x\, \neg\alpha)\wedge(\forall x\, \neg\beta)]\leftrightarrow(\neg\forall x\neg\alpha)\vee(\neg\forall x\neg\beta)$ , which is just $\exists x\, (\alpha\vee \beta)\leftrightarrow (\exists x\, \alpha)\vee (\exists x\, \beta)$ .

The two propositions are proved. $\square$

Proposition 19. The following formulas are deducible:

$\forall x\forall y\, \alpha\leftrightarrow \forall y\forall x\, \alpha$ .
$\exists x\exists y\, \alpha\leftrightarrow \exists y\exists x\, \alpha$ .
$\exists x\forall y\, \alpha\to \forall y\exists x\, \alpha$ .
$\forall y\exists x\, \alpha\nrightarrow \exists x\forall y\, \alpha$ .

In calculus a definition may involve the $\varepsilon$ - $\delta$ statement in the form $(\forall \varepsilon>0)(\exists \delta>0)\, \alpha$ . By this proposition it can be seen the quantifiers cannot be swapped.

One quick counterexample: $\forall y\exists x\, (x=y)$ does not imply $\exists x\forall y\, (x=y)$ .

We now prove this proposition. In order to prove $\forall x\forall y\, \alpha\leftrightarrow \forall y\forall x\, \alpha$ it suffices to prove $\forall y\forall x\, \alpha$ from $\forall x\forall y\, \alpha$ , by deduction theorem. (Note that $\leftarrow$ follows immediately from $\rightarrow$ .) By the axiom, we can deduce $\alpha$ from $\forall x\forall y\, \alpha$ . By generalization theorem we then have $\forall y\forall x\, \alpha$ .

The second formula is not difficult to prove with the result of the first formula.

Finally we shall prove $\exists x\forall y\, \alpha\to \forall y\exists x\, \alpha$ . By deduction theorem consider to deduce $\forall y\exists x\, \alpha$ from $\exists x\forall y\, \alpha$ . By generalization theorem consider to deduce $\exists x\, \alpha$ from $\exists x\forall y\, \alpha$ , which means to deduce $\neg\forall x\neg\alpha$ from $\neg\forall x\neg\forall y\, \alpha$ . By modus ponens consider to deduce $\neg\forall x\neg\forall y\, \alpha\to\neg\forall x\, \neg\alpha$ , which can be obtained from $\forall x\, \neg\alpha\to \forall x\neg\forall y\, \alpha$ . By deduction theorem and generalization theorem consider to deduce from $\forall x\, \neg\alpha$ that $\neg\forall y\, \alpha$ . It suffices to deduce $\neg\alpha\to\neg\forall y\, \alpha$ , implied by $\forall y\, \alpha\to \alpha$ . $\square$

4. Nonlogical Axioms We have developed enough logic to do mathematics (there are some useful tautologies that have not been covered in the previous propositions, but they can be deduced from the four propositional axioms). In our deductive system, there are three fundamental symbols that are purely logical:
\[\vee,\quad\neg,\quad \forall.\]We adopt one rule of inference, modus ponens, and some logical axioms, constituting the set $\Lambda$ .

To construct mathematics, we need two extra symbols and the set $\Gamma$ of nonlogical axioms. What we do is essentially the manipulation of these symbols starting from $\Lambda\cup\Gamma$ . It is commonly said that mathematics can be "embedded" into set theory. The two extra symbols are the most fundamental two in set theory:
\[=,\quad \in,\]representing equality and membership respectively. Then we can precisely characterize the atomic formulas, i.e., the formulas in the form $x\in y$ or $x=y$ . (The equality symbol can also be a logical symbol, but here we treat it as a mathematical symbol characterized by the extensionality axiom.)

It is theoretically possible to write all mathematics using only the three logical symbols and the two mathematical symbols. For example, in natural language we say $A$ is a set, while in logical language it is $(A=\varnothing)\vee\exists a\, (a\in A)$ . Here the symbol $\varnothing$ is a notation that denotes the set in the empty set axiom. In spite of that possibility, it is impractical to restrict ourselves to using only the strictly formalized language.

Now the set $\Gamma$ of nonlogical axioms, i.e., the set of axioms in ZFC set theory, which will be introduced in later chapters, is listed in the following. In addition to the empty set $\varnothing$ , there are some other abbreviations, e.g., the inclusion $\subseteq$ , the mapping, and the successor $a^+$ for $a$ .

Axioms

$\forall A\forall B\, [\forall x\, (x\in A\leftrightarrow x\in B)\leftrightarrow A=B]$ . (Extensionality Axiom)
$\exists A\, \forall x\, (x\notin A)$ . (Empty Set Axiom)
$\forall A\forall B\, \exists C\, \forall x\, (x\in C\leftrightarrow x=A\vee x=B)$ . (Pairing Axiom)
$\forall S\, \exists B\, \forall x\,(x\in B\leftrightarrow (\exists A\in S)\, x\in A)$ . (Union Axiom)
$\forall A\, \exists B\, \forall x\, (x\in B\leftrightarrow x\subseteq A)$ . (Power Set Axiom)
$\forall A _ 1\dots\forall A _ n\forall A\, \exists B\, \forall x\, (x\in B\leftrightarrow (x\in A)\wedge P)$ .
Here $P$ is a formula not containing $B$ . (Subset Axioms)
$\forall A _ 1\dots\forall A _ n\forall A\quad[ (\forall x\in A)\forall y _ 1\forall y _ 2\, (\varphi(x,y _ 1)=\varphi(x,y _ 2)\rightarrow y _ 1=y _ 2)$
$\longrightarrow \exists B\, \forall y(y\in B\leftrightarrow (\exists x\in A)\varphi(x,y))]$ .
Here $\varphi(x,y)$ is a formula not containing $B$ . (Replacement Axioms)
$\forall A\forall I [\forall i\, [i \in I \to \exists a (a \in A(i))] \to \exists f\, \forall i ( i \in I \to f(i) \in A(i) )]$ .
Here $f$ is a mapping. (Choice Axiom)
$(\forall A\neq\varnothing)(\exists x\in A)\, x\cap A=\varnothing$ . (Regularity Axiom)
$\exists A\, [\varnothing\in A\wedge(\forall a\in A)\, a^+\in A]$ . (Infinity Axiom)

Logic for Mathematics

评论

发表回复取消回复

Logic for Mathematics

评论

发表回复 取消回复

发表回复取消回复