The reflexivity, antisymmetry, transitivity and totality axioms for a <total order> are universal with <quantifier-free formula> matrices, and hence inductive with an empty existential block. Add $\forall x\,\exists y\,(y<x)$ and $\forall x\,\exists z\,(x<z)$, with strict inequalities expressed using $\le$ and inequality. These exclude least and greatest elements. \b[This theory is inductive.]

Solution

Past exam of the mathematics course of the University of Cambridge / 2006 / ii / Paper 3 / 16H / a / Solution

 Solution (source code)