Theories and Their Models

Reading preferences

Optional display controls need JavaScript. All reading content and navigation work without it.

How to use Read

This page follows Theories and Their Models in source order. Every equation is native, unflattened MathML, and every source coordinate is available offline.

Four disclosed reader corrections

The frozen source and accepted projected transcript remain unchanged. These four reviewed interventions affect reader metadata, speech, and MathML only.

TR018-SOURCE-001: The final v sub two lacks the object-language marker used for every neighboring variable. The reader supplies that marker without changing the frozen source occurrence. Open the affected occurrence.
TR018-SOURCE-002: The extensionality row opens the scope of the z quantifier with a parenthesis instead of the square bracket required by the local quantifier macro. The reader restores the scope bracket. Open the affected occurrence.
TR018-SOURCE-003: At line 121, the source closes the universal-u implication before its aligned existential consequent; at line 123, it closes the universal-x implication before its aligned totality-and-uniqueness consequent. The reader groups both displayed consequents inside their respective universal implications without changing the frozen source. Open the affected occurrence.
TR018-SOURCE-004: The injectivity antecedent closes both universal scopes before the aligned existence clause. The reader groups that clause into the antecedent described by the following prose. Open the affected occurrence.

Introduction

Definition of a closed theory and its closure

A set of sentences $Γ$ source 29 is closed iff, whenever $Γ ⊨ A$ source 30 then $A \in Γ$ source 30. The closure of a set of sentences $Γ$ source 31 is ${A : Γ ⊨ A}$ source 31.

We say that $Γ$ source 33 is axiomatized by a set of sentences $Δ$ source 34 if $Γ$ source 34 is the closure of $Δ$ source 34.

source 28

Explanation

We can think of an axiomatic theory as the set of sentences that is axiomatized by its set of axioms $Δ$ source 39. In other words, when we have a first-order language which contains non-logical symbols for the primitives of the axiomatically developed science we wish to study, together with a set of sentences that express the fundamental laws of the science, we can think of the theory as represented by all the sentences in this language that are entailed by the axioms. This ranges from simple examples with only a single primitive and simple axioms, such as the theory of partial orders, to complex theories such as Newtonian mechanics.

The important logical facts that make this formal approach to the axiomatic method so important are the following. Suppose $Γ$ source 50 is an axiom system for a theory, i.e., a set of sentences.

We can state precisely when an axiom system captures an intended class of structures. That is, if we are interested in a certain class of structures, we will successfully capture that class by an axiom system $Γ$ source 56 iff the structures are exactly those $M$ source 57 such that $M ⊨ Γ$ source 57.
We may fail in this respect because there are $M$ source 58 such that $M ⊨ Γ$ source 59, but $M$ source 59 is not one of the structures we intend. This may lead us to add axioms which are not true in $M$ source 61.
If we are successful at least in the respect that $Γ$ source 62 is true in all the intended structures, then a sentence $A$ source 63 is true in all intended structures whenever $Γ ⊨ A$ source 64. Thus we can use logical tools (such as derivation methods) to show that sentences are true in all intended structures simply by showing that they are entailed by the axioms.
Sometimes we don't have intended structures in mind, but instead start from the axioms themselves: we begin with some primitives that we want to satisfy certain laws which we codify in an axiom system. One thing that we would like to verify right away is that the axioms do not contradict each other: if they do, there can be no concepts that obey these laws, and we have tried to set up an incoherent theory. We can verify that this doesn't happen by finding a model of $Γ$ source 75. And if there are models of our theory, we can use logical methods to investigate them, and we can also use logical methods to construct models.
The independence of the axioms is likewise an important question. It may happen that one of the axioms is actually a consequence of the others, and so is redundant. We can prove that an axiom $A$ source 81 in $Γ$ source 81 is redundant by proving $Γ ∖ {A} ⊨ A$ source 81. We can also prove that an axiom is not redundant by showing that $(Γ ∖ {A}) \cup {\neg A}$ source 83 is satisfiable. For instance, this is how it was shown that the parallel postulate is independent of the other axioms of geometry.
Another important question is that of definability of concepts in a theory: The choice of the language determines what the models of a theory consist of. But not every aspect of a theory must be represented separately in its models. For instance, every ordering $\leq$ source 90 determines a corresponding strict ordering $<$ source 90—given one, we can define the other. So it is not necessary that a model of a theory involving such an order must also contain the corresponding strict ordering. When is it the case, in general, that one relation can be defined in terms of others? When is it impossible to define a relation in terms of others (and hence must add it to the primitives of the language)?

