Decidable Theories II The Monadic Second Order Theory of All Countab
- PDF / 11,787,491 Bytes
- 223 Pages / 483 x 720 pts Page_size
- 82 Downloads / 148 Views
328 Decidable Theories !! Edited by G. H. MLiller and D. Siefkes i
J. Richard Bechi Purdue University, Lafayette, IN/USA
Dirk Siefkes Mathematisches Institut der Universit~t Heidelberg, Heidelberg/BRD
The Monadic Second Order Theory of All Countable Ordinals
Springer-Verlag Berlin.Heidelberg • New York 19 73
A M S Subject Classifications (1970): 02-02, 02F 10, 0 2 G 0 5 , 0 2 G 10, 68-02, 6 8 A 25, 0 2 G 20, 02 H I0, 02K20
I S B N 3-540-06345-5 S p r i n g e r - V e r l a g B e r l i n • H e i d e l b e r g • N e w Y o r k I S B N 0-387-06345-5 S p r i n g e r - V e r l a g N e w Y o r k • H e i d e l b e r g • B e r l i n
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 Berlin • Heidelberg 197£ Library of Congress Catalog Card Number 73-82358. Printed in Germany. Offsetdruck: Julius Beltz, HemsbachlBergstr.
Table of Contents
J. Richard BGchi: The Monadic Second q.
iOrder
Theory of
~q
Monadic second order theories; the prenex form lemma
4
The language,
z~
standard models, monadic second order
theories
9
Prenex forms, sup conditions
2.
Standard axiom systems, relativization
17
A method for eliminating set-quantifiers
2q
Decision method for monadic second order theories,
2q
transition system, finite automata Decidability results for monadic second order
27
theories Open problems
.
37
The working of the method in the ,case of
Go
40
Item q : Transition systems, runs
z~O
Item 2 : The complementation lemma, the subset
z~2
construction in the finite case, merging,
automata
normal form Item 3 : The decision-method Item 2': The subset-construction at
54 ~,
deter-
56
ministic automata normal form 4.
The subset-construction extender up to
~q
Deterministic automata normal form for countable ordinals
7q
71
IV
The input-free case:
~q - spectrum, associated
86
operators, expansion, head, tail, character, absorption automata, the Tarski-Lindenbaum algebra, equivalent countable ordinals Decision method for 5.
NT[co]
and
MT[~],~
Data Loading...