Main Lectures in Logic and Set Theory. Volume 2: Set Theory

# Lectures in Logic and Set Theory. Volume 2: Set Theory

Volume II, on formal (ZFC) set theory, incorporates a self-contained "chapter 0" on proof techniques so that it is based on formal logic, in the style of Bourbaki. The emphasis on basic techniques provides a solid foundation in set theory and a thorough context for the presentation of advanced topics (such as absoluteness, relative consistency results, two expositions of Godel's construstive universe, numerous ways of viewing recursion and Cohen forcing).
Categories: Mathematics\\Logic
Year: 2003
Language: english
Pages: 575
ISBN 10: 0521753740
ISBN 13: 9780521753746
Series: Cambridge Studies in Advanced Mathematics 83
File: PDF, 2.13 MB

## You may be interested in

### Lectures in Logic and Set Theory. Volume 1: Mathematical Logic

Year: 2003
Language: english
File: PDF, 1.38 MB

Post a Review You can write a book review and share your experiences. Other readers will always be interested in your opinion of the books you've read. Whether you've loved the book or not, if you give your honest and detailed thoughts then people will find new books that are right for them.
1

### Mathematical Logic

Year: 2008
Language: english
File: DJVU, 2.16 MB
2

### Lectures in Logic and Set Theory. Volume 1: Mathematical Logic

Year: 2003
Language: english
File: PDF, 1.38 MB
```This page intentionally left blank

CAMBRIDGE STUDIES IN
EDITORIAL BOARD
B. BOLLOBAS, W. FULTON, A. KATOK, F. KIRWAN,
P. SARNAK
Lectures in Logic and Set Theory Volume 2
This two-volume work bridges the gap between introductory expositions of
logic or set theory on one hand, and the research literature on the other. It can
be used as a text in an advanced undergraduate or beginning graduate course
in mathematics, computer science, or philosophy. The volumes are written in
a user-friendly conversational lecture style that makes them equally effective
for self-study or class use.
Volume 2, on formal (ZFC) set theory, incorporates a self-contained
“Chapter 0” on proof techniques so that it is based on formal logic, in the style
of Bourbaki. The emphasis on basic techniques will provide the reader with
a solid foundation in set theory and sets a context for the presentation of advanced topics such as absoluteness, relative consistency results, two expositions of Gödel’s constructible universe, numerous ways of viewing recursion,
and a chapter on Cohen forcing.
George Tourlakis is Professor of Computer Science at York University of
Ontario.

2
3
5
7
8
10
11
12
14
15
16
17
19
20
21
22
24
25
26
27
28
29
30
31
32
33
34
35
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73

K. Petersen Ergodic theory
P.T. Johnstone Stone spaces
J.-P. Kahane Some random series of functions, 2nd edition
J. Lambek & P.J. Scott Introduction to higher-order categorical logic
H. Matsumura Commutative ring theory
M. Aschbacher Finite group theory, 2nd edition
J.L. Alperin Local representation theory
P. Koosis The logarithmic integral I
S.J. Patterson An introduction to the theory of the Riemann zeta-function
H.J. Baues Algebraic homotopy
V.S. Varadarajan Introduction to harmonic analysis on semisimple Lie groups
W. Dicks & M. Dunwoody Groups acting on graphs
R. Fritsch & R. Piccinini Cellular structures in topology
H. Klingen Introductory lectures on Siegel modular forms
P. Koosis The logarithmic integral II
M.J. Collins Representations and characters of ﬁnite groups
H. Kunita Stochastic ﬂows and stochastic differential equations
P. Wojtaszczyk Banach spaces for analysts
J.E. Gilbert & M.A.M. Murray Clifford algebras and Dirac operators in harmonic analysis
A. Frohlich & M.J. Taylor Algebraic number theory
K. Goebel & W.A. Kirk Topics in metric ﬁxed point theory
J.F. Humphreys Reﬂection groups and Coxeter groups
D.J. Benson Representations and cohomology I
D.J. Benson Representations and cohomology II
C. Allday & V. Puppe Cohomological methods in transformation groups
C. Soule et al. Lectures on Arakelov geometry
A. Ambrosetti & G. Prodi A primer of nonlinear analysis
J. Palis & F. Takens Hyperbolicity, stability and chaos at homoclinic bifurcations
Y. Meyer Wavelets and operators 1
C. Weibel, An introduction to homological algebra
W. Bruns & J. Herzog Cohen-Macaulay rings
V. Snaith Explicit Brauer induction
G. Laumon Cohomology of Drinfeld modular varieties I
E.B. Davies Spectral theory and differential operators
J. Diestel, H. Jarchow, & A. Tonge Absolutely summing operators
P. Mattila Geometry of sets and measures in Euclidean spaces
R. Pinsky Positive harmonic functions and diffusion
G. Tenenbaum Introduction to analytic and probabilistic number theory
C. Peskine An algebraic introduction to complex projective geometry
Y. Meyer & R. Coifman Wavelets
R. Stanley Enumerative combinatorics I
I. Porteous Clifford algebras and the classical groups
M. Audin Spinning tops
V. Jurdjevic Geometric control theory
H. Volklein Groups as Galois groups
J. Le Potier Lectures on vector bundles
D. Bump Automorphic forms and representations
G. Laumon Cohomology of Drinfeld modular varieties II
D.M. Clark & B.A. Davey Natural dualities for the working algebraist
J. McCleary A user’s guide to spectral sequences II
P. Taylor Practical foundations of mathematics
M.P. Brodmann & R.Y. Sharp Local cohomology
J.D. Dixon et al. Analytic pro-P groups
R. Stanley Enumerative combinatorics II
R.M. Dudley Uniform central limit theorems
J. Jost & X. Li-Jost Calculus of variations
A.J. Berrick & M.E. Keating An introduction to rings and modules
S. Morosawa Holomorphic dynamics
A.J. Berrick & M.E. Keating Categories and modules with K-theory in view
K. Sato Levy processes and inﬁnitely divisible distributions
H. Hida Modular forms and Galois cohomology
R. Iorio & V. Iorio Fourier analysis and partial differential equations
R. Blei Analysis in integer and fractional dimensions
F. Borceaux & G. Janelidze Galois theories
B. Bollobas Random graphs

LECTURES IN LOGIC
AND SET THEORY
Volume 2: Set Theory

GEORGE TOURLAKIS
York University

  
Cambridge, New York, Melbourne, Madrid, Cape Town, Singapore, São Paulo
Cambridge University Press
The Edinburgh Building, Cambridge  , United Kingdom
Published in the United States by Cambridge University Press, New York
www.cambridge.org
Information on this title: www.cambridge.org/9780521753746
© George Tourlakis 2003
This book is in copyright. Subject to statutory exception and to the provision of
relevant collective licensing agreements, no reproduction of any part may take place
without the written permission of Cambridge University Press.
First published in print format 2003
ISBN-13 978-0-511-06872-0 eBook (EBL)
ISBN-10 0-511-06872-7 eBook (EBL)
ISBN-13 978-0-521-75374-6 hardback
ISBN-10 0-521-75374-0 hardback

Cambridge University Press has no responsibility for the persistence or accuracy of
s for external or third-party internet websites referred to in this book, and does not
guarantee that any content on such websites is, or will remain, accurate or appropriate.

To the memory of my parents

Contents

Preface
A Bit of Logic: A User’s Toolbox
I.1
First Order Languages
I.2
A Digression into the Metatheory:
Informal Induction and Recursion
I.3
Axioms and Rules of Inference
I.4
Basic Metatheorems
I.5
Semantics
I.6
Deﬁned Symbols
I.7
Formalizing Interpretations
I.8
The Incompleteness Theorems
I.9
Exercises
II The Set-Theoretic Universe, Naı̈vely
II.1
The “Real Sets”
II.2
A Naı̈ve Look at Russell’s Paradox
II.3
The Language of Axiomatic Set Theory
II.4
On Names
III The Axioms of Set Theory
III.1
Extensionality
III.2
Set Terms; Comprehension; Separation
III.3
The Set of All Urelements; the Empty Set
III.4
Class Terms and Classes
III.5
Axiom of Pairing
III.6
Axiom of Union
III.7
Axiom of Foundation
III.8
Axiom of Collection
III.9
Axiom of Power Set

I

vii

page xi
1
7
20
29
43
53
66
77
87
94
99
99
105
106
110
114
114
119
130
134
145
149
156
160
178

viii

Contents

III.10 Pairing Functions and Products
III.11 Relations and Functions
III.12 Exercises
IV
The Axiom of Choice
IV.1
Introduction
IV.2
More Justiﬁcation for AC; the “Constructible”
Universe Viewpoint
IV.3
Exercises
V
The Natural Numbers; Transitive Closure
V.1
The Natural Numbers
V.2
Algebra of Relations; Transitive Closure
V.3
Algebra of Functions
V.4
Equivalence Relations
V.5
Exercises
VI
Order
VI.1
PO Classes, LO Classes, and WO Classes
VI.2
Induction and Inductive Deﬁnitions
VI.3
Comparing Orders
VI.4
Ordinals
VI.5
The Transﬁnite Sequence of Ordinals
VI.6
The von Neumann Universe
VI.7
A Pairing Function on the Ordinals
VI.8
Absoluteness
VI.9
The Constructible Universe
VI.10 Arithmetic on the Ordinals
VI.11 Exercises
VII Cardinality
VII.1 Finite vs. Inﬁnite
VII.2 Enumerable Sets
VII.3 Diagonalization; Uncountable Sets
VII.4 Cardinals
VII.5 Arithmetic on Cardinals
VII.6 Coﬁnality; More Cardinal Arithmetic;
Inaccessible Cardinals
VII.7 Inductively Deﬁned Sets Revisited;
Relative Consistency of GCH
VII.8 Exercises
VIII Forcing
VIII.1 PO Sets, Filters, and Generic Sets
VIII.2 Constructing Generic Extensions

182
193
210
215
215
218
229
232
232
253
272
276
281
284
284
293
316
323
340
358
373
377
395
410
426
430
431
442
451
457
470
478
494
512
518
520
524

Contents
VIII.3 Weak Forcing
VIII.4 Strong Forcing
VIII.5 Strong vs. Weak Forcing
VIII.6 M[G] Is a CTM of ZFC If M Is
VIII.7 Applications
VIII.8 Exercises
Bibliography
List of Symbols
Index

ix
528
532
543
544
549
558
560
563
567

Preface

This volume contains the basics of Zermelo-Fraenkel axiomatic set theory. It is
situated between two opposite poles: On one hand there are elementary texts that
familiarize the reader with the vocabulary of set theory and build set-theoretic
tools for use in courses in analysis, topology, or algebra – but do not get into
metamathematical issues. On the other hand are those texts that explore issues
of current research interest, developing and applying tools (constructibility,
absoluteness, forcing, etc.) that are aimed to analyze the inability of the axioms
to settle certain set-theoretic questions.
Much of this volume just “does set theory”, thoroughly developing the theory
of ordinals and cardinals along with their arithmetic, incorporating a careful discussion of diagonalization and a thorough exposition of induction and inductive
(recursive) deﬁnitions. Thus it serves well those who simply want tools to apply to other branches of mathematics or mathematical sciences in general (e.g.,
theoretical computer science), but also want to ﬁnd out about some of the subtler
results of modern set theory.
Moreover, a fair amount is included towards preparing the advanced reader
to read the research literature. For example, we pay two visits to Gödel’s constructible universe, the second of which concludes with a proof of the relative
consistency of the axiom of choice and of the generalized continuum hypothesis
with ZF. As such a program requires, I also include a thorough discussion of
formal interpretations and absoluteness. The lectures conclude with a short but
detailed study of Cohen forcing and a proof of the non-provability in ZF of the
continuum hypothesis.
The level of exposition is designed to ﬁt a spectrum of mathematical sophistication, from third-year undergraduate to junior graduate level (each group will
ﬁnd here its favourite chapters or sections that serve its interests and level of
preparation).
xi

xii

Preface

The volume is self-contained. Whatever tools one needs from mathematical
logic have been included in Chapter I. Thus, a reader equipped with a combination of sufﬁcient mathematical maturity and patience should be able to
read it and understand it. There is a trade-off: the less the maturity at hand, the
more the supply of patience must be. To pinpoint this “maturity”: At least two
courses from among calculus, linear algebra, and discrete mathematics at the
junior level should have exposed the reader to sufﬁcient diversity of mathematical issues and proof culture to enable him or her to proceed with reasonable
ease.
A word on approach. I use the Zermelo-Fraenkel axiom system with the axiom
of choice (AC). This is the system known as ZFC. As many other authors do, I
simplify nomenclature by allowing “proper classes” in our discussions as part
of our metalanguage, but not in the formal language.
I said earlier that this volume contains the “basics”. I mean this characterisation in two ways: One, that all the fundamental tools of set theory as needed
elsewhere in the mathematical sciences are included in detailed exposition. Two,
that I do not present any applications of set theory to other parts of mathematics,
because space considerations, along with a decision to include certain advanced
relative consistency results, have prohibited this.
“Basics” also entails that I do not attempt to bring the reader up to speed
with respect to current research issues. However, a reader who has mastered
the advanced metamathematical tools contained here will be able to read the
literature on such issues.
The title of the book reﬂects two things: One, that all good short titles are
taken. Two, more importantly, it advertises my conscious effort to present the
material in a conversational, user-friendly lecture style. I deliberately employ
classroom mannerisms (such as “pauses” and parenthetical “why”s, “what if”s,
and attention-grabbing devices for passages that I feel are important). This
aims at creating a friendly atmosphere for the reader, especially one who has
decided to study the topic without the guidance of an instructor. Friendliness
also means steering clear of the terse axiom-deﬁnition-theorem recipe, and
explaining how some concepts were arrived at in their present form. In other
words, what makes things tick. Thus, I approach the development of the key
concepts of ordinals and cardinals, initially and tentatively, in the manner they
were originally introduced by Georg Cantor (paradox-laden and all). Not only
does this afford the reader an understanding of why the modern (von Neumann)
approach is superior (and contradiction-free), but it also shows what it tries to
accomplish. In the same vein, Russell’s paradox is visited no less than three

Preface

xiii

times, leaving us in the end with a ﬁrm understanding that it has nothing to do
with the “truth” or otherwise of the much-maligned statement “x ∈ x” but it is
just the result of a diagonalization of the type Cantor originally taught us.
A word on coverage. Chapter I is our “Chapter 0”. It contains the tools needed
to enable us do our job properly – a bit of mathematical logic, certainly no more
than necessary. Chapter II informally outlines what we are about to describe
axiomatically: the universe of all the “real” sets and other “objects” of our
intuition, a caricature of the von Neumann “universe”. It is explained that the
whole fuss about axiomatic set theory† is to have a formal theory derive true
statements about the von Neumann sets, thus enabling us to get to know the
nature and structure of this universe. If this is to succeed, the chosen axioms
must be seen to be “true” in the universe we are describing.
To this end I ensure via informal discussions that every axiom that is introduced is seen to “follow” from the principle of the formation of sets by stages, or
from some similarly plausible principle devised to keep paradoxes away. In this
manner the reader is constantly made aware that we are building a meaningful
set theory that has relevance to mathematical intuition and expectations (the
“real” mathematics), and is not just an artiﬁcial choice of a contradiction-free
set of axioms followed by the mechanical derivation of a few theorems.
With this in mind, I even make a case for the plausibility of the axiom of
choice, based on a popularization of Gödel’s constructible universe argument.
This occurs in Chapter IV and is informal.
The set theory we do allows atoms (or Urelemente),‡ just like Zermelo’s.
The re-emergence of atoms has been defended aptly by Jon Barwise (1975) and
others on technical merit, especially when one does “restricted set theories”
(e.g., theory of admissible sets).
Our own motivation is not technical; rather it is philosophical and pedagogical. We ﬁnd it extremely counterintuitive, especially when addressing
undergraduate audiences, to tell them that all their familiar mathematical
objects – the “stuff of mathematics” in Barwise’s words – are just perverse
“box-in-a-box-in-a-box . . . ” formations built from an inﬁnite supply of empty
boxes. For example, should I be telling my undergraduate students that their
”?
familiar number “2” really is just a short name for something like “
√
And what will I tell them about “ 2 ”?
†

‡

O.K., maybe not the whole fuss. Axiomatics also allow us to meaningfully ask, and attempt to
answer, metamathematical questions of derivability, consistency, relative consistency, independence. But in this volume much of the fuss is indeed about learning set theory.
Allows, but does not insist that there are any.

xiv

Preface

Some mathematicians have said that set theory (without atoms) speaks only
of sets and it chooses not to speak about objects such as cows or ﬁsh (colourful
terms for urelements). Well, it does too! Such (“atomless”) set theory is known
to be perfectly capable of constructing “artiﬁcial ” cows and ﬁsh, and can then
proceed to talk about such animals as much as it pleases.
While atomless ZFC has the ability to construct or codify all the familiar
mathematical objects in it, it does this so well that it betrays the prime directive
of the axiomatic method, which is to have a theory that applies to diverse
concrete (meta – i.e., outside the theory and in the realm of “everyday math”)
mathematical systems. Group theory and projective geometry, for example,
fulﬁll the directive.
In atomless ZFC the opposite appears to be happening: One is asked to
embed the known mathematics into the formal system.
We prefer a set theory that allows both artiﬁcial and real cows and ﬁsh, so that
when we want to illustrate a point in an example utilizing, say, the everyday set
of integers, Z, we can say things like “let the atoms (be interpreted to) include
the members of Z . . . ”.
But how about technical convenience? Is it not hard to include atoms in a
formal set theory? In fact, not at all!
A word on exposition devices. I freely use a pedagogical feature that, I believe,
originated in Bourbaki’s books – that is, marking an important or difﬁcult topic
by placing a “winding road” sign in the margin next to it. I am using here the
same symbol that Knuth employed in his TEXbook, namely, , marking with
it the beginning and end of an important passage.
Topics that are advanced, or of the “read at your own risk” type, can be
.
omitted without loss of continuity. They are delimited by a double sign,
Most chapters end with several exercises. I have stopped making attempts to
sort exercises between “hard” and “just about right”, as such classiﬁcations are
rather subjective. In the end, I’ll pass on to you the advice one of my professors
at the University of Toronto used to offer: “Attempt all the problems. Those you
can do, don’t do. Do the ones you cannot”.
What to read. Just as in the advice above, I suggest that you read everything
that you do not already know if time is no object. In a class environment the
coverage will depend on class length and level, and I defer to the preferences of
the instructor. I suppose that a fourth-year undergraduate audience ought to see
the informal construction of the constructible universe in Chapter IV, whereas
a graduate audience would rather want to see the formal version in Chapter VI.
The latter group will probably also want to be exposed to Cohen forcing.

Preface

xv

Acknowledgments. I wish to thank all those who taught me, a group that is too
large to enumerate, in which I must acknowledge the presence and inﬂuence
of my parents, my students, and the writings of Shoenﬁeld (in particular, 1967,
1978, 1971).
The staff at Cambridge University Press provided friendly and expert support, and I thank them. I am particularly grateful for the encouragement received
from Lauren Cowles and Caitlin Doggart at the initial (submission and refereeing) and advanced stages (production) of the publication cycle respectively.
I also wish to record my appreciation to Zach Dorsey of TechBooks and
his team. In both volumes they tamed my English and LATEX, ﬁtting them to
Cambridge speciﬁcations, and doing so with professionalism and ﬂexibility.
This has been a long project that would have not been successful without
the support and understanding – for my long leaves of absence in front of a
computer screen – that only one’s family knows how to provide.
I ﬁnally wish to thank Donald Knuth and Leslie Lamport for their typesetting
systems TEX and LATEX that make technical writing fun (and also empower
authors to load the pages with and other signs).
George Tourlakis
Toronto, March 2002

I
A Bit of Logic: A User’s Toolbox

This prerequisite chapter – what some authors call a “Chapter 0” – is an abridged
version of Chapter I of volume 1 of my Lectures in Logic and Set Theory. It is offered here just in case that volume Mathematical Logic is not readily accessible.
Simply put, logic† is about proofs or deductions. From the point of view of
the user of the subject – whose best interests we attempt to serve in this chapter –
logic ought to be just a toolbox which one can employ to prove theorems, for
example, in set theory, algebra, topology, theoretical computer science, etc.
The volume at hand is about an important specimen of a mathematical theory,
or logical theory, namely, axiomatic set theory. Another signiﬁcant example,
which we do not study here, is arithmetic. Roughly speaking, a mathematical
theory consists on one hand of assumptions that are speciﬁc to the subject
matter – the so-called axioms – and on the other hand a toolbox of logical rules.
One usually performs either of the following two activities with a mathematical
theory: One may choose to work within the theory, that is, employ the tools and
the axioms for the sole purpose of proving theorems. Or one can take the entire
theory as an object of study and study it “from the outside” as it were, in order to
pose and attempt to answer questions about the power of the theory (e.g., “does
the theory have as theorems all the ‘true’ statements about the subject matter?”),
its reliability (meaning whether it is free from contradictions or not), how its
reliability is affected if you add new assumptions (axioms), etc.
Our development of set theory will involve both types of investigations indicated above:
(1) Primarily, we will act as users of logic in order to deduce “true” statements about sets (i.e., theorems of set theory) as consequences of certain
†

We drop the qualiﬁer “mathematical” from now on, as this is the only type of logic we are about.

1

2

I. A Bit of Logic: A User’s Toolbox

“obviously true”† statements that we accept up front without proof, namely,
the ZFC axioms.‡ This is pretty much analogous to the behaviour of a
geometer whose job is to prove theorems of, say, Euclidean geometry.
(2) We will also look at ZFC from the outside and address some issues of the
type “is such and such a sentence (of set theory) provable from the axioms
of ZFC and the rules of logic alone?”
It is evident that we need a precise formulation of set theory, that is, we must
turn it into a mathematical object in order to make task (2), above, a meaningful
mathematical activity.§ This dictates that we develop logic itself formally, and
subsequently set theory as a formal theory.
Formalism,¶ roughly speaking, is the abstraction of the reasoning processes
(proofs) achieved by deleting any references to the “truth content” of the component mathematical statements (formulas). What is important in formalist
reasoning is solely the syntactic form of (mathematical) statements as well as
that of the proofs (or deductions) within which these statements appear.
A formalist builds an artiﬁcial language, that is, an inﬁnite – but ﬁnitely
speciﬁable# – collection of “words” (meaning symbol sequences, also called
expressions). He|| then uses this language in order to build deductions – that
is, ﬁnite sequences of words – in such a manner that, at each step, he writes
down a word if and only if it is “certiﬁed” to be syntactically correct to do so.
“Certiﬁcation” is granted by a toolbox consisting of the very same rules of logic
that we will present in this chapter.
The formalist may pretend, if he so chooses, that the words that appear in a
proof are meaningless sequences of meaningless symbols. Nevertheless, such
posturing cannot hide the fact that (in any purposefully designed theory) these

†

‡
§
¶
#
||

We often quote a word or cluster of related words as a warning that the crude English meaning
is not necessarily the intended meaning, or it may be ambiguous. For example, the ﬁrst “true”
in the sentence where this footnote originates is technical, but in a ﬁrst approximation may be
taken to mean what “true” means in English. “Obviously true” is an ambiguous term. Obvious to
whom? However, the point is – to introduce another ambiguity – that “reasonable people” will
accept the truth of the (ZFC) axioms.
This is an acronym reﬂecting the names of Zermelo and Fraenkel – the founders of this particular
axiomatization – and the fact that the so-called axiom of choice is included.
Here is an analogy: It is the precision of the rules for the game of chess that makes the notion of
analyzing a chessboard conﬁguration meaningful.
The person who practises formalism is a formalist.
The ﬁnite speciﬁcation is achieved by a ﬁnite collection of “rules”, repeated applications of which
build the words.
By deﬁnition, “he”, “his”, “him” – and their derivatives – are gender-neutral in this volume.

I. A Bit of Logic: A User’s Toolbox

3

words codify “true” (intuitively speaking) statements. Put bluntly, we must have
something meaningful to talk about before we bother to codify it.
Therefore, a formal theory is a laboratory version (artiﬁcial replica or simulation, if you will) of a “real” mathematical theory of the type encountered
in mathematics,† and formal proofs do unravel (codiﬁed versions of) “truths”
beyond those embodied in the adopted axioms.
It will be reassuring for the uninitiated that it is a fact of logic that the totality of the “universally true” statements – that is, those that hold in all of
mathematics and not only in speciﬁc theories – coincides with the totality
of statements that we can deduce purely formally from some simple universally true assumptions such as x = x, without any reference to meaning or
“truth” (Gödel’s completeness theorem for ﬁrst order logic). In short, in this
case formal deducibility is as powerful as “truth”. The ﬂip side is that formal
deducibility cannot be as powerful as “truth” when it is applied to speciﬁc
mathematical theories such as set theory or arithmetic (Gödel’s incompleteness
theorem).
Formalization allows us to understand the deeper reasons that have prevented set theorists from settling important questions such as the continuum
hypothesis – that is, the statement that there are no cardinalities between that of
the set of natural numbers and that of the set of the reals. This understanding is
gathered by “running diagnostics” on our laboratory replica of set theory. That
is, just as an engineer evaluates a new airplane design by building and testing
a model of the real thing, we can ﬁnd out, with some startling successes, what
are the limitations of our theory, that is, what our assumptions are incapable of
logically implying.‡ If the replica is well built,§ we can then learn something
about the behaviour of the real thing.
In the case of formal set theory and, for example, the question of our failure
to resolve the continuum hypothesis, such diagnostics (the methods of Gödel
and Cohen – see Chapters VI and VIII) return a simple answer: We have not
included enough assumptions in (whether “real” or “formal”) set theory to settle
this question one way or another.
†
‡

§

Examples of “real” (non-formalized) theories are Euclid’s geometry, topology, the theory of
groups, and, of course, Cantor’s “naı̈ve” or “informal” set theory.
In model theory “model” means exactly the opposite of what it means here. A model airplane
abstracts the real thing. A model of a formal (i.e., abstract) theory is a “concrete” or “real” version
of the abstract theory.
This is where it pays to choose reasonable assumptions, assumptions that are “obviously true”.

4

I. A Bit of Logic: A User’s Toolbox

But what about the interests of the reader who only wants to practise set
theory, and who therefore may choose to skip the parts of this volume that just
talk about set theory? Does, perchance, formalism put him into an unnecessary
straitjacket?
We think not. Actually it is easier, and safer, to reason formally than to do so
informally. The latter mode often mixes syntax and semantics (meaning), and
there is always the danger that the “user” may assign incorrect (i.e., convenient,
but not general) meanings to the symbols that he manipulates, a phenomenon
that anyone who is teaching mathematics must have observed several times
with some distress.
Another uncertainty one may encounter in an informal approach is this:
“What can we allow to be a ‘property’ in mathematics?” This is an important
question, for we often want to collect objects that share a common property,
or we want to prove some property of the natural numbers by induction or by
the least principle. But what is a property? Is colour a property? How about
mood? It is not enough to say, “no, these are not properties”, for these are
just two frivolous examples. The question is how to describe accurately and
unambiguously the inﬁnite variety of properties that are allowed. Formalism
can do just that.†
“Formalism for the user” is not a revolutionary slogan. It was advocated
by Hilbert, the founder of formalism, partly as a means of – as he believed‡ –
formulating mathematical theories in a manner that allows one to check them
(i.e., run diagnostic tests on them) for freedom from contradiction,§ but also as
the right way to do mathematics. By this proposal he hoped to salvage mathematics itself – which, Hilbert felt, was about to be destroyed by the Brouwer
school of intuitionist thought. In a way, his program could bridge the gap
between the classical and the intuitionist camps, and there is some evidence
that Heyting (an inﬂuential intuitionist and contemporary of Hilbert) thought
that such a rapprochement was possible. After all, since meaning is irrelevant
to a formalist, all that he is doing (in a proof ) is shufﬂing ﬁnite sequences of
†

‡
§

Well, almost. So-called cardinality considerations make it impossible to describe all “good”
properties formally. But, practically and empirically speaking, we can deﬁne all that matter for
“doing mathematics”.
This belief was unfounded, as Gödel’s incompleteness theorems showed.
Hilbert’s metatheory – that is, the “world” or “lab” outside the theory, where the replica is
actually manufactured – was ﬁnitary. Thus – Hilbert believed – all this theory building and
theory checking ought to be effected by ﬁnitary means. This was another ingredient that was
consistent with peaceful coexistence with the intuitionists. And, alas, this ingredient was the one
that – as some writers put it – destroyed Hilbert’s program to found mathematics on his version
of formalism. Gödel’s incompleteness theorems showed that a ﬁnitary metatheory is not up to

I. A Bit of Logic: A User’s Toolbox

5

symbols, never having to handle or argue about inﬁnite objects – a good thing,
as far as an intuitionist is concerned.†
In support of the “formalism for the user” position we must not fail to
mention Bourbaki’s (1966a) monumental work, which is a formalization of a
huge chunk of mathematics, including set theory, algebra, topology, and theory
of integration. This work is strictly for the user of mathematics, not for the
metamathematician who studies formal theories. Yet, it is fully formalized,
true to the spirit of Hilbert, and it comes in a self-contained package, including
a “Chapter 0” on formal logic.
More recently, the proposition of employing formal reasoning as a tool has
been gaining support in a number of computer science undergraduate curricula,
where logic and discrete mathematics are taught in a formalized setting, starting
with a rigorous course in the two logical calculi (propositional and predicate),
emphasizing the point of view of the user of logic (and mathematics) – hence
with an attendant emphasis on calculating (i.e., writing and annotating formal)
proofs. Pioneering works in this domain are the undergraduate text (1994) and
the paper (1995) of Gries and Schneider.
You are urged to master the technique of writing formal proofs by studying
how we go about it throughout this volume, especially in Chapter III.‡ You will
ﬁnd that writing and annotating formal proofs is a discipline very much like
computer programming, so it cannot be that hard. Computer programming is
taught in the ﬁrst year, isn’t it?§
†

‡
§

True, a formalist applies classical logic, while an intuitionist applies a different logic where, for
example, double negation is not removable. Yet, unlike a Platonist, a formalist does not believe –
or he does not have to disclose to his intuitionist friends that he might do – that inﬁnite sets exist
in the metatheory, as his tools are just ﬁnite symbol sequences. To appreciate the tension here,
consider this anecdote: It is said that when Kronecker – the father of intuitionism – was informed
of Lindemann’s proof (1882) that π is transcendental, while he granted that this was an interesting
result, he also dismissed it, suggesting that π – whose decimal expansion is, of course, inﬁnite
but not periodic – “does not exist” (see Wilder (1963, p. 193)). We do not propound the tenets of
intuitionism here, but it is fair to state that inﬁnite sets are possible in intuitionistic mathematics
as this has later evolved in the hands of Brouwer and his Amsterdam school. However, such
sets must be (like all sets of intuitionistic mathematics) ﬁnitely generated – just like our formal
languages and the set of theorems (the latter provided that our axioms are too) – in a sense that
may be familiar to some readers who have had a course in automata and language theory. See
Wilder (1963, p. 234).
Many additional paradigms of formal proofs, in the context of arithmetic, are found in Chapter II
of volume 1 of these Lectures.
One must not gather the impression that formal proofs are just obscure sequences of symbol
sequences akin to Morse code. Just as one does in computer programming, one also uses comments
in formal proofs – that is, annotations (in English, Greek, or your favourite natural language)
that aim to explain or justify for the beneﬁt of the reader the various proof steps. At some point,
when familiarity allows and the length of (formal) proofs becomes prohibitive, we agree to relax
the proof style. Read on!

6

I. A Bit of Logic: A User’s Toolbox

It is also fair to admit, in defense of “semantic reasoning”, that meaning is
an important tool for formulating conjectures, for analyzing a given proof in
order to ﬁgure out what makes it tick, or indeed for discovering the proof, in
rough outline, in the ﬁrst place. For these very reasons we supplement many of
our formal arguments in this volume with discussions that are based on intuitive
semantics, and with several examples taken from informal mathematics.
We forewarn the reader of the inevitability with which the informal language
of sets already intrudes in this chapter (as it indeed does in all mathematics).
More importantly, some of the elementary results of Cantorian naı̈ve set theory
are needed here. Conversely, formal set theory needs the tools and some of the
results developed here. This apparent “chicken or egg” phenomenon is often
called “bootstrapping”,† not to be confused with “circularity” – which it is not:
Only informal set theory notation and results are needed here in order to found
formal set theory.
This is a good place to summarize our grand plan:
First (in this chapter), we will formalize the rules of reasoning in general – as
these apply to all mathematics – and develop their properties. We will skip the
detailed study of the interaction between formalized rules and their intended
meaning (semantics), as well as the study of the limitations of these formalized
rules. Nevertheless, we will state without proof the relevant important results
that come into play here, the completeness and incompleteness theorems (both
due to Kurt Gödel).
Secondly (starting with the next chapter), once we have learnt about these
tools of formalized reasoning – what they are and how to use them – we will
next become users of formal logic so that we can discover important theorems
of (or, as we say, develop) set theory. Of course, we will not forget to run a few
diagnostics. For example, Chapter VIII is entirely on metamathematical issues.
Formal theories, and their artiﬁcial languages, are deﬁned (built) and “tested”
within informal mathematics (the latter also called “real” mathematics by
Platonists). The ﬁrst theory that we build here is general-purpose, or “pure”,
formal logic. We can then build mathematical formal theories (e.g., set theory)
by just adding “impurities”, namely, the appropriate special symbols and appropriate special assumptions (written in the artiﬁcial formal language).
We describe precisely how we construct these languages and theories using
the usual abundance of mathematical notation, notions, and techniques available
†

The term “bootstrapping” is suggestive of a person pulling himself up by his bootstraps. Reputedly, this technique, which is pervasive, among others, in the computer programming ﬁeld – as
alluded to in the term “booting” – was invented by Baron Münchhausen.

I.1. First Order Languages

7

to us, augmented by the descriptive power of natural language (e.g., English,
or Greek, or French, or German, or Russian), as particular circumstances or
geography might dictate. This milieu within which we build, pursue, and study
our theories – besides “real mathematics” – is also often called the metatheory,
or more generally, metamathematics. The language we speak while at it, this
mélange of mathematics and natural language, is the metalanguage.
I.1. First Order Languages
In the most abstract and thus simplest manner of describing it, a formalized
mathematical theory (also, formalized logical theory) consists of the following
sets of things: a set of basic or primitive symbols, V , used to build symbol
sequences (also called strings, or expressions, or words, over V ); a set of
strings, Wff, over V , called the formulas of the theory; and ﬁnally, a subset of
Wff, Thm, the set of theorems of the theory.†
Well, this is the extension of a theory, that is, the explicit set of objects in it.
How is a theory given?
In most cases of interest to the mathematician it is given by specifying V and
two sets of simple rules, namely, formula-building rules and theorem-building
rules. Rules from the ﬁrst set allow us to build, or generate, Wff from V .
The rules of the second set generate Thm from Wff. In short (e.g., Bourbaki
(1966b)), a theory consists of an alphabet of primitive symbols and rules used
to generate the “language of the theory” (meaning, essentially, Wff) from these
symbols, and some additional rules used to generate the theorems. We expand
on this below.
I.1.1 Remark. What is a rule? We run the danger of becoming circular or too
pedantic if we overdeﬁne this notion. Intuitively, the rules we have in mind
are string manipulation rules – that is, “black boxes” (or functions) that receive string inputs and respond with string outputs. For example, a well-known
theorem-building rule receives as input a formula and a variable, and it returns
(essentially) the string composed of the symbol ∀, immediately followed by the

variable and, in turn, immediately followed by the formula.‡
(1) First off, the ( ﬁrst order) formal language, L, where the theory is “spoken”§
is a triple (V , Term, Wff), that is, it has three important components, each
of them a set. V is the alphabet (or vocabulary) of the language. It is the
†
‡
§

For a less abstract, but more detailed view of theories see p. 39.
This rule is usually called “generalization”.
We will soon say what makes a language “ﬁrst order”.

8

I. A Bit of Logic: A User’s Toolbox

collection of the basic syntactic “bricks” (symbols) that we use to form
symbol sequences (or expressions) that are terms (members of Term) or
formulas (members of Wff). We will ensure that the processes that build
terms or formulas, using the basic building blocks in V , are (intuitively)
algorithmic (“mechanical”). Terms will formally codify objects, while formulas will formally codify statements about objects.
(2) Reasoning in the theory will be the process of discovering “true statements”
about objects – that is, theorems. This discovery journey begins with certain formulas which codify statements that we take for granted (i.e., accept
without proof as “basic truths”). Such formulas are the axioms. There are
two types of axioms. Special, or nonlogical, axioms are to describe speciﬁc
aspects of any theory that we might be building; they are “basic truths”
in a restricted context. For example, “x + 1 = 0” is a special axiom that
contributes towards the characterization of number theory over N. This is a
“basic truth” in the context of N but is certainly not true of the integers or the
rationals – which is good, because we do not want to confuse N with the integers or the rationals. The other kind of axiom will be found in all theories.
It is the kind that is “universally valid”, that is, not a theory-speciﬁc truth
but one that holds in all branches of mathematics (for example, “x = x” is
such a universal truth). This is why this type of axiom will be called logical.
(3) Finally, we will need rules for reasoning, actually called rules of inference.
These are rules that allow us to deduce, or derive, a true statement from other
statements that we have already established as being true.† These rules will
be chosen to be oblivious to meaning, being only conscious of form. They
will apply to statement conﬁgurations of certain recognizable forms and
will produce (derive) new statements of some corresponding recognizable
forms (see Remark I.1.1).
I.1.2 Remark. We may think of axioms (of either logical or nonlogical type) as
being special cases of rules, that is, rules that receive no input in order to produce
an output. In this manner item (2) above is subsumed by item (3), thus we are
faithful to our abstract deﬁnition of theory (where axioms were not mentioned).
An example, outside mathematics, of an inputless rule is the rule invoked
when you type date on your computer keyboard. This rule receives no input,

and outputs the current date on your screen.
We next look carefully into (ﬁrst order) formal languages.
†

The generous use of the term “true” here is only meant to motivate. “Provable” or “deducible”
formula, or “theorem”, will be the technically precise terminology that we will soon deﬁne to
replace the term “true statement”.

I.1. First Order Languages

9

There are two parts in each ﬁrst order alphabet. The ﬁrst, the collection of
the logical symbols, is common to all ﬁrst order languages (regardless of which
theory is spoken in them). We describe this part immediately below.
Logical Symbols.
LS.1. Object or individual variables. An object variable is any one symbol out
of the unending sequence v0 , v1 , v2 , . . . . In practice – whether we are
using logic as a tool or as an object of study – we agree to be sloppy with
notation and use, generically, x, y, z, u, v, w with or without subscripts
or primes as names of object variables.† This is just a matter of notational convenience. We allow ourselves to write, say, z instead of, say,
v120000000000560000009 . Object variables (intuitively) “vary over” (i.e., are
allowed to take values that are) the objects that the theory studies (e.g.,
numbers, sets, atoms, lines, points, etc., as the case may be).
LS.2. The Boolean or propositional connectives. These are the symbols “¬”
and “∨”.‡ These are pronounced not and or respectively.
LS.3. The existential quantiﬁer, that is, the symbol “∃”, pronounced exists or
for some.
LS.4. Brackets, that is, “(” and “)”.
LS.5. The equality predicate. This is the symbol “=”, which we use to indicate
that objects are “equal”. It is pronounced equals.
The logical symbols will have a ﬁxed interpretation. In particular, “=” will
always be expected to mean equals.
The theory-speciﬁc part of the alphabet is not ﬁxed, but varies from theory
to theory. For example, in set theory we just add the nonlogical (or special)
symbols, ∈ and U . The ﬁrst is a special predicate symbol (or just predicate) of
arity 2; the second is a predicate symbol of arity 1.§
In number theory we adopt instead the special symbols S (intended meaning:
successor, or “ + 1”, function), +, ×, 0, <, and (sometimes) a symbol for the
†

‡
§

Conventions such as this one are essentially agreements – effected in the metatheory – on how to
be sloppy and get away with it. They are offered in the interest of user-friendliness and readability.
There are also theory-speciﬁc conventions, which may allow additional names in our informal
(metamathematical) notation. Such examples, in set theory, occur in the following chapters.
The quotes are not part of the symbol. They serve to indicate clearly, e.g., in the case of “∨” here,
what is part of the symbol and what is not (the following period is not).
“arity” is derived from “ary” of “unary”, “binary”, etc. It denotes the number of arguments
needed by a symbol according to the dictates of correct syntax. Function and predicate symbols
need arguments.

10

I. A Bit of Logic: A User’s Toolbox

exponentiation operation (function) a b . The ﬁrst three are function symbols of
arities 1, 2, and 2 respectively. 0 is a constant symbol, < is a predicate of arity 2,
and whatever symbol we might introduce to denote a b would have arity 2.
The following list gives the general picture.
Nonlogical Symbols.
NLS.1. A (possibly empty) set of symbols for constants. We normally use
the metasymbols† a, b, c, d, e, with or without primes or subscripts, to
stand for constants unless we have in mind some alternative “standard”
formal notation in speciﬁc theories (e.g., ∅, 0, ω).
NLS.2. A (possibly empty) set of symbols for predicate symbols or relation
symbols for each possible arity n > 0. We normally use P, Q, R,
generically, with or without primes or subscripts, to stand for predicate
symbols. Note that = is in the logical camp. Also note that theoryspeciﬁc formal symbols are possible for predicates, e.g., <, ∈, U .
NLS.3. Finally, a (possibly empty) set of symbols for functions for each possible arity n > 0. We normally use f, g, h, generically, with or without
primes or subscripts, to stand for function symbols. Note that theoryspeciﬁc formal symbols are possible for functions, e.g., +, ×.
I.1.3 Remark. (1) We have the option of assuming that each of the logical
symbols that we named in LS.1–LS.5 have no further structure and that the
symbols are, ontologically, identical to their names, that is, they are just these
exact signs drawn on paper (or on any equivalent display medium).
In this case, changing the symbols, say, ¬ and ∃ to ∼ and E respectively
results in a “different” logic, but one that is, trivially, isomorphic to the one we
are describing: Anything that we may do in, or say about, one logic trivially
translates to an equivalent activity in, or utterance about, the other as long as
we systematically carry out the translations of all occurrences of ¬ and ∃ to ∼
and E respectively (or vice versa).
An alternative point of view is that the symbol names are not the same as
(identical with) the symbols they are naming. Thus, for example, “¬” names
the connective we pronounce not, by we do not know (or care) exactly what
the nature of this connective is (we only care about how it behaves). Thus, the
name “¬” becomes just a typographical expedient and may be replaced by other
names that name the same object, not.
This point of view gives one ﬂexibility in, for example, deciding how the
variable symbols are “implemented”. It often is convenient to suppose that the
†

Metasymbols are informal (i.e., outside the formal language) symbols that we use within “real”
mathematics – the metatheory – in order to describe, as we are doing here, the formal language.

I.1. First Order Languages

11

entire sequence of variable symbols was built from just two symbols, say, “v”
and “|”.† One way to do this is by saying that vi is a name for the symbol
sequence
v|...|.
  
i |’s

Or, preferably – see (2) below – vi might be a name for the symbol sequence
v | . . . | v.
  
i |’s

Regardless of option, vi and v j will name distinct objects if i = j.
This is not the case for the metavariables (abbreviated informal names)
x, y, z, u, v, w. Unless we say explicitly otherwise, x and y may name the
same formal variable, say, v131 .
We will mostly abuse language and deliberately confuse names with the
symbols they name. For example, we will say “let v1007 be an object variable . . . ”
rather than “let v1007 name an object variable . . . ”, thus appearing to favour
option one.
(2) Any two symbols included in the alphabet are distinct. Moreover, if any
of them are built from simpler sub-symbols – e.g., v0 , v1 , v2 , . . . might really
name the strings vv, v|v, v||v, . . . – then none of them is a substring (or subexpression) of any other.‡
(3) A formal language, just like a natural language (such as English or Greek),
is alive and evolving. The particular type of evolution we have in mind is the
one effected by formal deﬁnitions. Such deﬁnitions continually add nonlogical
symbols to the language.§
Thus, when we say that, e.g., “∈ and U are the only nonlogical symbols of
set theory”, we are telling a small white lie. More accurately, we ought to have
said that “∈ and U are the only ‘primitive’ (or primeval) nonlogical symbols of
set theory”, for we will add loads of other symbols such as ∪, ω, ∅, ⊂, and ⊆.
This evolution affects the (formal) language of any theory, not just that of

set theory.
†

‡
§

We intend these two symbols to be identical to their names. No philosophical or other purpose
will be served by allowing more indirection here (such as “v names u, which actually names w,
which actually is . . . ”).
What we have stated under (2) are requirements, not metatheorems. That is, they are nothing of
the sort that we can prove about our formal language within everyday mathematics.
This phenomenon will be visited upon in some detail in what follows. By the way, any additions
are made to the nonlogical side of the alphabet, since all the logical symbols have been given,
once and for all.

12

I. A Bit of Logic: A User’s Toolbox

Wait a minute! If formal set theory is to serve as the foundation of all mathematics, and if the present chapter is to assist towards that purpose, then how is
it that we are already employing natural numbers like 12000000560000009 as
subscripts in the names of object variables? How is it permissible to already talk
about “sets of symbols” when we are about to found a theory of sets formally?
Surely we do not have† any of these items yet, do we?
This protestation is offered partly in jest. We have already said that we work
within real mathematics as we build the “replicas” or “simulators” of logic
and set theory. Say we are Platonists. Then the entire body of mathematics –
including inﬁnite sets, in particular the set of natural numbers N – is available
to us as we are building whatever we are building.
We can thus describe how we assemble the simulator and its various parts
using our knowledge of real mathematics, the language of real mathematics,
and all “building blocks” available to us, including sets, inﬁnite or otherwise,
and natural numbers. This mathematics “exists” whether or not anyone ever
builds a formal simulator for naı̈ve set theory, or logic for that matter. Thus any
apparent circularity disappears.
Now if we are not Platonists, then our mathematical “reality” is more restricted, but, nevertheless, building a simulator or not in this reality does not
affect the existence of the reality. We will, however, this time, revise our tools.
For example, if we prefer to think that individual natural numbers exist (up
to any size), but not so their collection N, then it is still possible to build our
formal languages (in particular, as many object variables as we want) – pretty
much as already described – in this restricted metatheory. We may have to
be careful not to say that we have a unending sequence of such variables, as
this would presume the existence of inﬁnite sets in the metatheory.‡ We can
say instead that a variable is any object of the form vi where i is a (meaningless) word of (meaningless) symbols, the latter chosen out of the set or list
“0, 1, 2, 3, 4, 5, 6, 7, 8, 9”.
Clearly the above approach works even within a metatheory that has failed
to acknowledge the existence of any natural numbers.§
In this volume we will take the normal user-friendly position that is habitual nowadays, namely, that our metatheory is the Platonist’s (inﬁnitary)
mathematics.
†
‡
§

“Do not have” in the sense of having not formally deﬁned – or proved to exist – or both.
A ﬁnitist would have none of it, although a post-Brouwer intuitionist would be content that such
a sequence is ﬁnitely describable.
Hilbert, in his ﬁnitistic metatheory, built whatever natural numbers he needed by repeating the
stroke symbol “|”.

I.1. First Order Languages

13

I.1.4 Deﬁnition (Terminology about Strings). A symbol sequence, or expression (or string), that is formed by using symbols exclusively out of a given set†
M is called a string over the set, or alphabet, M.
If A and B denote strings (say, over M), then the symbol A ∗ B, or more
simply AB, denotes the symbol sequence obtained by listing ﬁrst the symbols
of A in the given left to right sequence, immediately followed by the symbols of
B in the given left to right sequence. We say that AB is (more properly, denotes
or names) the concatenation of the strings A and B in that order.
We denote the fact that the strings (named) C and D are identical sequences
(but we just say that they are equal) by writing C ≡ D. The symbol ≡ denotes
the negation of the string equality symbol ≡. Thus, if # and ? are (we do mean
“are”) symbols from an alphabet, then #?? ≡ #?? but #? ≡ #??. We can also
employ ≡ in contexts such as “let A ≡ ##?”, where we give the name A to the
string ##?.‡
In this book the symbol ≡ will be used exclusively in the metatheory as equality
of strings over some set M.
The symbol λ normally denotes the empty string, and we postulate for it the
following behaviour:
A ≡ Aλ ≡ λA

for all strings A.

We say that A occurs in B, or is a substring of B, iff § there are strings C and
D such that B ≡ C AD. For example, “(” occurs four times in the (explicit)
string “¬(()∨)((”, at positions 2, 3, 7, 8. Each time this happens we have an
occurrence of “(” in “¬(()∨)((”.
If C ≡ λ, we say that A is a preﬁx of B. If moreover D ≡ λ, then we say

that A is a proper preﬁx of B.
I.1.5 Deﬁnition (Terms). The set of terms, Term, is the smallest set of strings
over the alphabet V with the following two properties:
(1) Any of the items in LS.1 or NLS.1 (x, y, z, a, b, c, etc.) are included.
†
‡

§

A set that supplies symbols to be used in building strings is not special. It is just a set. However,
it often has a special name: “alphabet”.
Punctuation, such as “.”, is not part of the string. One often avoids such footnotes by quoting
strings that are explicitly written as symbol sequences. For example, if A stands for the string
#, one writes A ≡ “#”. Note that we must not write “A”, unless we mean a string whose only
symbol is A.
If and only if.

14

I. A Bit of Logic: A User’s Toolbox

(2) If f is a function† of arity n and t1 , t2 , . . . , tn are included, then so is the
string “ f t1 t2 . . . tn ”.
The symbols t, s, and u, with or without subscripts or primes, will denote
arbitrary terms. As they are used to describe the syntax of terms, we often call
such symbols syntactic variables – which is synonymous with metavariables.


I.1.6 Remark. (1) We often abuse notation and write f (t1 , . . . , tn ) instead of
f t1 . . . tn .
(2) Deﬁnition I.1.5 is an inductive deﬁnition.‡ It deﬁnes a more or less complicated term by assuming that we already know what simpler terms look like.
This is a standard technique employed in real mathematics (within which we are
deﬁning the formal language). We will have the opportunity to say more about
comment
such inductive deﬁnitions – and their appropriateness – in a
later on.
(3) We relate this particular manner of deﬁning terms to our working definition of a theory (given on p. 7 immediately before Remark I.1.1 in terms
of “rules” of formation). Item (2) in I.1.5 essentially says that we build new
terms (from old ones) by applying the following general rule: Pick an arbitrary
function symbol, say f . This has a speciﬁc formation rule associated with it.
Namely, “for the appropriate number, n, of an already existing ordered list of
terms, t1 , . . . , tn , build the new term consisting of f , immediately followed by
the ordered list of the given terms”.
For example, suppose we are working in the language of number theory.
There is a function symbol + available there. The rule associated with + builds
the new term +ts for any prior obtained terms t and s. Thus, +v1 v13 and
+v121 + v1 v13 are well-formed terms. We normally write terms of number theory in inﬁx notation,§ i.e., t +s, v1 +v13 and v121 +(v1 +v13 ) (note the intrusion of
brackets, to indicate sequencing in the application of +).
A by-product of what we have just described is that the arity of a function
symbol f is whatever number of terms the associated rule will require as
input.
†
‡

§

We will omit from now on the qualiﬁcation “symbol” from terminology such as “function symbol”, “constant symbol”, “predicate symbol”.
Some mathematicians are adamant that we call this a recursive deﬁnition and reserve the term
“induction” for “induction proofs”. This is seen to be unwarranted hairsplitting if we consider
that Bourbaki (1966b) calls induction proofs “démonstrations par récurrence”. We will be less
dogmatic: Either name is all right.
Function symbol placed between the arguments.

I.1. First Order Languages

15

(4) A crucial word used in I.1.5 (which recurs in all inductive deﬁnitions) is
“smallest”. It means “least inclusive” (set). For example, we may easily think of
a set of strings that satisﬁes both conditions of the above deﬁnition, but which
is not “smallest” by virtue of having additional elements, such as the string
“¬¬(”.
Pause. Why is “¬¬(” not in the smallest set as deﬁned above, and therefore
not a term?
The reader may wish to ponder further on the import of the qualiﬁcation
“smallest” by considering the familiar (similar) example of N. The principle of
induction in N ensures that this set is the smallest with the properties
(i) 0 is included, and
(ii) if n is included, then so is n + 1.
By contrast, all of Z (set of integers), Q (set of rational numbers), and R (set
of real numbers) satisfy (i) and (ii), but they are clearly not the “smallest” such.


I.1.7 Deﬁnition (Atomic Formulas). The set of atomic formulas, Af, contains
precisely:
(1) The strings t = s for every possible choice of terms t, s.
(2) The strings Pt1 t2 . . . tn for every possible choices of n-ary predicates P (for
all choices of n > 0) and all possible choices of terms t1 , t2 , . . . , tn .

We often abuse notation and write P(t1 , . . . , tn ) instead of Pt1 . . . tn .
I.1.8 Deﬁnition (Well-Formed Formulas). The set of well-formed formulas,
Wff, is the smallest set of strings or expressions over the alphabet V with the
following properties:
(a) All the members of Af are included.
(b) If A and B denote strings (over V ) that are included, then (A ∨ B ) and
(¬A) are also included.
(c) If A is† a string that is included and x is any object variable (which may or
may not occur (as a substring) in the string A), then the string ((∃x)A)

is also included. We say that A is the scope of (∃x).
†

Denotes.

16

I. A Bit of Logic: A User’s Toolbox

I.1.9 Remark.
(1) The above is yet another inductive deﬁnition. Its statement (in the metalanguage) is facilitated by the use of syntactic, or meta-, variables – A and
B – used as names for arbitrary (indeterminate) formulas. We ﬁrst encountered
the use of syntactic variables in Deﬁnition I.1.5.
In general, we will let calligraphic capital letters A, B , C , D, E, F , G
(with or without primes or subscripts) be syntactic variables (i.e., metalinguistic
names) denoting well-formed formulas, or just formulas, as we often say. The
deﬁnition of Wff given above is standard. In particular, it permits well-formed
formulas such as ((∃x)((∃x)x = 0)) in the interest of making the formation
rules context-free.†
(2) The rules of syntax just given do not allow us to write things such as ∃ f
or ∃P where f and P are function and predicate symbols respectively. That
quantiﬁcation is deliberately restricted to act solely on object variables makes
the language ﬁrst order.
(3) We have already indicated in Remark I.1.6 where the arities of function
and predicate symbols come from (Deﬁnitions I.1.5 and I.1.7 referred to them).
These are numbers that are implicit (“hardwired”) within the formation rules
for terms and atomic formulas. Each function, and each predicate symbol – e.g.,
+, ×, ∈, < – has its own unique associated formation rule. This rule “knows”
how many terms are needed (on the “input side”) in order to form a term or
atomic formula.
There is an alternative way of making arities of symbols known (in the
metatheory): Rather than embedding arities in the formation rules, we can hide
them inside the ontology of the symbols, not making them explicit in the name.
For example, a new symbol, say ∗, can be used to record arity. That is, we can
think of a predicate (or function) symbol as consisting of two parts: an arity
part and an “all the rest” part, the latter needed to render the symbol unique.
For example, ∈ may be actually the short name for the symbol “∈∗∗ ”, where
this latter name is identical to the symbol it denotes, or “what you see is what
you get” – see Remark I.1.3(1) and (2), p. 10. The presence of the two asterisks
declares the arity. Some people say this differently: They make available to the
metatheory a “function”, ar , from “the set of all predicate and function symbols”
(of a given language) to the natural numbers, so that for any function symbol f
or predicate symbol P, ar ( f ) and ar (P) yield the arity of f or P respectively.‡
†
‡

In some presentations, formation rule I.1.8(c) is context-sensitive: It requires that x be not already
quantiﬁed in A.
In mathematics we understand a function as a set of input-output pairs. One can “glue” the two
parts of such pairs together, as in “∈∗∗ ” – where “∈” is the input part and “∗∗” is the output part,
the latter denoting “2” – etc. Thus, the two approaches are equivalent.

I.1. First Order Languages

17

(4) As a consequence of the remarks in (3) the theory can go about its job of
generating, say, terms using the formation rules, at the same time being unable
to see or discuss these arities, since these are hidden inside the rules (or inside
the function or predicate names in the alternative approach). So it is not in the
theory’s “competence” to say, e.g., “hmm, this function has arity 10011132”.
Indeed, a theory cannot even say “hmm, so this is a function (or a term, or a
wff )”. A theory just generates strings. It does not test them for membership in
syntactic categories, such as variable, function, term, or wff. A human user of
the theory, on the other hand, can, of course, make such observations. Indeed,
in theories such as set theory and arithmetic, the human user can even write a
computer program that correctly makes such observations. But both of these
agents, human and computer, act in the metatheory.
(5) Abbreviations:
Abr1. The string ((∀x)A) abbreviates the string (¬((∃x)(¬A))). Thus, for
any explicitly written formula A, the former notation is informal (metamathematical), while the latter is formal (within the formal language). In
particular, ∀ is a metalinguistic symbol. “∀x” is the universal quantiﬁer.
A is its scope. The symbol ∀ is pronounced for all.
We also introduce – in the metalanguage – a number of additional Boolean
connectives in order to abbreviate certain strings:
Abr2. Conjunction, ∧. (A ∧ B ) stands for (¬((¬A) ∨ (¬B ))). The symbol
∧ is pronounced and.
Abr3. Classical or material implication, →. (A → B ) stands for ((¬A) ∨
B ). (A → B ) is pronounced if A, then B .
Abr4. Equivalence, ↔. (A ↔ B ) stands for ((A → B ) ∧ (B → A)).
Abr5. To minimize the use of brackets in the metanotation, we adopt standard
priorities of connectives, that is, ∀, ∃, and ¬ have the highest; then
we have (in decreasing order of priority) ∧, ∨, →, ↔; and we agree
not to use outermost brackets. All associativities are right – that is,
if we write A → B → C , then this is a (sloppy) counterpart for
(A → (B → C )).
(6) The language just deﬁned, L, is one-sorted, that is, it has a single sort or
type of object variable. Is this not inconvenient? After all, our set theory will
have both atoms and sets. In other theories, e.g., geometry, one has points, lines,
and planes. One would have hoped to have different types of variables, one for
each.
Actually, to do this would amount to a totally unnecessary complication of
syntax. We can (and will) get away with just one sort of object variable. For

18

I. A Bit of Logic: A User’s Toolbox

example, in set theory we will also introduce a 1-ary† predicate, U , whose job is
to test an object for “sethood”‡ (vs. atom status). Similar remedies are available
to other theories. For example, geometry will manage with one sort of variable,
and unary predicates “Point”, “Line”, and “Plane”.
Apropos language, some authors emphasize the importance of the nonlogical
symbols, taking at the same time the formation rules for granted; thus they say
that we have a language, say, “L = {∈, U }” rather than “L = (V , Term, Wff )
where V has ∈ and U as its only nonlogical symbols”. That is, they use

“language” for the nonlogical part of the alphabet.
This comment requires some familiarity with elementary concepts – such
as BNF notation for grammar speciﬁcation – encountered in a course on
formal languages and automata, or, alternatively in language manuals for Algollike programming languages (such as Algol itself, Pascal, etc.); hence the
sign.
We have said above “This rule ‘knows’ how many terms are needed (on
the ‘input side’) in order to form a term or atomic formula.” We often like to
personify rules, theories, and the like, to make the exposition more relaxed.
This runs the danger of being misunderstood on occasion. Here is how a rule
“knows”.
Syntactic deﬁnitions in the part of theoretical computer science known as
formal language theory are given by a neat notation called BNF:§ To ﬁx ideas,
let us say that we are describing the terms of a speciﬁc ﬁrst order language that
contains just one constant symbol, “c”, and just two function symbols, “ f ” and
“g”, where we intend the former to be ternary (arity 3) and the latter of arity 5.
Moreover, assume that the variables v0 , v1 , . . . are short names for vv, v|v, . . .
respectively.
Then, using the syntactic names ter m, var , str okes to stand for any
term, any variable, any string of strokes, we can recursively deﬁne these syntactic categories as follows, where
 we read “→” as “is deﬁned as” (the right

hand side), and the big stroke, “” – pronounced “or” – gives alternatives in the
†
‡
§

More usually called unary.
People writing about, or teaching, set theory have made this word up. Of course, one means by
it the property of being a set.


Backus-Naur form. Rules (1)–(3) are in BNF. In particular the alternative symbol “” is part of
BNF notation, and so is the . . .  notation for the names of syntactic categories. The “→” has
many typographical variants, including “::=”.

I.1. First Order Languages

19

deﬁnition (of the left hand side):


(1) strokes → λstrokes|
(2) var → vstrokesv




(3) term → cvar


f termtermtermgtermtermtermtermterm
For example, rule (1) says that a string of strokes is (deﬁned as) either the empty
string λ, or a string of strokes followed by a single stroke.
Rule (3) shows clearly how the “knowledge” of the arities of f and g is
“hardwired” within the rule. For example, the third alternative of that rule says
that a term is a string composed of the symbol “ f ” followed immediately by
three strings, each of which is a term.
A variable that is quantiﬁed is bound in the scope of the quantiﬁer. Nonquantiﬁed variables are free. We also give below, by induction on formulas,
precise (metamathematical) deﬁnitions of “free” and “bound”.
I.1.10 Deﬁnition (Free and Bound Variables). An object variable x occurs
free in a term t or atomic formula A iff it occurs in t or A as a substring
(see I.1.4).
x occurs free in (¬A) iff it occurs free in A.
x occurs free in (A ∨ B ) iff it occurs free in at least one of A and B .
x occurs free in ((∃y)A) iff x occurs free in A and y is not the same variable
as x.†
The y in ((∃y)A) is, of course, not free – even if it might be so in A – as
we have just concluded in this inductive deﬁnition. We say that it is bound in

((∃y)A). Trivially, terms and atomic formulas have no bound variables.
I.1.11 Remark. (1) Of course, Deﬁnition I.1.10 takes care of the deﬁned connectives as well, via the obvious translation procedure.
(2) Notation. If A is a formula, then we often write A [y1 , . . . , yk ] to
indicate interest in the variables y1 , . . . , yk , which may or may not be free in
†

Recall that x and y are abbreviations of names such as v1200098 and v11009 (which name distinct
variables). However, it could be that both x and y name v101 . Therefore it is not redundant to say
“and y is not the same variable as x”. By the way, x ≡ y says the same thing, by I.1.4.

20

I. A Bit of Logic: A User’s Toolbox

A. There may be other free variables in A that we may have chosen not to include in the list. On the other hand, if we use round brackets, as in A(y1 , . . . , yk ),
then we are implicitly asserting that y1 , . . . , yk is the complete list of free

variables that occur in A.
I.1.12 Deﬁnition. A term or formula is closed iff no free variables occur in it.
A closed formula is called a sentence.
A formula is open iff it contains no quantiﬁers (thus, an open formula may

also be closed).
I.2. A Digression into the Metatheory: Informal
Induction and Recursion
We have already seen a number of inductive or recursive deﬁnitions in Section I.1. The reader, most probably, has already seen or used such deﬁnitions
elsewhere.
We will organize the common important features of inductive deﬁnitions in
this section for easy reference. We will revisit these issues, within the framework
of formal set theory, in due course, but right now we need to ensure that our grasp
of these notions and techniques, at the metamathematical level, is sufﬁcient for
our needs.
One builds a set S by recursion, or inductively (or by induction), out of two
ingredients: a set of initial objects, I , and a set of rules or operations, R. A
member of R – a rule – is a (possibly inﬁnite) table, or relation, like
y1

...

yn

z

a1
b1
..
.

...
...

an
bn
..
.

an+1
bn+1
..
.

If the above rule (table) is called Q, then we use the notations Q(a1 , . . . , an ,
an+1 ) and† a1 , . . . , an , an+1  ∈ Q interchangeably to indicate that the ordered
sequence or “row” a1 , . . . , an , an+1 is present in the table. We say “Q(a1 , . . . ,
an , an+1 ) holds” or “Q(a1 , . . . , an , an+1 ) is true”, but we often also say that
“Q applied to a1 , . . . , an yields an+1 ”, or that “an+1 is a result or output of
Q, when the latter receives input a1 , . . . , an ”. We often abbreviate such inputs
†

“x ∈ A” means that “x is a member of – or is in – A” in the informal set-theoretic sense.

I.2. A Digression into the Metatheory

21

using vector notation, namely, an (or just a , if n is understood). Thus, we often
write Q(
an+1 ) for Q(a1 , . . . , an , an+1 ).
A rule Q that has n + 1 columns is called (n + 1)-ary.
I.2.1 Deﬁnition. We say “a set T is closed under an (n + 1)-ary rule Q” to
mean that whenever c1 , . . . , cn are all in T , then d ∈ T for all d satisfying

Q(c1 , . . . , cn , d).
With these preliminary understandings out of the way, we now state
I.2.2 Deﬁnition. S is deﬁned by recursion, or by induction, from initial objects
I and set of rules R, provided it is the smallest (least inclusive) set with the
properties
(1) I ⊆ S,†
(2) S is closed under every Q in R. In this case we say that S is R-closed.
We write S = Cl(I , R), and say that “S is the closure of I under R”.



We have at once:
I.2.3 Metatheorem (Induction on S). If S = Cl(I , R) and if some set T
satisﬁes
(1) I ⊆ T , and
(2) T is closed under every Q in R,
then S ⊆ T .
Pause. Why is the above a metatheorem?
The above principle of induction on S is often rephrased as follows: To prove
that a “property” P(x) holds for all members of Cl(I , R), just prove that
(a) Every member of I has the property, and
(b) The property propagates with every rule in R, i.e., if P(ci ) holds (is true)
for i = 1, . . . , n, and if Q(c1 , . . . , cn , d) holds, then d too has property
P(x) – that is, P(d) holds.
†

From our knowledge of elementary informal set theory, we recall that A ⊆ B means that every
member of A is also a member of B.

22

I. A Bit of Logic: A User’s Toolbox

Of course, this rephrased principle is valid, for if we let T be the set of all
objects that have property P(x) – for which set one employs the well-established
symbol {x : P(x)} – then this T satisﬁes (1) and (2) of the metatheorem.†
I.2.4 Deﬁnition (Derivations and Parses). A (I , R)-derivation, or simply
derivation – if I and R are understood – is a ﬁnite sequence of objects
d1 , . . . , dn (n ≥ 1) such that each di is
(1) A member of I , or‡
(2) For some (r + 1)-ary Q ∈ R, Q(d j1 , . . . , d jr , di ) holds, and jl < i for
l = 1, . . . , r .
We say that di is derivable within i steps.
A derivation of an object A is also called a parse of a.



Trivially, if d1 , . . . , dn is a derivation, then so is d1 , . . . , dm for any 1 ≤ m < n.
If d is derivable within n steps, it is also derivable in k steps or less for all
k > n, since we can lengthen a derivation arbitrarily by adding I -elements to it.
I.2.5 Remark. The following metatheorem shows that there is a way to “construct” Cl(I , R) iteratively, i.e., one element at a time by repeated application
of the rules.
This result shows deﬁnitively that our inductive deﬁnitions of terms (I.1.5)
and well-formed formulas (I.1.8) fully conform with our working deﬁnition of
theory, as an alphabet and a set of rules that are used to build formulas and

theorems (p. 7).
I.2.6 Metatheorem.
Cl(I , R) = {x : x is (I , R)-derivable within some number of steps, n}
Proof. For notational convenience let us write
T = {x : x is (I , R)-derivable within some number of steps, n}.
As we know from elementary naı̈ve set theory, we need to show here both
Cl(I , R) ⊆ T and Cl(I , R) ⊇ T to settle the claim.
⊆: We do induction on Cl(I , R) (using I.2.3). Now I ⊆ T , since every
member of I is derivable in n = 1 step (why?).
†

‡

We are sailing too close to the wind here. It turns out that not all properties P(x) lead to sets
{x : P(x)}. Our explanation was naı̈ve. However, formal set theory, which is meant to save us
from our naı̈veté, upholds the principle (a)–(b) using just a slightly more complicated explanation.
The reader can see this explanation in Chapter VII.
This “or” is inclusive: (1), or (2), or both.

I.2. A Digression into the Metatheory

23

Also, T is closed under every Q in R. Indeed, let such an (r + 1)-ary Q be
chosen. Let
Q(a1 , . . . , ar , b)

(i)

and {a1 , . . . , ar } ⊆ T . Thus, each ai has a (I , R)-derivation. Concatenate all
these derivations:
. . . , a1 , . . . , a2 , . . . , . . . , ar
The above is a derivation (why?). But then, so is
. . . , a1 , . . . , a2 , . . . , . . . , ar , b
by (i). Thus, b ∈ T .
⊇: We argue this – that is, if d ∈ T , then d ∈ Cl(I , R) – by induction on
the number of steps, n, in which d is derivable.
For n = 1 we have d ∈ I and we are done, since I ⊆ Cl(I , R).
Let us make the induction hypothesis (I.H.) that for derivations of ≤ n steps
the claim is true.
Let then d be derivable within n + 1 steps. Thus, there is a derivation
a1 , . . . , an , d.
Now, if d ∈ I , we are done as above (is this a “real case”?).
If on the other hand Q(a j1 , . . . , a jr , d), then, for i = 1, . . . , r , we have
a ji ∈ Cl(I , R) by the I.H.; hence d ∈ Cl(I , R), since the closure is closed

under all Q ∈ R.
I.2.7 Example. One can see now that N = Cl(I , R), where I = {0} and R
contains just the relation y = x + 1 (input x, output y). Similarly, Z, the set
of all integers, is Cl(I , R), where I = {0} and R contains just the relations
y = x + 1 and y = x − 1 (input x, output y).
For the latter, the inclusion Cl(I , R) ⊆ Z is trivial (by I.2.3). For ⊇ we easily see that any n ∈ Z has a (I , R)-derivation (and then we are done by I.2.6).
For example, if n > 0, then 0, 1, 2, . . . , n is a derivation, while if n < 0, then
0, −1, −2, . . . , n is one. If n = 0, then the one-term sequence 0 is a derivation.
Another interesting closure is obtained by I = {3} and the two relations

z = x + y and z = x − y. This is the set {3k : k ∈ Z} (see Exercise I.1).
Pause. So, taking the ﬁrst sentence of I.2.7 one step further, we note that we
have just proved the induction principle for N, for that is exactly what the
“equation” N = Cl(I , R) says (by I.2.3). Do you agree?
There is another way to view the iterative construction of Cl(I , R): The
set is constructed in stages. Below we are using some more notation borrowed

24

I. A Bit of Logic: A User’s Toolbox

from informal set theory. For any sets A and B we write A ∪ B to indicate the
set union which consists of all the members found in A or B or in both. More
generally, if we have a lot of sets, X 0 , X 1 , X 2 , . . . , that is, one X i for every
integer i ≥ 0 – which we denote by the compact notation (X i )i≥0 – then we
may wish to form a set that includes all the objects found as members all over
the X i , that is (using inclusive, or “logical”, “or”s below), form
{x : x ∈ X 0 or x ∈ X 1 or . . .}
or, more elegantly and precisely,
{x : for some i ≥ 0, x ∈ X i }
The latter is called the union of the sequence (X i )i≥0 and is often denoted by


X i or
Xi
i≥0

i≥0

Correspondingly, we write

i≤n

Xi

or



Xi

i≤n

if we only want to take a ﬁnite union, also indicated clumsily as X 0 ∪ · · · ∪ X n .
I.2.8 Deﬁnition (Stages). In connection with Cl(I , R) we deﬁne the sequence
of sets (X i )i≥0 by induction on n, as follows:
X0 = I

X n+1 =


i≤n


Xi

∪ b : for some Q ∈ R and some an in



X i , Q(
an , b)

i≤n

That is, to form X n+1 we append to i≤n X i all the outputs of all the relations
in R acting on all possible inputs, the latter taken from i≤n X i .
We say that X i is built at stage i, from initial objects I and rule set R. 
In words, at stage 0 we are given the initial objects (X 0 = I ). At stage 1 we
apply all possible relations to all possible objects that we have so far – they
form the set X 0 – and build the ﬁrst stage set, X 1 , by appending the outputs to
what we have so far. At stage 2 we apply all possible relations to all possible
objects that we have so far – they form the set X 0 ∪ X 1 – and build the second
stage set, X 2 , by appending the outputs to what we have so far. And so on.
When we work in the metatheory, we take for granted that we can have
simple inductive deﬁnitions on natural numbers. The reader is familiar with

I.2. A Digression into the Metatheory

25

several such deﬁnitions, e.g.,
a0 = 1
(for a = 0 throughout)
= a · an
a
n+1

We will (meta)prove a general theorem on the feasibility of recursive deﬁnitions
later on (I.2.13).
The following theorem connects stages and closures.
I.2.9 Metatheorem. With the X i as in I.2.8,

Cl(I , R) =
Xi
i≥0

Proof. ⊆: We do induction on Cl(I , R). For the basis, I = X 0 ⊆

i≥0

Xi .

We show that i≥0 X i is R-closed. Let Q ∈ R and Q(
an , b) hold, for some
an in i≥0 X i . Thus, by deﬁnition of union, there are integers j1 , j2 , . . . , jn
such that ai ∈ X ji , i = 1, . . . , n. If k = max{ j1 , . . . , jn }, then an is in i≤k X i ;
hence b ∈ X k+1 ⊆ i≥0 X i .
⊇: It sufﬁces to prove that X n ⊆ Cl(I , R), a fact we can prove by induction
on n. For n = 0 it holds by I.2.2. As an I.H. we assume the claim for all n ≤ k.
The case for k + 1: X k+1 is the union of two sets. One is
a subset of Cl(I , R) by the I.H. The other is
b : for some Q ∈ R and some a in



i≤k

X i . This is

X i , Q(
a , b)

i≤k

This too is a subset of Cl(I , R), by the preceding observation and the fact that

Cl(I , R) is R-closed.
N.B. An inductively deﬁned set can be built by stages.
I.2.10 Deﬁnition (Immediate Predecessors; Ambiguity). If d ∈ Cl(I , R)
and for some Q and a1 , . . . , ar it is the case that Q(a1 , . . . , ar , d), then the
a1 , . . . , ar are immediate Q-predecessors of d, or just immediate predecessors
if Q is understood; for short, i.p.
A pair (I , R) is called ambiguous if some d ∈ Cl(I , R) satisﬁes any
(or all) of the following conditions:
(i) It has two (or more) distinct sets of immediate P-predecessors for some
rule P.

26

I. A Bit of Logic: A User’s Toolbox

(ii) It has both immediate P-predecessors and immediate Q-predecessors, for
P = Q.
(iii) It is a member of I , yet it has immediate predecessors.
If (I , R) is not ambiguous, then it is unambiguous.



I.2.11 Example. The pair ({00, 0}, {Q}), where Q(x, y, z) holds iff z = x y
(where “x y” denotes the concatenation of the strings x and y, in that order), is
ambiguous. For example, 0000 has the two immediate predecessor sets {00, 00}
and {0, 000}. Moreover, while 00 is an initial object, it does have immediate
predecessors – namely, the set {0, 0} (or, what amounts to the same thing, {0}).


I.2.12 Example. The pair (I , R) where I = {3} and R consists of z = x + y
and z = x − y is ambiguous. Even 3 has (inﬁnitely many) distinct sets of i.p.
(e.g., any {a, b} such that a + b = 3, or a − b = 3).
The pairs that effect the deﬁnition of Term (I.1.5) and Wff (I.1.8) are un
ambiguous (see Exercises I.2 and I.3).
I.2.13 Metatheorem (Deﬁnition by Recursion). Let (I , R) be unambiguous,
and Cl(I , R) ⊆ A, where A is some set. Let also Y be a set, and† h : I → Y
and g Q , for each Q ∈ R, be given functions. For any (r +1)-ary Q, an input for
the function g Q is a sequence a, b1 , . . . , br , where a is in A and the b1 , . . . , br
are all in Y . All the g Q yield outputs in Y .
Under these assumptions, there is a unique function f : Cl(I , R) → Y
such that

y = h(x)
and x ∈ I



or, for some Q ∈ R,
(1)
y = f (x) iff

y = g Q (x, o1 , . . . , or ) and Q(a1 , . . . , ar , x) holds,


where oi = f (ai ) for i = 1, . . . , r
The reader may wish to skip the proof on ﬁrst reading.
 by‡
Proof. Existence part. For each (r + 1)-ary Q ∈ R, deﬁne Q


 a1 , o1 , . . . , ar , or , b, g Q (b, o1 , . . . , or ) iff Q(a1 , . . . , ar , b)
Q
†
‡

(2)

The notation f : A → B is common in informal (and formal) mathematics. It denotes a function
f that receives “inputs” from the set A and yields “outputs” in the set B.
For a relation Q, writing just “Q(a1 , . . . , ar , b)” is equivalent to writing “Q(a1 , . . . , ar , b) holds”.

I.2. A Digression into the Metatheory

27

 is effected for all possible
For any a1 , . . . , ar , b, the above deﬁnition of Q
choices of o1 , . . . , or such that g Q (b, o1 , . . . , or ) is deﬁned.
 to form a set of rules R.

Collect now all the Q

Let also I = {x, h(x) : x ∈ I }.
) is a 2-ary relation that for every
We will verify that the set F = Cl(I, R
input yields at most one output, and therefore is a function. For such a relation
it is customary to write, letting the context fend off the obvious ambiguity in
the use of the letter F,
y = F(x)

iff

F(x, y)

(∗)

We will further verify that replacing f in (1) above by F results in a valid
equivalence (the “iff” holds). That is, F satisﬁes (1).
(a) We establish that F is a relation composed of pairs x, y (x is input, y is
output) where x ∈ Cl(I , R) and y ∈ Y . This follows easily by induction
on F (I.2.3), since I ⊆ F, and the property (of containing such pairs)
 (recall that the g Q yield outputs in Y ).
propagates with each Q
(b) We next show “if x, y ∈ F and x, z ∈ F, then y = z” – that is, F is
single-valued, or well deﬁned, in short, it is a function. We again employ
induction on F, thinking of the quoted statement as a “property” of the
pair x, y: Suppose that x, y ∈ I and let also x, z ∈ F. By I.2.6,
 1 , o1 , . . . , ar , or , x, z), where Q(a1 , . . . , ar , x) and
x, z ∈ I, or Q(a
 and a1 , o1 , . . . , ar , or 
z = g Q (x, o1 , . . . , or ), for some (r + 1)-ary Q
in F. The right hand side of the italicized “or” cannot hold for an unambiguous (I , R), since x cannot have i.p. Thus x, z ∈ I, hence y =
 let
h(x) = z. To prove that the property propagates with each Q,
 1 , o1 , . . . , ar , or , x, y)
Q(a
but also

P(b1 , o1 , . . . , bl , ol , x, z)
where Q(a1 , . . . , ar , x), P(b1 , . . . , bl , x), and
y = g Q (x, o1 , . . . , or )

and

z = g P (x, o1 , . . . , ol )

(3)

= 
Since (I , R) is unambiguous, Q = P (hence also Q
P), r = l, and

ai = bi , for i = 1, . . . , r . By the I.H., oi = oi , for i = 1, . . . , r ; hence
y = z by (3).

28

I. A Bit of Logic: A User’s Toolbox

 ), to
(c) Finally, we show that F satisﬁes (1). We do induction on Cl(I, R
prove ←: If x ∈ I and y = h(x), then F(x, y) (i.e., y = F(x) in the
alternative notation (∗)), since I ⊆ F. Let next y = g Q (x, o1 , . . . , or )
and
 i = 1, . . . , r . By (2),
 Q(a1 , . . . , ar , x), where also F(ai , oi ), for
 a1 , o1 , . . . , ar , or , x, g Q (x, o1 , . . . , or ) ; thus – F being closed unQ
der all the rules in 
R – F(x, g Q (b, o1 , . . . , or )) holds, in short, F(x, y) or
y = F(x). For →, now we assume that F(x, y) holds and we want to infer
the right hand side (of iff ) in (1). We employ Metatheorem I.2.6.
Case 1. Let x, y be F-derivable† in n = 1 step. Then x, y ∈ I. Thus
y = h(x).
Case 2. Suppose next that x, y is F-derivable within n + 1 steps, namely,
we have a derivation
x1 , y1 , x2 , y2 , . . . , xn , yn , x, y

(4)

 1 , o1 , . . . , ar , or , x, y) and Q(a1 , . . . , ar , x) (see (2)), and
where Q(a
each of a1 , o1 , . . . , ar , or  appears in the above derivation, to the left of
x, y. This entails (by (2)) that y = g Q (x, o1 , . . . , or ). Since the ai , oi 
appear in (4), F(ai , oi ) holds for i = 1, . . . , r . Thus, x, y satisﬁes the
right hand side of iff in (1), once more.
Uniqueness part. Let the function K also satisfy (1). We show, by induction
on Cl(I , R), that
for all x ∈ Cl(I , R) and all y ∈ Y,

y = F(x) iff y = K (x)

(5)

→: Let x ∈ I , and y = F(x). By lack of ambiguity, the case conditions
of (1) are mutually exclusive. Thus, it must be that y = h(x). But then, y = K (x)
as well, since K satisﬁes (1) too.
Let now Q(a1 , . . . , ar , x) and y = F(x). By (1), there are (unique, as
we now know) o1 , . . . , or such that oi = F(ai ) for i = 1, . . . , r , and y =
g Q (x, o1 , . . . , or ). By the I.H., oi = K (ai ). But then (1) yields y = K (x) as
well (since K satisﬁes (1)).
←:

Just interchange the letters F and K in the above argument.



The above clearly is valid for functions h and g Q that may fail to be deﬁned
everywhere in their “natural” input sets. To be able to have this degree of
generality without having to state additional deﬁnitions (such as those of left
ﬁelds, right ﬁelds, partial functions, total functions, nontotal functions, and
Kleene weak equality) we have stated the recurrence (1) the way we did (to
†

)-derivable.
Cl(I, R

I.3. Axioms and Rules of Inference

29

keep an eye on both the input and output side of things) rather than the usual

h(x)
if x ∈ I
f (x) =
g Q (x, f (a1 ), . . . , f (ar )) if Q(a1 , . . . , ar , x) holds,
Of course, if all the g Q and h are deﬁned everywhere on their input sets (i.e.,
they are “total”), then f is deﬁned everywhere on Cl(I , R) (see Exercise I.4).
I.3. Axioms and Rules of Inference
Now that we have our language L, we will embark on using it to formally
effect deductions. These deductions start at the axioms. Deductions employ
“acceptable”, purely syntactic – i.e., based on form, not on substance – rules
that allow us to write a formula down (to deduce it) solely because certain other
formulas that are syntactically related to it were already deduced (i.e., already
written down). These string-manipulation rules are called rules of inference.
We describe in this section the axioms and the rules of inference that we will
accept into our logical calculus and that are common to all theories.
We start with a precise deﬁnition of tautologies in our ﬁrst order language L.
I.3.1 Deﬁnition (Prime Formulas in Wff. Propositional Variables). A formula A ∈ Wff is a prime formula or a propositional variable iff it is either
Pri1. atomic or
Pri2. a formula of the form ((∃x)A ).
We use the lowercase letters p, q, r (with or without subscripts or primes) to
denote arbitrary prime formulas (propositional variables) of our language. 
That is, a prime formula either has no propositional connectives, or if it does,
it hides them inside the scope of (∃x).
We may think of a propositional variable as a “blob of ink” that is all that a
myopic being makes out of a formula described in I.3.1. The same being will
see an arbitrary well-formed formula as a bunch of blobs, brackets and Boolean
connectives (¬, ∨), “correctly connected” as stipulated below.†
I.3.2 Deﬁnition (Propositional Formulas). The set of propositional formulas
over V , denoted here by Prop, is the smallest set such that:
(1) Every propositional variable (over V ) is in Prop.
(2) If A and B are in Prop, then so are (¬A) and (A ∨ B ).
†

Interestingly, our myope can see the brackets and the Boolean connectives.



30

I. A Bit of Logic: A User’s Toolbox

I.3.3 Metatheorem. Prop = Wff.
Proof. ⊆: We do induction on Prop. Every item in I.3.2(1) is in Wff. Wff
satisﬁes I.3.2(2) (see I.1.8(b)). Done.
⊇: We do induction on Wff. Every item in I.1.8(a) is a propositional variable
(over V ), and hence is in Prop.
Prop trivially satisﬁes I.1.8(b). It also satisﬁes I.1.8(c), for if A is in Prop,
then it is in Wff by the ⊆-direction above. Then, by I.3.1, ((∃x)A) is a propositional variable, and hence in Prop.

We are done once more.
I.3.4 Deﬁnition (Propositional Valuations). We can arbitrarily assign a value
of 0 or 1 to every A in Wff (or Prop) as follows:
(1) We ﬁx an assignment of 0 or 1 to every prime formula. We can think of this
as an arbitrary but ﬁxed function v : {all prime formulas over L} → {0, 1}
in the metatheory.
(2) We deﬁne by recursion an extension of v, denoted by v̄:
v̄((¬A)) = 1 − v̄(A)
v̄((A ∨ B )) = v̄(A ) · v̄(B )
where “·” above denotes number multiplication.
We call, traditionally, the values 0 and 1 by the names “true” and “false”
respectively, and write t and f respectively.
We also call a valuation v a truth (value) assignment.
We use the jargon “A takes the truth value t (respectively, f) under a valu
ation v” to mean “v̄(A ) = 0 (respectively, v̄(A) = 1)”.
The above inductive deﬁnition of v̄ relies on the fact that Deﬁnition I.3.2 of
Prop is unambiguous (I.2.10, p. 25), so that a propositional formula is uniquely
readable (or parsable) (see Exercises I.5 and I.6). It employs the metatheorem
on recursive deﬁnitions (I.2.13).
The reader may think that all this about unique readability is just an annoying
quibble. Actually it can be a matter of life or death. The ancient Oracle of
Delphi had the nasty habit of issuing ambiguous – not uniquely readable, that
is – pronouncements. One famous such pronouncement, rendered in English,
went like this: “You will go you will return not dying in the war”.† Given that
†

The original was “I ξ εις αϕιξ εις oυ θ νηξ εις εν π oλεµ ω”.
ι

I.3. Axioms and Rules of Inference

31

ancient Greeks did not use punctuation, the above has two diametrically opposite
meanings depending on whether you put a comma before or after “not”.
The situation with formulas in Prop would have been as disastrous in the
absence of brackets – which serve as punctuation – because unique readability
would then not be guaranteed: For example, for three distinct prime formulas
p, q, r we could ﬁnd a v such that v( p → q → r ) depended on whether we meant
to insert brackets around “ p → q” or around “q → r ” (can you ﬁnd such a v?).
I.3.5 Remark (Truth Tables). Deﬁnition I.3.4 is often given in terms of truth
functions. For example, we could have deﬁned (in the metatheory, of course)
the function F¬ : {t, f} → {t, f} by

t if x = f
F¬ (x) =
f
if x = t
We could then say that v̄((¬A)) = F¬ (v̄(A)). One can similarly take care of
all the connectives (∨ and all the abbreviations) with the help of truth functions
F∨ , F∧ , F→ , F↔ . These functions are conveniently given via so-called truth
tables as indicated below:
x

y

F¬ (x)

F∨ (x, y)

F∧ (x, y)

F→ (x, y)

F↔ (x, y)

f
f
t
t

f
t
f
t

t
t
f
f

f
t
t
t

f
f
f
t

t
t
f
t

t
f
f
t


I.3.6 Deﬁnition (Tautologies, Satisﬁable Formulas, Unsatisﬁable Formulas
in Wff). A formula A ∈ Wff (equivalently, in Prop) is a tautology iff for all
valuations v, v̄(A) = t.
We call the set of all tautologies, as deﬁned here, Taut. The symbol |=Taut A
says “A is in Taut”.
A formula A ∈ Wff (equivalently, in Prop) is satisﬁable iff for some
valuation v, v̄(A ) = t. We say that v satisﬁes A.
A set of formulas  is satisﬁable iff for some valuation v, v̄(A) = t for
every A in . We say that v satisﬁes .

32

I. A Bit of Logic: A User’s Toolbox

A formula A ∈ Wff (equivalently, in Prop) is unsatisﬁable iff for all
valuations v, v̄(A) = f. A set of formulas  is unsatisﬁable iff for all valuations
v, v̄(A) = f for some A in .

“Satisﬁable” and “unsatisﬁable” are terms introduced here in the propositional
or Boolean sense. These terms have a more complicated meaning when we
decide to “see” the object variables and quantiﬁers that occur in formulas.
I.3.7 Deﬁnition (Tautologically Implies, for Formulas in Wff ). Let A and
 be respectively any formula and any set of formulas (over L). The symbol
 |=Taut A, pronounced “ tautologically implies A ”, means that every truth
assignment v that satisﬁes  also satisﬁes A.

We have at once
I.3.8 Lemma.†  |=Taut A iff  ∪ {¬A } is unsatisﬁable (in the propositional
sense).
If  = ∅, then  |=Taut A says just |=Taut A , since the hypothesis “every truth
assignment v that satisﬁes ”, in the deﬁnition above, is vacuously satisﬁed.
For that reason we almost never write ∅ |=Taut A and write instead |=Taut A.
I.3.9 Exercise. For any formula A and any two valuations v and v  , v̄(A) =
v̄  (A) if v and v  agree on all the propositional variables that occur in A.
In the same manner,  |=Taut A is oblivious to v-variations that do not

affect the variables that occur in  and A (see Exercise I.7).
Before presenting the axioms, we need to introduce the concept of substitution.
I.3.10 Tentative Deﬁnition (Substitution of a Term for a Variable). Let A
be a formula, x an (object) variable, and t a term.
A [x ← t] denotes the result of “replacing” all free occurrences of x in A
by the term t, provided no variable of t was “captured” (by a quantiﬁer) during
†

The word “lemma” has Greek origin, “λήµµα”, plural “lemmata” – many people say “lemmas” –
from “ήµµατ α”. It derives from the verb “λαµβ άνω” (to take) and thus means “taken thing”.
In mathematical reasoning a lemma is a provable auxiliary statement that is taken and used as
a stepping stone in lengthy mathematical arguments – invoked therein by name, as in “. . . by
Lemma such and such . . . ” – much as subroutines (or procedures) are taken and used as auxiliary
stepping stones to elucidate lengthy computer programs. Thus our purpose in having lemmata is
to shorten proofs by breaking them up into modules.

I.3. Axioms and Rules of Inference

33

substitution. If the proviso is valid, then we say that “t is substitutable for x
(in A)”, or that “t is free for x (in A)”.
If the proviso is not valid, then the substitution is undeﬁned.

I.3.11 Remark. There are a number of issues about Deﬁnition I.3.10 that need
discussion or clariﬁcation.
Any reasonable person will be satisﬁed with the above deﬁnition “as is”.
However, there are some obscure points (deliberately quoted, above).
(1) What is this about “capture”? Well, suppose that A ≡ (∃x)¬x = y. Let
t ≡ x.† Then, if we ignore the provison in I.3.10, A [y ← t] ≡ (∃x)¬x =
x, which says something altogether different than the original. Intuitively,
this is unexpected (and undesirable): A codes a statement about the free
variable y, i.e., a statement about all objects which could be values (or
meanings) of y. One would have expected that, in particular, A [y ← x] –
if the substitution were allowed – would make this very same statement
about the values of x. It does not.‡ What happened is that x was captured
by the quantiﬁer upon substitution, thus distorting A’s original meaning.
(2) Are we sure that the term “replace” is mathematically precise?
(3) Is A [x ← t] always a formula, if A is?
A revisitation of I.3.10 via an inductive deﬁnition (by induction on terms
and formulas) settles (1)–(3) at once (in particular, the intuitive terms “replace”
and “capture” do not appear in the inductive deﬁnition). Here it goes:
First off, let us deﬁne s[x ← t], where s is also a term, by cases:


t
if s ≡ x




if s ≡ a, a constant
a
s[x ← t] ≡
(symbol)



y
if
s
≡
y, a variable ≡ x


 f r [x ← t]r [x ← t] . . . r [x ← t] if s ≡ f r . . . r
1
2
n
1
n
Pause. Is s[x ← t] always a term? That this is so follows directly by induction
on terms, using the deﬁnition by cases above and the I.H. that each of ri [x ← t],
i = 1, . . . , n, is a term.
†
‡

Recall that in I.1.4 (p. 13) we deﬁned the symbol “≡” to be equality on strings. No further
reminders will be issued.
And that is why the substitution is not allowed. The original formula says that for any object y
there is an object that is different from it. On the other hand, A [y ← x] says that there is an
object that is different from itself.

34

I. A Bit of Logic: A User’s Toolbox

We turn now to formulas. The symbols P, r, s (with or without subscripts)
below denote a predicate of arity n, a term and a term (respectively).

s[x ← t] = r [x ← t]
if A ≡ s = r




Pr1 [x ← t]r2 [x ← t] . . . rn [x ← t] if A ≡ Pr1 . . . rn




(B [x ← t] ∨ C [x ← t])
if A ≡ (B ∨ C )





 ¬(B [x ← t])
if A ≡ (¬B )

A [x ← t] ≡ A
if A ≡ ((∃y)B ) and



y≡x






(∃y)(B [x ← t])
if A ≡ ((∃y)B ) and




y ≡ x and y does



not occur in t
In all cases above, the left hand side is deﬁned iff the right hand side is.
Pause. We have eliminated “replaces” and “captured”. Is though A [x ← t] a

formula (whenever it is deﬁned)? (See Exercise I.8.)
I.3.12 Deﬁnition (Simultaneous Substitution). The symbols A [y1 , . . . , yr ←
t1 , . . . , tr ] or, equivalently, A [yr ← tr ] – where yr is an abbreviation of
y1 , . . . , yr – denote simultaneous substitution of the terms t1 , . . . , tr into the
variables y1 , . . . , yr in the following sense: Let zr be variables that do not occur
at all (either as free or bound) in either A or tr . Then A [yr ← tr ] is short for
A [y1 ← z 1 ] . . . [yr ← zr ][z 1 ← t1 ] . . . [zr ← tr ]

(1)


Exercise I.9 shows that we obtain the same string in (1) above, regardless of
our choice of new variables zr .
More conventions: The symbol [x ← t] lies in the metalanguage. This
metasymbol has the highest priority, so that, e.g., A ∨ B [x ← t] means
A ∨ (B [x ← t]), (∃x)B [x ← t] means (∃x)(B [x ← t]), etc.
We often write A [y1 , . . . , yr ], rather than the terse A, in order to convey
our interest in the free variables y1 , . . . , yr that may or may not actually appear
free in A. Other variables, not mentioned in the notation, may also be free in
In this context, if t1 , . . . , tr are terms, the symbol A [t1 , . . . , tr ] abbreviates
A [yr ← tr ].
We are ready to introduce the (logical) axioms and rules of inference.

I.3. Axioms and Rules of Inference

35

Schemata.† Some of the axioms below will actually be schemata. A formula
schema, or formula form, is a string G of the metalanguage that contains syntactic variables (or metavariables), such as A, P, f, a, t, x.
Whenever we replace all these syntactic variables that occur in G by speciﬁc formulas, predicates, functions, constants, terms, or variables respectively,
we obtain a speciﬁc well-formed formula, a so-called instance of the schema.
For example, an instance of (∃x)x = a is (∃v12 )v12 = 0 (in the language of
Peano arithmetic). An instance of A → A is v101 = v114 → v101 = v114 .
I.3.13 Deﬁnition (Axioms and Axiom Schemata). The logical axioms are all
the formulas in the group Ax1 and all the possible instances of the schemata in
the remaining groups:
Ax1. All formulas in Taut.
Ax2. (Substitution axiom. Schema)
A [x ← t] → (∃x)A

for any term t.

By I.3.10–I.3.11, the notation already imposes a condition on t, that it is substitutable for x.
N.B. We often see the above written as
A [t] → (∃x) A [x]
or even
A [t] → (∃x)A
Ax3. (Schema) For each object variable x, the formula x = x.
Ax4. (Leibniz’s characterization of equality – ﬁrst order version. Schema) For
any formula A , object variable x, and any terms t and s, the formula
t = s → (A [x ← t] ↔ A [x ← s])
N.B. The above is written usually as
t = s → (A [t] ↔ A [s])
as long as we remember that the notation already requires that t and s be free
for x. We will denote the above set of logical axioms .

†

Plural of schema. This is of Greek origin, σ χ ήµα, meaning – e.g., in geometry – ﬁgure or
conﬁguration or even formation.

36

I. A Bit of Logic: A User’s Toolbox

The logical axioms for equality are not the strongest possible, but they are
adequate for the job. What Leibniz really proposed was the schema t = s ↔
(∀P)(P[t] ↔ P[s]), which says, intuitively, that “two objects t and s are equal
iff, for every property P, both have P or neither has P”.
Unfortunately, our system of notation (ﬁrst-order language) does not allow
quantiﬁca```
{"ft_lang_label":"__label__en","ft_lang_prob":0.9146415,"math_prob":0.93472207,"size":103247,"snap":"2019-13-2019-22","text_gpt3_token_len":27556,"char_repetition_ratio":0.14850402,"word_repetition_ratio":0.060074706,"special_character_ratio":0.2628357,"punctuation_ratio":0.16106284,"nsfw_num_words":0,"has_unicode_error":false,"math_prob_llama3":0.98151636,"pos_list":[0,1,2],"im_url_duplicate_count":[null,1,null],"WARC_HEADER":"{\"WARC-Type\":\"response\",\"WARC-Date\":\"2019-03-22T10:14:39Z\",\"WARC-Record-ID\":\"<urn:uuid:140302b9-cf77-4d8d-8041-b7c4491c0df4>\",\"Content-Length\":\"138671\",\"Content-Type\":\"application/http; msgtype=response\",\"WARC-Warcinfo-ID\":\"<urn:uuid:ee00ccc6-e82b-4bd5-ab84-724804c30f50>\",\"WARC-Concurrent-To\":\"<urn:uuid:b1d478f1-1a8c-4a33-91e3-fa72cee3d6e2>\",\"WARC-IP-Address\":\"5.45.79.90\",\"WARC-Target-URI\":\"https://b-ok.xyz/book/1024112/d8ae30\",\"WARC-Payload-Digest\":\"sha1:YAWZ2CMJZRZEAKCR5YADBEBYO3RMKZY5\",\"WARC-Block-Digest\":\"sha1:VABDTBF5QA3623XO622L46JEF6LXE63E\",\"WARC-Identified-Payload-Type\":\"text/html\",\"warc_filename\":\"/cc_download/warc_2019/CC-MAIN-2019-13/CC-MAIN-2019-13_segments_1552912202642.32_warc_CC-MAIN-20190322094932-20190322120932-00444.warc.gz\"}"}