Expressing Properties of Structures

Explanation

It is often useful and important to express conditions on functions and relations, or more generally, that the functions and relations in a structure satisfy these conditions. For instance, we would like to have ways of distinguishing those structures for a language which “capture” what we want the predicates to “mean” from those that do not. Of course we're completely free to specify which structures we “intend,” e.g., we can specify that the interpretation of the predicate $\leq$ source 21 must be an ordering, or that we are only interested in interpretations of $L$ source 22 in which the domain consists of sets and $\in$ source 23 is interpreted by the “is a element of” relation. But can we do this with sentences of the language? In other words, which conditions on a structure $M$ source 26 can we express by a sentence (or perhaps a set of sentences) in the language of $M$ source 27? There are some conditions that we will not be able to express. For instance, there is no sentence of $L_{A}$ source 29 which is only true in a structure $M$ source 30 if $| M | = ℕ$ source 30. We cannot express “the domain contains only natural numbers.” But there are “structural properties” of structures that we perhaps can express. Which properties of structures can we express by sentences? Or, to put it another way, which collections of structures can we describe as those making a sentence (or set of sentences) true?

Definition of a model of a sentence set

Source title: Model of a set.

Let $Γ$ source 40 be a set of sentences in a language $L$ source 40. We say that a structure $M$ source 41 is a model of $Γ$ source 41 if $M ⊨ A$ source 42 for all $A \in Γ$ source 42.

source 39

Example axiomatizing partial orders

The sentence $\forall x x \leq x$ source 46 is true in $M$ source 46 iff $\leq^{M}$ source 47 is a reflexive relation. The sentence $\forall x \forall y ((x \leq y \land y \leq x) \to x = y)$ source 48 is true in $M$ source 49 iff $\leq^{M}$ source 49 is anti-symmetric. The sentence $\forall x \forall y \forall z ((x \leq y \land y \leq z) \to x \leq z)$ source 50 is true in $M$ source 51 iff $\leq^{M}$ source 51 is transitive. Thus, the models of Displayed partial-order axioms $\begin{matrix} { & \forall x x \leq x, \\ \forall x \forall y ((x \leq y \land y \leq x) \to x = y), \\ \forall x \forall y \forall z ((x \leq y \land y \leq z) \to x \leq z)} \end{matrix}$ source 53 are exactly those structures in which $\leq^{M}$ source 60 is reflexive, anti-symmetric, and transitive, i.e., a partial order. Hence, we can take them as axioms for the first-order theory of partial orders.

source 45

Examples of First-Order Theories

Example theory of strict linear orders

The theory of strict linear orders in the language $L_{<}$ source 14 is axiomatized by the set Displayed strict-linear-order axioms $\begin{matrix} { & \forall x \neg x < x, \\ \forall x \forall y ((x < y \lor y < x) \lor x = y), \\ \forall x \forall y \forall z ((x < y \land y < z) \to x < z)} \end{matrix}$ source 16 It completely captures the intended structures: every strict linear order is a model of this axiom system, and vice versa, if $R$ source 24 is a linear order on a set $X$ source 25, then the structure $M$ source 25 with $| M | = X$ source 26 and $<^{M} = R$ source 26 is a model of this theory.

source 13

Example theory of groups

The theory of groups in the language $1$ source 30 (constant), $\cdot$ source 30 (two-place function) is axiomatized by Displayed group axioms $\begin{matrix} \forall x (x \cdot 1) = x \\ \forall x \forall y \forall z (x \cdot (y \cdot z)) = ((x \cdot y) \cdot z) \\ \forall x \exists y (x \cdot y) = 1 \end{matrix}$ source 32

source 29

Example Peano arithmetic

