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

DOWNLOAD

REPORT


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[~],~