Monadic $\Pi^1_1$-theories of $\Pi_1^1$}-properties.
Kees Doets · Notre Dame Journal of Formal Logic · 1989
Axiomatizations are provided for the monadic universal secondorder theories of: scattered orderings, well-orderings, complete orderings, the ordering of the natural numbers, of the reals, and of well-founded trees.Proofs employ the Ehrenfeucht-Fraϊsse-game. SummaryFor some Πj-statements vRφ{R), results of the following type are proved: Suppose that a monadic Π} -sentence VX X ... y/X k φ(Xι 9 ... ,X k ) is a consequence of VRφ(R), then the first-order sentence ψ(Uι,. .., U k ) is already a consequence of the first-order schema corresponding to vRφ(R) 9 which requires φ(R) only for R which are (parametrically) first-order definable in the language of ψ(U u ..., U k ).Cases considered here are: scattered orderings, well-orderings, complete orderings, models of order type ω, of order type λ, and well-founded trees.The method of proof uses the Ehrenfeucht-Fraϊsse-game.*I wish to thank Johan van Benthem for his questions (to which 3.1, 4.6, and 4.9 below form the answers) and his stimulating interest in the topic of this paper.