math.LO — Logic
A counterexample to Vaught's Conjecture for
We construct a sentence of having exactly many countable models up to isomorphism, but no perfect set of non-isomorphic models. This disproves Vaught's conjecture for infinitary logic. The construction follows a framework devised by Robin Knight, and the proof has been formally verified in Lean.
Primarily human-written textHuman understanding: all partsKnight systemsVaught’s conjectureinfinitary logicnumber of models