Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A note on the theory of well orders

Emil Jeřábek

TL;DR

The paper studies the first-order theory of the class $\mathcal{WO}$ of well-ordered sets, and proves that its theory is exactly the transfinite induction axiom schema $\mathsf{TI}$ and is decidable. A short, non-quantifier-elimination argument inspired by the Lau-Len method shows the equivalence: $\mathcal{WO}\vDash\varphi$ iff $\alpha\vDash\varphi$ for all $\alpha<\omega^\omega$ iff $\mathsf{TI}\vdash\varphi$. The approach uses finite Ehrenfeucht–Fraïssé-type reasoning, Ramsey theory to obtain a canonical $\alpha<\omega^\omega$ describing intervals, and a uniform satisfiability lemma (Lemma sat) that reduces decidability to a CNF-like representation of linear orders. Decidability follows since $\mathsf{TI}$ is recursively axiomatizable and, via Lemma sat, the complement set is recursively enumerable, yielding an effective decision procedure; this provides a self-contained, accessible proof that aligns with Lau-Len's methods while connecting to the established Doner-Mostowski-Tarski results.

Abstract

We give a simple proof that the first-order theory of well orders is axiomatized by transfinite induction, and that it is decidable.

A note on the theory of well orders

TL;DR

The paper studies the first-order theory of the class of well-ordered sets, and proves that its theory is exactly the transfinite induction axiom schema and is decidable. A short, non-quantifier-elimination argument inspired by the Lau-Len method shows the equivalence: iff for all iff . The approach uses finite Ehrenfeucht–Fraïssé-type reasoning, Ramsey theory to obtain a canonical describing intervals, and a uniform satisfiability lemma (Lemma sat) that reduces decidability to a CNF-like representation of linear orders. Decidability follows since is recursively axiomatizable and, via Lemma sat, the complement set is recursively enumerable, yielding an effective decision procedure; this provides a self-contained, accessible proof that aligns with Lau-Len's methods while connecting to the established Doner-Mostowski-Tarski results.

Abstract

We give a simple proof that the first-order theory of well orders is axiomatized by transfinite induction, and that it is decidable.
Paper Structure (1 section, 4 theorems, 3 equations)

This paper contains 1 section, 4 theorems, 3 equations.

Table of Contents

  1. Acknowledgements.

Key Result

Lemma 1

If $L_i\equiv_kL'_i$ for each $i\in I$, then $\sum_{i\in I}L_i\equiv_k\sum_{i\in I}L'_i$. If $I\equiv_kI'$, then $L\cdot I\equiv_kL\cdot I'$.

Theorems & Definitions (6)

  • Lemma 1
  • Theorem 2
  • Claim 2.1
  • Claim 2.2
  • Lemma 3
  • Theorem 4