The theory of Peano arithmetic is axiomatized by the following sentences in the language of arithmetic $L_{A}$ source 42. Displayed Peano-arithmetic axioms $\begin{matrix} \forall x \forall y (x^{'} = y^{'} \to x = y) \\ \forall x 0 \neq x^{'} \\ \forall x (x + 0) = x \\ \forall x \forall y (x + y^{'}) = {(x + y)}^{'} \\ \forall x (x \times 0) = 0 \\ \forall x \forall y (x \times y^{'}) = ((x \times y) + x) \\ \forall x \forall y (x < y \leftrightarrow \exists z (z^{'} + x) = y) \\ plus all sentences of the form & (A (0) \land \forall x (A (x) \to A (x^{'}))) \to \forall x A (x) \end{matrix}$ source 43 Since there are infinitely many sentences of the latter form, this axiom system is infinite. The latter form is called the induction schema. (Actually, the induction schema is a bit more complicated than we let on here.)

The last axiom is an explicit definition of $<$ source 59.

source 40

Example candidate theory of pure sets

The theory of pure sets plays an important role in the foundations (and in the philosophy) of mathematics. A set is pure if all its elements are also pure sets. The empty set counts therefore as pure, but a set that has something as a element that is not a set would not be pure. So the pure sets are those that are formed just from the empty set and no “urelements,” i.e., objects that are not themselves sets.

The following might be considered as an axiom system for a theory of pure sets: Displayed pure-set axioms $\begin{matrix} \exists x \neg \exists y y \in x \\ \forall x \forall y (\forall z (z \in x \leftrightarrow z \in y) \to x = y) \\ \forall x \forall y \exists z \forall u (u \in z \leftrightarrow (u = x \lor u = y)) \\ \forall x \exists y \forall z (z \in y \leftrightarrow \exists u (z \in u \land u \in x)) \\ plus all sentences of the form & \exists x \forall y (y \in x \leftrightarrow A (y)) \end{matrix}$ source 73 Reader correction: The extensionality row opens the scope of the z quantifier with a parenthesis instead of the square bracket required by the local quantifier macro. The reader restores the scope bracket. The first axiom says that there is a set with no elements (i.e., $\emptyset$ source 85 exists); the second says that sets are extensional; the third that for any sets $X$ source 86 and $Y$ source 86, the set ${X, Y}$ source 86 exists; the fourth that for any set $X$ source 87, the set $\cup X$ source 87 exists, where $\cup X$ source 87 is the union of all the elements of $X$ source 88.

The sentences mentioned last are collectively called the naive comprehension scheme. It essentially says that for every $A (x)$ source 92, the set ${x : A (x)}$ source 92 exists—so at first glance a true, useful, and perhaps even necessary axiom. It is called “naive” because, as it turns out, it makes this theory unsatisfiable: if you take $A (y)$ source 95 to be $\neg y \in y$ source 95, you get the sentence $\exists x \forall y (y \in x \leftrightarrow \neg y \in y)$ source 96 and this sentence is not satisfied in any structure.

source 62

Example theory of mereological parthood

In the area of mereology, the relation of parthood is a fundamental relation. Just like theories of sets, there are theories of parthood that axiomatize various conceptions (sometimes conflicting) of this relation.

The language of mereology contains a single two-place predicate symbol $P$ source 109, and $P (x, y)$ source 109 “means” that $x$ source 109 is a part of $y$ source 110. When we have this interpretation in mind, a structure for this language is called a parthood structure. Of course, not every structure for a single two-place predicate will really deserve this name. To have a chance of capturing “parthood,” $P^{M}$ source 114 must satisfy some conditions, which we can lay down as axioms for a theory of parthood. For instance, parthood is a partial order on objects: every object is a part (albeit an improper part) of itself; no two different objects can be parts of each other; a part of a part of an object is itself part of that object. Note that in this sense “is a part of” resembles “is a subset of,” but does not resemble “is an element of” which is neither reflexive nor transitive. Displayed mereology axioms $\begin{matrix} \forall x P (x, x) \\ \forall x \forall y ((P (x, y) \land P (y, x)) \to x = y) \\ \forall x \forall y \forall z ((P (x, y) \land P (y, z)) \to P (x, z)) \\ Moreover, any two objects have a mereological sum (an object that has these two objects as parts, and is minimal in this respect). & \forall x \forall y \exists z \forall u (P (z, u) \leftrightarrow (P (x, u) \land P (y, u))) \end{matrix}$ source 122 These are only some of the basic principles of parthood considered by metaphysicians. Further principles, however, quickly become hard to formulate or write down without first introducing some defined relations. For instance, most metaphysicians interested in mereology also view the following as a valid principle: whenever an object $x$ source 138 has a proper part $y$ source 138, it also has a part $z$ source 138 that has no parts in common with $y$ source 139, and so that the fusion of $y$ source 139 and $z$ source 139 is $x$ source 140.

