. 1
( 107 .)



>>

LANGUAGE,
PROOF AND
LOGIC
JON BARWISE & JOHN ETCHEMENDY

In collaboration with
Gerard Allwein
Dave Barker-Plummer
Albert Liu




SEVEN BRIDGES PRESS
7
7




NEW YORK • LONDON
Copyright © 1999
CSLI Publications
Center for the Study of Language and Information
Leland Stanford Junior University
03 02 01 00 99 54321



Librar y of Congress Cataloging-in-Publication Data

Bar wise, Jon.


Language, proof and logic / Jon Bar wise and John Etchemendy ;
in collaboration with Gerard Allwein, Dave Barker-Plummer, and
Albert Liu.

p. cm.

ISBN 1-889119-08-3 (pbk. : alk. paper)
I. Etchemendy, John, 1952- II. Allwein, Gerard, 1956-
III. Barker-Plummer, Dave. IV. Liu, Albert, 1966- V. Title.
IN PROCESS

99-41113
CIP
Acknowledgements

Our primary debt of gratitude goes to our three main collaborators on this
project: Gerry Allwein, Dave Barker-Plummer, and Albert Liu. They have
worked with us in designing the entire package, developing and implementing
the software, and teaching from and re¬ning the text. Without their intelli-
gence, dedication, and hard work, LPL would neither exist nor have most of
its other good properties.
In addition to the ¬ve of us, many people have contributed directly and in-
directly to the creation of the package. First, over two dozen programmers have
worked on predecessors of the software included with the package, both earlier
versions of Tarski™s World and the program Hyperproof, some of whose code
has been incorporated into Fitch. We want especially to mention Christopher
Fuselier, Mark Greaves, Mike Lenz, Eric Ly, and Rick Wong, whose outstand-
ing contributions to the earlier programs provided the foundation of the new
software. Second, we thank several people who have helped with the develop-
ment of the new software in essential ways: Rick Sanders, Rachel Farber, Jon
Russell Barwise, Alex Lau, Brad Dolin, Thomas Robertson, Larry Lemmon,
and Daniel Chai. Their contributions have improved the package in a host of
ways.
Prerelease versions of LPL have been tested at several colleges and uni-
versities. In addition, other colleagues have provided excellent advice that we
have tried to incorporate into the ¬nal package. We thank Selmer Bringsjord,
Renssalaer Polytechnic Institute; Tom Burke, University of South Carolina;
Robin Cooper, Gothenburg University; James Derden, Humboldt State Uni-
versity; Josh Dever, SUNY Albany; Avrom Faderman, University of Rochester;
James Garson, University of Houston; Ted Hodgson, Montana State Univer-
sity; John Justice, Randolph-Macon Women™s College; Ralph Kennedy, Wake
Forest University; Michael O™Rourke, University of Idaho; Greg Ray, Univer-
sity of Florida; Cindy Stern, California State University, Northridge; Richard
Tieszen, San Jose State University; Saul Traiger, Occidental College; and Lyle
Zynda, Indiana University at South Bend. We are particularly grateful to John
Justice, Ralph Kennedy, and their students (as well as the students at Stan-
ford and Indiana University), for their patience with early versions of the
software and for their extensive comments and suggestions.
We would also like to thank Stanford™s Center for the Study of Language
and Information and Indiana University™s College of Arts and Sciences for



iii
iv / Acknowledgements


their ¬nancial support of the project. Finally, we are grateful to our two
publishers, Dikran Karagueuzian of CSLI Publications and Clay Glad of Seven
Bridges Press, for their skill and enthusiasm about LPL.




Acknowledgements
Contents

Acknowledgements iii

Introduction 1
The special role of logic in rational inquiry . . . . . . . . . . . . . . 1
Why learn an arti¬cial language? . . . . . . . . . . . . . . . . . . . . 2
Consequence and proof . . . . . . . . . . . . . . . . . . . . . . . . . . 4
Instructions about homework exercises (essential! ) . . . . . . . . . . 5
To the instructor . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10
Web address . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15


I Propositional Logic 17
1 Atomic Sentences 19
1.1 Individual constants . . . . . . . . . . . . . . . . . . . . . . . . 19
1.2 Predicate symbols . . . . . . . . . . . . . . . . . . . . . . . . . 20
1.3 Atomic sentences . . . . . . . . . . . . . . . . . . . . . . . . . . 23
1.4 General ¬rst-order languages . . . . . . . . . . . . . . . . . . . 28
1.5 Function symbols (optional ) . . . . . . . . . . . . . . . . . . . . 31
1.6 The ¬rst-order language of set theory (optional ) . . . . . . . . 37
1.7 The ¬rst-order language of arithmetic (optional) . . . . . . . . 38
1.8 Alternative notation (optional ) . . . . . . . . . . . . . . . . . . 40

