Nonfinite axiomatizability of torsion-free abelian groups (source code)

= Nonfinite axiomatizability of torsion-free abelian groups

The class of <torsion-free group>[torsion-free] <abelian groups> has an infinite first-order axiomatization but no <finite axiomatizability>[finite axiomatization]. Add $\forall x(nx=0\to x=0)$ for every positive <integer> $n$ to the <abelian group> <axioms>. If an equivalent finite theory existed, <compactness theorem>[compactness] would make it follow from finitely many of these conditions. A <cyclic group> of <prime number>[prime] order larger than the finitely many integers mentioned satisfies those conditions but has <torsion subgroup>[torsion], a contradiction.