We summarize the details of how we choose to model WaterWorld boards in first-order logic: exactly what relations we make up, and the formal domain axioms which capture the game's rules.
This will follow almost exactly the same pattern as our WaterWorld model in Propositional axioms for WaterWorld. However, we will take advantage of the additional flexibility provided by first-order logic.
Rather than modeling only the default 6×4 WaterWorld board;, we will be able to model any board representable by our relations. This will allow boards of any size and configuration, with one major constraint each location can have at most three neighboring pirates.