TEXS AND MONOGRAPHS IN COMPUTER SCIENCE
A LOGICAL APPROACH
TO DISCR
David Gr.e
Fred B. Schneider
MATH
I
-TL
-
I neorem:
(Vx I P * Q)
g- S : * '-
{x P} C {x [ Q}
q
Proof:
{x I P} C {x [ Q}
(Def. of Subset C,,, with v not
occurring free in P or Q)
I v {x P}:v E{x I Q})
( (V
|x
I RI
-= R
A: iv:wice)
(Vv I P[x - v] : Q[* := v])
(Trading; Dummy renaming
(YX I P[x - v][v:Ax XI
Q[x - vv :] = x])
|
(R[x:V][v:XI = R if v
does not occur free in 'R twce
(VxI: P =iQ Q)
f
<
.
.
iE
iti;
.
g
.
/
.
Ps
@1
L:s
..
4
:
gAlwz
SprinWrQrlag
X ME
y,
Table of Precedences
[x := e] (textual substitution)
. (function application)
unary prefix operators: +
**
* / ± mod gcd
+ - u n x o -
#I
-
>
C D
= < > G C C D 2
V A
(highest precedence)
- #
P
(conjunctional, see page 29)
-
(lowest precedence)
(a)
(b)
(c)
(d)
(e)
(f)
(g)
(h)
(i)
(j)
(k)
(1)
(m)
All nonassociative binary infix operators associate to the left, except **,
a , and ', which associate to the right.
The operators on lines (j), (1), and (in) may have a slash /
them to denote negation -e.g.
through
b # c is an abbreviation for -(b =- c) .
Greek letters and their Transliterations
Name
Alpha
Beta
Gamma
Delta
Epsilon
Zeta
Eta
Theta
a
fi
y
6
e
Sign It.
a
b
g
d
e
z
e
th
7i
V
Name
Iota
b
Kappa
n
Lambda A
Mu
Nu
Xi
Omicron
Pi
Sign Tr.
i
k
I
A m
n
v
x
o
p
o
7r
Name
Rho
Sigma
Tau
Upsilon
Phi
Chi
Psi
Omega
Types Used in this Text
Sign TPr.
r
s
t
p
a
r-
v
0
X
4b
w
y, u
ph
ch
ps
o
z
N
Z+
2-
Q
P
integer
nat
positive
negative
rational
reals
positive reals R+
bool
sets
bags
sequences
integers: . .. ,-3,-2,-1,0,1,2,3....
natural numbers: 0, 1, 2 ..
positive integers: 1, 2, 3 ....
negative integers: 1, 2, 3,...
rationals i/i for ii
real numbers
positive real numbers
booleans: true, false
B
set of elements of type t
set (t)
bag(t) bag of elements of type t
seq(t)
sequence of elements of type t
integers, j $4 0
Texts and Monographs in Computer Science
Editors
David Gries
Fred B. Schneider
Advisory Board
F.L. Bauer
S.D. Brookes
C.E. Leiserson
M. Sipser
Texts and Monographs in Computer Science
Suad Alagic
Object-Oriented Database Programming
1989. XV, 320 pages, 84 illus.
Suad Alagic
Relational Database Technology
1986. Xl, 259 pages, 114 illus.
Suad Alagic and Michael A. Arbib
The Design of Well-Structured and Correct Programs
1978. X, 292 pages, 68 illus.
S. Thomas Alexander
Adaptive Signal Processing: Theory and Applications
1986. IX, 179 pages, 42 illus.
Krzysztof R. Apt and Ernst-Rudiger Olderog
Verification of Sequential and Concurrent Programs
1991. XVI, 441 pages
Michael A. Arbib, A.J. Kfoury, and Robert N. Moll
A Basis for Theoretical Computer Science
1981. VIII, 220 pages, 49 illus.
Friedrich L. Bauer and Hans Wossner
Algorithmic Language and Program Development
1982. XVI, 497 pages, 109 illus.
W. Bischofberger and G. Pomberger
Prototyping-Orlented Software Development: Concepts and Tools
1992. XI, 215 pages, 89 illus.
Ronald V. Book and Friedrich Otto
String-Rewriting Systems
1993. Vii, 200 pages
Kaare Christian
A Guide to Modula-2
1986. XIX, 436 pages, 46 illus.
Edsger W. Dijkstra
Selected Writings on Computing: A Personal Perspective
1982. XVII, 362 pages, 13 illus.
(continued after ind4
A Logical Approach
to Discrete Math
David Gries
Fred B. Schneider
With 25 Illustrations
I
Springer-Verlag
New York Berlin Heidelberg London Paris
Tokyo Hong Kong Barcelona Budapest
David Gries
Department of Computer Science
Cornell University
Upson Hall
Ithaca, NY 14853-7501
USA
Fred B. Schneider
Department of Computer Science
Cornell University
Upson Hall
Ithaca, NY 14853-7501
USA
Library of Congress Cataloging-in-Publication Data
Gries, David.
11st ed]
A logical approach to discrete math / David Gries and Fred B.
cm. -
(Texts and monographs in computer science)
Includes bibliographical references and index.
ISBN 0-387-94115-0
1. Mathematics.
I. Schneider, Fred B. II. Title.
Schneider.
p.
QA39.2.G7473 1994
51 0-dc2O
Ill. Series.
93-27848
Printed on acid-free paper.
© 1993 Springer-Verlag New York, Inc.
All rights reserved. This work may not be translated or copied in whole or in part with(
the written permission of the publisher (Springer-Verlag New York, Inc., 175 Fifth Aveni
New York, NY 10010, USA), except for brief excerpts in connection with reviews or sc&
arly analysis. Use in connection with any form of information storage and retrieval, ell
tronic adaptation, computer software, or by similar or dissimilar methodology now kno,
or hereafter developed is forbidden.
The use of general descriptive names, trade names, trademarks, etc., in this publication
even if the former are not especially identified, is not to be taken as a sign that such naml
as understood by the Trade Marks and Merchandise Marks Act, may accordingly be us
freely by anyone.
Production managed by Hal Henglein; manufacturing supervised by Jacqui Ashri.
Photocomposed copy produced from the authors' LaTeX files.
Printed and bound by Braun-Brumfield, Ann Arbor, Ml.
Printed in the United States of America.
987654321
ISBN 0-387-94115-0 Springer-Verlag New York Berlin Heidelberg
ISBN 3-540-94115-0 Springer-Verlag Berlin Heidelberg New York
To the women in our lives,
Elaine and Mimi
Preface
This text attempts to change the way we teach logic to beginning students.
Instead of teaching logic as a subject in isolation, we regard it as a basic
tool and show how to use it. We strive to give students a skill in the propo-
sitional and predicate calculi and then to exercise that skill thoroughly in
applications that arise in computer science and discrete mathematics.
We are not logicians, but programming methodologists, and this text
reflects that perspective. We are among the first generation of scientists
who are more interested in using logic than in studying it. With this text,
we hope to empower further generations of computer scientists and math-
ematicians to become serious users of logic.
Logic is the glue
Logic is the glue that binds together methods of reasoning, in all domains.
The traditional proof methods -for example, proof by assumption, con-
tradiction, mutual implication, and induction- have their basis in formal
logic. Thus, whether proofs are to be presented formally or informally, a
study of logic can provide understanding.
But we want to impart far more than the anatomy of the glue
proof
theory and model theory. We want to impart a skill in its use. For this rea-
son, we emphasize syntactic manipulation of formulas as a powerful tool for
discovering and certifying truths. Of course, syntactic manipulation cannot
completely replace thinking about meaning. However, the discomfort with
and reluctance to do syntactic manipulation that accompanies unfamiliar-
ity with the process unnecessarily forces all reasoning to be in terms of
meaning. Our goal is to balance the tendency to reason semantically with
the ability to perform syntactic reasoning. Students thereby acquire under-
standing of when syntactic reasoning is more suitable, as well as confidence
in applying it.
When we teach the propositional and predicate calculi, students are put
in a syntactic straightjacket. Proofs must be written rigorously. This is an
advantage, not a disadvantage, because students learn what it means for a
proof to be rigorous and that rigor is easily achieved. We also describe prin-
ciples and strategies for developing proofs and go over several proofs for the
same theorem, discussing their advantages and disadvantages. Gradually,