2 The Logic of Atomic Sentences 41
2.1 Valid and sound arguments . . . . . . . . . . . . . . . . . . . . 41
2.2 Methods of proof . . . . . . . . . . . . . . . . . . . . . . . . . . 46
2.3 Formal proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
2.4 Constructing proofs in Fitch . . . . . . . . . . . . . . . . . . . . 58
2.5 Demonstrating nonconsequence . . . . . . . . . . . . . . . . . . 63
2.6 Alternative notation (optional ) . . . . . . . . . . . . . . . . . . 66

3 The Boolean Connectives 67
3.1 Negation symbol: ¬ . . . . . . . . . . . . . . . . . . . . . . . . . 68
3.2 Conjunction symbol: § . . . . . . . . . . . . . . . . . . . . . . . 71
3.3 Disjunction symbol: ∨ . . . . . . . . . . . . . . . . . . . . . . . 74
3.4 Remarks about the game . . . . . . . . . . . . . . . . . . . . . 77



v
vi / Contents


3.5 Ambiguity and parentheses . . . . . . . . . . . . . . . . . . . . 79
3.6 Equivalent ways of saying things . . . . . . . . . . . . . . . . . 82
3.7 Translation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84
3.8 Alternative notation (optional ) . . . . . . . . . . . . . . . . . . 89

4 The Logic of Boolean Connectives 93
4.1 Tautologies and logical truth . . . . . . . . . . . . . . . . . . . 94
4.2 Logical and tautological equivalence . . . . . . . . . . . . . . . 106
4.3 Logical and tautological consequence . . . . . . . . . . . . . . . 110
4.4 Tautological consequence in Fitch . . . . . . . . . . . . . . . . . 114
4.5 Pushing negation around (optional) . . . . . . . . . . . . . . . 117
4.6 Conjunctive and disjunctive normal forms (optional ) . . . . . . 121

5 Methods of Proof for Boolean Logic 127
5.1 Valid inference steps . . . . . . . . . . . . . . . . . . . . . . . . 128
5.2 Proof by cases . . . . . . . . . . . . . . . . . . . . . . . . . . . . 131
5.3 Indirect proof: proof by contradiction . . . . . . . . . . . . . . . 136
5.4 Arguments with inconsistent premises (optional ) . . . . . . . . 140

6 Formal Proofs and Boolean Logic 142
6.1 Conjunction rules . . . . . . . . . . . . . . . . . . . . . . . . . . 143
6.2 Disjunction rules . . . . . . . . . . . . . . . . . . . . . . . . . . 148
6.3 Negation rules . . . . . . . . . . . . . . . . . . . . . . . . . . . 154
6.4 The proper use of subproofs . . . . . . . . . . . . . . . . . . . . 163
6.5 Strategy and tactics . . . . . . . . . . . . . . . . . . . . . . . . 167
6.6 Proofs without premises (optional) . . . . . . . . . . . . . . . . 173

7 Conditionals 176
7.1 Material conditional symbol: ’ . . . . . . . . . . . . . . . . . . 178
7.2 Biconditional symbol: ” . . . . . . . . . . . . . . . . . . . . . . 181
7.3 Conversational implicature . . . . . . . . . . . . . . . . . . . . 187
7.4 Truth-functional completeness (optional ) . . . . . . . . . . . . . 190
7.5 Alternative notation (optional ) . . . . . . . . . . . . . . . . . . 196

8 The Logic of Conditionals 198
8.1 Informal methods of proof . . . . . . . . . . . . . . . . . . . . . 198
8.2 Formal rules of proof for ’ and ” . . . . . . . . . . . . . . . . 206
8.3 Soundness and completeness (optional) . . . . . . . . . . . . . . 214
8.4 Valid arguments: some review exercises . . . . . . . . . . . . . . 222




Contents
Contents / vii



II Quanti¬ers 225
9 Introduction to Quanti¬cation 227
9.1 Variables and atomic w¬s . . . . . . . . . . . . . . . . . . . . . 228
9.2 The quanti¬er symbols: ∀, ∃ . . . . . . . . . . . . . . . . . . . . 230
9.3 W¬s and sentences . . . . . . . . . . . . . . . . . . . . . . . . . 231
9.4 Semantics for the quanti¬ers . . . . . . . . . . . . . . . . . . . . 234
9.5 The four Aristotelian forms . . . . . . . . . . . . . . . . . . . . 239
9.6 Translating complex noun phrases . . . . . . . . . . . . . . . . 243
9.7 Quanti¬ers and function symbols (optional ) . . . . . . . . . . . 251
9.8 Alternative notation (optional ) . . . . . . . . . . . . . . . . . . 255

