An axiom system for the weak monadic second order theory of two successors.

Autor: Siefkes, Dirk
Zdroj: Israel Journal of Mathematics; May1978, Vol. 30 Issue 3, p264-284, 21p
Abstrakt: A compelte axiom system for the weak monadic second order theory of two successor functions, W2S, is presented. The axiom system consists, roughly, of the generalized Peano axioms and of an inductive definition of the finite sets. For the proof, methods of J. R. Buchi and J. Doner are used to obtain a new decision procedure for W2S, whose proofs are easily formalized. Different finiteness axioms are discussed. [ABSTRACT FROM AUTHOR]
Databáze: Complementary Index
Externí odkaz: