Decidable Theories I
- PDF / 8,619,288 Bytes
- 142 Pages / 504 x 720 pts Page_size
- 35 Downloads / 189 Views
120
Decidable Theories I Edited by Gert H. MUlier, Heidelberg
Dirk Siefkes Mathematisches Institut der Universitat, Heidelberg
Buehl's Monadic Second Order Successor Arithmetic
Springer-Verlag Berlin· Heidelberg· New York 1970
Lecture Notes in Mathematics A collection of informal reports and seminars Edited by A. Dold, Heidelberg and B. Eckmann, ZOrich Series: Mathematisches Institut der Universitat Heidelberg Adviser: K. Krickeberg
120
Decidable Theories I Edited by Gert H. MUlier, Heidelberg
Dirk Siefkes Mathematisches Institut der Universitat, Heidelberg
Buehl's Monadic Second Order Successor Arithmetic
Springer-Verlag Berlin· Heidelberg· New York 1970
This work is subject to copyright. All rights are reserved, whether the whole or part of the material is concerned, specifically those of translation, reprinting, re-use of illustrations, broadcasting, reproduction by photocopying machine or similar means, and storage in data banks. Under §54 of the German Copyright Law where copies are made for other than private use, a fee is payable to the publisher, the amount of the fee to be determined by' agreement with the publisher. @ by Springer-Verlag Betlin . Heidelberg 1970. Library of Congress Catalog Card Number 70-111900. Printed in Germany.
TItle No.
To Marie Luise
Editor's Preface For several years I conducted a Seminar on decision procedures of various mathematical theories at the Mathematical Institute of the University of Heidelberg, some of the time jointly with Professor O. Herrmann. It is planned that I should continue this seminar with Dr.D.Siefkes. The results will be published in a subseries of ''Lecture Notes in Hathematics", to be called "Decidable Theories". The following aspects were, and will be, decisive both for the seminar and the Lecture Notes arising out of it. (i) The decidable theory in question and the decision procedure are set up in purely syntactical terms, hence not referring, for instance, to the true sentences of a preferred model. The transformation steps which in the simplest case lead to an equivalence with the propositional constants T (true) or F (raIse) are proved within the theory in question, of course, using syntactical means. (ii) A presentation of a decision procedure in the sense of (i), provides a set of operational devices which, if applied to a sentence, leads to its decision. From such devices certain syntactical_parameters of a sentence can be exhibited, and in these terms an estimation of the compleXity of the decision procedure can be made. Obviously, most presentations of decision procedures in the literature are given so that the decidability is proved in the simplest mathematical way. Hence it is not surprising that a presentation aiming at practical applications results in some remarkable simplifications of the decision procedure. A decision procedure usually is: 1) the reduction of an arbitrary sentence to a normal form (using the axioms of the theory) and 2) the reduction of a given sentence in normal form to T or F, as usual. Relative to
Data Loading...
