TAILIEUCHUNG - Language Proof And Logic

What do the ¯elds of astronomy, economics, ¯nance, law, mathematics, med- icine, physics, and sociology have in common? Not much in the way of sub- ject matter, that's for sure. And not all that much in the way of methodology. What they do have in common, with each other and with many other ¯elds, is their dependence on a certain standard of rationality. In each of these ¯elds, it is assumed that the participants can di®erentiate between rational argu- mentation based on assumed principles or evidence, and wild speculation or nonsequiturs, claims that in no way follow from the assumptions. In other words, these ¯elds all presuppose an. | LANGUAGE PROOF AND LOGIC JON BARWISE JOHN ETCHEMENDY In collaboration with Gerard Allwein Dave Barker-Plummer Albert Liu CSLI Publications Center for the Study of Language and Information Stanford California SEVEN BRIDGES PRESS NEW YORK LONDON Copyright 1999 CSLI Publications Center for the Study of Language and Information Leland Stanford Junior University 03 02 01 00 99 5 4 3 2 1 Library of Congress Cataloging-in-Publication Data Barwise Jon. Language proof and logic Jon Barwise 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 1956III. 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 refining the text. Without their intelligence dedication and hard work LPL would neither exist nor have most of its other good properties. In addition to the five of us many people have contributed directly and indirectly 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 outstanding contributions to the earlier programs provided the foundation of the new software. Second we thank several people who have helped with the development 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

• Ôn thi ĐH-CĐ
• Predicate symbols
• Individual constants
• Atomic sentences
• Alternative notation
• Methods of proof
• General first order languages