source 102

Expressing Relations in a Structure

Explanation

One main use formulas can be put to is to express properties and relations in a structure $M$ source 16 in terms of the primitives of the language $L$ source 17 of $M$ source 17. By this we mean the following: the domain of $M$ source 18 is a set of objects. The constants, functions, and predicates are interpreted in $M$ source 19 by some objects in $| M |$ source 20, functions on $| M |$ source 20, and relations on $| M |$ source 21. For instance, if ${A^{2}}_{0}$ source 21 is in $L$ source 21, then $M$ source 22 assigns to it a relation $R = {A^{2}}_{0}^{M}$ source 22. Then the formula ${A^{2}}_{0} (v_{1}, v_{2})$ source 23 expresses that very relation, in the following sense: if a variable assignment $s$ source 25 maps $v_{1}$ source 25 to $a \in | M |$ source 25 and $v_{2}$ source 26 to $b \in | M |$ source 26, then $R a b iff M, s ⊨ {A^{2}}_{0} (v_{1}, v_{2}) .$ source 27 Note that we have to involve variable assignments here: we can't just say “ $R a b$ source 31 iff $M ⊨ {A^{2}}_{0} (a, b)$ source 31” because $a$ source 31 and $b$ source 32 are not symbols of our language: they are elements of $| M |$ source 33.

Since we don't just have atomic formulas, but can combine them using the logical connectives and the quantifiers, more complex formulas can define other relations which aren't directly built into $M$ source 38. We're interested in how to do that, and specifically, which relations we can define in a structure.

Definition of a formula expressing a relation

Let $A (v_{1}, \dots, v_{n})$ source 43 be a formula of $L$ source 43 in which only $v_{1}$ source 44,…, $v_{n}$ source 44 occur free, and let $M$ source 44 be a structure for $L$ source 45. $A (v_{1}, \dots, v_{n})$ source 45 expresses the relation $R \subseteq {| M |}^{n}$ source 46 iff $R a_{1} \dots a_{n} iff M, s ⊨ A (v_{1}, \dots, v_{n})$ source 47 for any variable assignment $s$ source 51 with $s (v_{i}) = a_{i}$ source 51 ( $i = 1, \dots, n$ source 51).

source 42

Example definable arithmetic relations