10 The Logic of Quanti¬ers 257
10.1 Tautologies and quanti¬cation . . . . . . . . . . . . . . . . . . . 257
10.2 First-order validity and consequence . . . . . . . . . . . . . . . 266
10.3 First-order equivalence and DeMorgan™s laws . . . . . . . . . . 275
10.4 Other quanti¬er equivalences (optional ) . . . . . . . . . . . . . 280
10.5 The axiomatic method (optional) . . . . . . . . . . . . . . . . . 283

11 Multiple Quanti¬ers 289
11.1 Multiple uses of a single quanti¬er . . . . . . . . . . . . . . . . 289
11.2 Mixed quanti¬ers . . . . . . . . . . . . . . . . . . . . . . . . . . 293
11.3 The step-by-step method of translation . . . . . . . . . . . . . . 298
11.4 Paraphrasing English . . . . . . . . . . . . . . . . . . . . . . . . 300
11.5 Ambiguity and context sensitivity . . . . . . . . . . . . . . . . 304
11.6 Translations using function symbols (optional ) . . . . . . . . . 308
11.7 Prenex form (optional ) . . . . . . . . . . . . . . . . . . . . . . . 311
11.8 Some extra translation problems . . . . . . . . . . . . . . . . . 315

12 Methods of Proof for Quanti¬ers 319
12.1 Valid quanti¬er steps . . . . . . . . . . . . . . . . . . . . . . . . 319
12.2 The method of existential instantiation . . . . . . . . . . . . . . 322
12.3 The method of general conditional proof . . . . . . . . . . . . . 323
12.4 Proofs involving mixed quanti¬ers . . . . . . . . . . . . . . . . 329
12.5 Axiomatizing shape (optional ) . . . . . . . . . . . . . . . . . . 338

13 Formal Proofs and Quanti¬ers 342
13.1 Universal quanti¬er rules . . . . . . . . . . . . . . . . . . . . . 342
13.2 Existential quanti¬er rules . . . . . . . . . . . . . . . . . . . . . 347
13.3 Strategy and tactics . . . . . . . . . . . . . . . . . . . . . . . . 352
13.4 Soundness and completeness (optional ) . . . . . . . . . . . . . . 361




Contents
viii / Contents


13.5 Some review exercises (optional ) . . . . . . . . . . . . . . . . . 361

14 More about Quanti¬cation (optional ) 364
14.1 Numerical quanti¬cation . . . . . . . . . . . . . . . . . . . . . . 366
14.2 Proving numerical claims . . . . . . . . . . . . . . . . . . . . . 374
14.3 The, both, and neither . . . . . . . . . . . . . . . . . . . . . . . 379
14.4 Adding other determiners to fol . . . . . . . . . . . . . . . . . 383
14.5 The logic of generalized quanti¬cation . . . . . . . . . . . . . . 389
14.6 Other expressive limitations of ¬rst-order logic . . . . . . . . . 397


III Applications and Metatheory 403
15 First-order Set Theory 405
15.1 Naive set theory . . . . . . . . . . . . . . . . . . . . . . . . . . 406
15.2 Singletons, the empty set, subsets . . . . . . . . . . . . . . . . . 412
15.3 Intersection and union . . . . . . . . . . . . . . . . . . . . . . . 415
15.4 Sets of sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 419
15.5 Modeling relations in set theory . . . . . . . . . . . . . . . . . . 422
15.6 Functions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 427
15.7 The powerset of a set (optional ) . . . . . . . . . . . . . . . . . 429
15.8 Russell™s Paradox (optional ) . . . . . . . . . . . . . . . . . . . . 432
15.9 Zermelo Frankel set theory zfc (optional ) . . . . . . . . . . . . 433

16 Mathematical Induction 442
16.1 Inductive de¬nitions and inductive proofs . . . . . . . . . . . . 443
16.2 Inductive de¬nitions in set theory . . . . . . . . . . . . . . . . . 451
16.3 Induction on the natural numbers . . . . . . . . . . . . . . . . . 453
16.4 Axiomatizing the natural numbers (optional ) . . . . . . . . . . 456
16.5 Proving programs correct (optional ) . . . . . . . . . . . . . . . 458

. 1
( 107 .)



>>