If a celestial body in the solar system has cleared its orbit of other debris and has a nearly spherical shape due to its own gravity, then it is a planet.
∀x (CelestialBody(x) ∧ In(x, solarSystem) ∧ (∃y (OrbitOf(y, x) ∧ Clear(x, y) ∧ DebrisFree(y))) ∧ NearlySphericalShape(x, gravity) → Planet(x))