In the standard model of arithmetic $N$ source 56, the formula $v_{1} < v_{2} \lor v_{1} = v_{2}$ source 56 expresses the $\leq$ source 57 relation on $ℕ$ source 58. The formula $v_{2} = {v_{1}}^{'}$ source 58 expresses the successor relation, i.e., the relation $R \subseteq ℕ^{2}$ source 59 where $R n m$ source 60 holds if $m$ source 60 is the successor of $n$ source 60. The formula $v_{1} = {v_{2}}^{'}$ source 61 expresses the predecessor relation. The formulas $\exists v_{3} (v_{3} \neq 0 \land v_{2} = (v_{1} + v_{3}))$ source 62 and $\exists v_{3} (v_{1} + {v_{3}}^{'}) = v_{2}$ source 63 Reader correction: The final v sub two lacks the object-language marker used for every neighboring variable. The reader supplies that marker without changing the frozen source occurrence. both express the $<$ source 64 relation. This means that the predicate symbol $<$ source 65 is actually superfluous in the language of arithmetic; it can be defined.

source 55

Exercise defining arithmetic relations

Unsolved exercise. The source supplies the prompt only; no solution is added.

Find formulas in $L_{A}$ source 81 which define the following relations:

$n$ source 83 is between $i$ source 83 and $j$ source 83;
$n$ source 84 evenly divides $m$ source 84 (i.e., $m$ source 84 is a multiple of $n$ source 84);
$n$ source 85 is a prime number (i.e., no number other than $1$ source 85 and $n$ source 85 evenly divides $n$ source 86).

source 80

Exercise transforming an expressed relation

Unsolved exercise. The source supplies the prompt only; no solution is added.

Suppose the formula $A (v_{1}, v_{2})$ source 91 expresses the relation $R \subseteq {| M |}^{2}$ source 91 in a structure $M$ source 92. Find formulas that express the following relations:

the inverse $R^{- 1}$ source 95 of $R$ source 95;
the relative product $R | R$ source 96;

Can you find a way to express $R^{+}$ source 98, the transitive closure of $R$ source 98?

source 90

Exercise on definability in the natural-number order

Unsolved exercise. The source supplies the prompt only; no solution is added.

Let $L$ source 102 be the language containing a 2-place predicate symbol $<$ source 103 only (no other constants, functions or predicates— except of course $=$ source 104). Let $N$ source 104 be the structure such that $| N | = ℕ$ source 105, and $<^{N} = {⟨ n, m ⟩ : n < m}$ source 105. Prove the following:

${0}$ source 108 is definable in $N$ source 108;
${1}$ source 109 is definable in $N$ source 109;
${2}$ source 110 is definable in $N$ source 110;
for each $n \in ℕ$ source 111, the set ${n}$ source 111 is definable in $N$ source 112;
every finite subset of $| N |$ source 113 is definable in $N$ source 114;
every co-finite subset of $| N |$ source 115 is definable in $N$ source 116 (where $X \subseteq ℕ$ source 116 is co-finite iff $ℕ ∖ X$ source 117 is finite).

source 101

The Theory of Sets

Almost all of mathematics can be developed in the theory of sets. Developing mathematics in this theory involves a number of things. First, it requires a set of axioms for the relation $\in$ source 15. A number of different axiom systems have been developed, sometimes with conflicting properties of $\in$ source 17. The axiom system known as $ZFC$ source 18, Zermelo–Fraenkel set theory with the axiom of choice stands out: it is by far the most widely used and studied, because it turns out that its axioms suffice to prove almost all the things mathematicians expect to be able to prove. But before that can be established, it first is necessary to make clear how we can even express all the things mathematicians would like to express. For starters, the language contains no constants or functions, so it seems at first glance unclear that we can talk about particular sets (such as $\emptyset$ source 26 or $ℕ$ source 26), can talk about operations on sets (such as $X \cup Y$ source 27 and $℘ (X)$ source 27), let alone other constructions which involve things other than sets, such as relations and functions.

To begin with, “is an element of” is not the only relation we are interested in: “is a subset of” seems almost as important. But we can define “is a subset of” in terms of “is an element of.” To do this, we have to find a formula $A (x, y)$ source 34 in the language of set theory which is satisfied by a pair of sets $⟨ X, Y ⟩$ source 36 iff $X \subseteq Y$ source 36. But $X$ source 36 is a subset of $Y$ source 36 just in case all elements of $X$ source 37 are also elements of $Y$ source 37. So we can define $\subseteq$ source 38 by the formula $\forall z (z \in x \to z \in y)$ source 39 Now, whenever we want to use the relation $\subseteq$ source 42 in a formula, we could instead use that formula (with $x$ source 43 and $y$ source 43 suitably replaced, and the bound variable $z$ source 44 renamed if necessary). For instance, extensionality of sets means that if any sets $x$ source 45 and $y$ source 45 are contained in each other, then $x$ source 46 and $y$ source 46 must be the same set. This can be expressed by $\forall x \forall y ((x \subseteq y \land y \subseteq x) \to x = y)$ source 47, or, if we replace $\subseteq$ source 48 by the above definition, by $\forall x \forall y ((\forall z (z \in x \to z \in y) \land \forall z (z \in y \to z \in x)) \to x = y) .$ source 50 This is in fact one of the axioms of $ZFC$ source 54, the “axiom of extensionality.”

There is no constant for $\emptyset$ source 57, but we can express “ $x$ source 57 is empty” by $\neg \exists y y \in x$ source 58. Then “ $\emptyset$ source 58 exists” becomes the sentence $\exists x \neg \exists y y \in x$ source 59. This is another axiom of $ZFC$ source 60. (Note that the axiom of extensionality implies that there is only one empty set.) Whenever we want to talk about $\emptyset$ source 62 in the language of set theory, we would write this as “there is a set that's empty and …” As an example, to express the fact that $\emptyset$ source 64 is a subset of every set, we could write $\exists x (\neg \exists y y \in x \land \forall z x \subseteq z)$ source 66 where, of course, $x \subseteq z$ source 70 would in turn have to be replaced by its definition.

To talk about operations on sets, such as $X \cup Y$ source 73 and $℘ (X)$ source 73, we have to use a similar trick. There are no function symbols in the language of set theory, but we can express the functional relations $X \cup Y = Z$ source 75 and $℘ (X) = Y$ source 76 by Displayed definitions of union and power set $\begin{matrix} \forall u ((u \in x \lor u \in y) \leftrightarrow u \in z) \\ \forall u (u \subseteq x \leftrightarrow u \in y) \end{matrix}$ source 77 since the elements of $X \cup Y$ source 81 are exactly the sets that are either elements of $X$ source 82 or elements of $Y$ source 82, and the elements of $℘ (X)$ source 83 are exactly the subsets of $X$ source 83. However, this doesn't allow us to use $x \cup y$ source 84 or $℘ (x)$ source 84 as if they were terms: we can only use the entire formulas that define the relations $X \cup Y = Z$ source 86 and $℘ (X) = Y$ source 86. In fact, we do not know that these relations are ever satisfied, i.e., we do not know that unions and power sets always exist. For instance, the sentence $\forall x \exists y ℘ (x) = y$ source 89 is another axiom of $ZFC$ source 90 (the power set axiom).

Now what about talk of ordered pairs or functions? Here we have to explain how we can think of ordered pairs and functions as special kinds of sets. One way to define the ordered pair $⟨ x, y ⟩$ source 94 is as the set ${{x}, {x, y}}$ source 95. But like before, we cannot introduce a function that names this set; we can only define the relation $⟨ x, y ⟩ = z$ source 97, i.e., ${{x}, {x, y}} = z$ source 97: $\forall u (u \in z \leftrightarrow (\forall v (v \in u \leftrightarrow v = x) \lor \forall v (v \in u \leftrightarrow (v = x \lor v = y))))$ source 98 This says that the elements $u$ source 102 of $z$ source 102 are exactly those sets which either have $x$ source 103 as its only element or have $x$ source 103 and $y$ source 103 as its only elements (in other words, those sets that are either identical to ${x}$ source 105 or identical to ${x, y}$ source 105). Once we have this, we can say further things, e.g., that $X \times Y = Z$ source 106: $\forall z (z \in Z \leftrightarrow \exists x \exists y (x \in X \land y \in Y \land ⟨ x, y ⟩ = z))$ source 107

A function $f : X \to Y$ source 112 can be thought of as the relation $f (x) = y$ source 112, i.e., as the set of pairs ${⟨ x, y ⟩ : f (x) = y}$ source 113. We can then say that a set $f$ source 114 is a function from $X$ source 114 to $Y$ source 114 if (a) it is a relation $\subseteq X \times Y$ source 115, (b) it is total, i.e., for all $x \in X$ source 115 there is some $y \in Y$ source 116 such that $⟨ x, y ⟩ \in f$ source 116 and (c) it is functional, i.e., whenever $⟨ x, y ⟩, ⟨ x, y^{'} ⟩ \in f$ source 117, $y = y^{'}$ source 118 (because values of functions must be unique). So “ $f$ source 118 is a function from $X$ source 119 to $Y$ source 119” can be written as: Displayed definition of a function graph $\forall u (u \in f \to \exists x \exists y (x \in X \land y \in Y \land ⟨ x, y ⟩ = u)) \land \forall x (x \in X \to (\exists y (y \in Y \land maps (f, x, y)) \land \forall y \forall y^{'} ((maps (f, x, y) \land maps (f, x, y^{'})) \to y = y^{'})))$ source 120 Reader correction: At line 121, the source closes the universal-u implication before its aligned existential consequent; at line 123, it closes the universal-x implication before its aligned totality-and-uniqueness consequent. The reader groups both displayed consequents inside their respective universal implications without changing the frozen source. where $maps (f, x, y)$ source 128 abbreviates $\exists v (v \in f \land ⟨ x, y ⟩ = v)$ source 128 (this formula expresses “ $f (x) = y$ source 129”).

It is now also not hard to express that $f : X \to Y$ source 131 is injective, for instance: Displayed definition of injectivity $f : X \to Y \land \forall x \forall x^{'} (((x \in X \land x^{'} \in X) \land \exists y (maps (f, x, y) \land maps (f, x^{'}, y))) \to x = x^{'})$ source 133 Reader correction: The injectivity antecedent closes both universal scopes before the aligned existence clause. The reader groups that clause into the antecedent described by the following prose. A function $f : X \to Y$ source 139 is injective iff, whenever $f$ source 139 maps $x, x^{'} \in X$ source 139 to a single $y$ source 140, $x = x^{'}$ source 140. If we abbreviate this formula as $inj (f, X, Y)$ source 141, we're already in a position to state in the language of set theory something as non-trivial as Cantor's theorem: there is no injective function from $℘ (X)$ source 143 to $X$ source 143: $\forall X \forall Y (℘ (X) = Y \to \neg \exists f inj (f, Y, X))$ source 144

One might think that set theory requires another axiom that guarantees the existence of a set for every defining property. If $A (x)$ source 150 is a formula of set theory with the variable $x$ source 151 free, we can consider the sentence $\exists y \forall x (x \in y \leftrightarrow A (x)) .$ source 153 This sentence states that there is a set $y$ source 156 whose elements are all and only those $x$ source 157 that satisfy $A (x)$ source 157. This schema is called the “comprehension principle.” It looks very useful; unfortunately it is inconsistent. Take $A (x) \equiv \neg x \in x$ source 159, then the comprehension principle states $\exists y \forall x (x \in y \leftrightarrow x \notin x),$ source 161 i.e., it states the existence of a set of all sets that are not elements of themselves. No such set can exist—this is Russell's Paradox. $ZFC$ source 166, in fact, contains a restricted—and consistent—version of this principle, the separation principle: $\forall z \exists y \forall x (x \in y \leftrightarrow (x \in z \land A (x)) .$ source 168

Exercise deriving Russell's contradiction

Unsolved exercise. The source supplies the prompt only; no solution is added.

Show that the comprehension principle is inconsistent by giving a derivation that shows $\exists y \forall x (x \in y \leftrightarrow x \notin x) ⊢ ⊥ .$ source 176 It may help to first show $(A \to \neg A) \land (\neg A \to A) ⊢ ⊥$ source 179.

source 173

Expressing the Size of Structures

Proposition expressing at least and at most n elements

The sentence Displayed sentence for at least n elements $\begin{matrix} A_{\geq n} \equiv \exists x_{1} \exists x_{2} \dots \exists x_{n} \\ \begin{matrix} (x_{1} \neq x_{2} \land x_{1} \neq x_{3} \land x_{1} \neq x_{4} \land \dots \land x_{1} \neq x_{n} \land \\ x_{2} \neq x_{3} \land x_{2} \neq x_{4} \land \dots \land x_{2} \neq x_{n} \land \\ ⋮ \\ x_{n - 1} \neq x_{n}) \end{matrix} \end{matrix}$ source 23 is true in a structure $M$ source 33 iff $| M |$ source 33 contains at least $n$ source 34 elements. Consequently, $M ⊨ \neg A_{\geq n + 1}$ source 34 iff $| M |$ source 35 contains at most $n$ source 35 elements.

source 21

Proposition expressing exactly n elements

The sentence Displayed sentence for exactly n elements $\begin{matrix} A_{= n} \equiv \exists x_{1} \exists x_{2} \dots \exists x_{n} \\ \begin{matrix} (x_{1} \neq x_{2} \land x_{1} \neq x_{3} \land x_{1} \neq x_{4} \land \dots \land x_{1} \neq x_{n} \land \\ x_{2} \neq x_{3} \land x_{2} \neq x_{4} \land \dots \land x_{2} \neq x_{n} \land \\ ⋮ \\ x_{n - 1} \neq x_{n} \land \\ \forall y (y = x_{1} \lor \dots \lor y = x_{n})) \end{matrix} \end{matrix}$ source 41 is true in a structure $M$ source 52 iff $| M |$ source 52 contains exactly $n$ source 53 elements.

source 39

Proposition characterizing infinite structures

A structure is infinite iff it is a model of ${A_{\geq 1}, A_{\geq 2}, A_{\geq 3}, \dots} .$ source 58

source 56

There is no single purely logical sentence which is true in $M$ source 63 iff $| M |$ source 64 is infinite. However, one can give sentences with non-logical predicates which only have infinite models (although not every infinite structure is a model of them). The property of being a finite structure, and the property of being a nonenumerable structure cannot even be expressed with an infinite set of sentences. These facts follow from the compactness and Löwenheim–Skolem theorems.