Propositions There are a myriad of propositions for WaterWorld, which can be grouped: Whether or not a location contains a pirate: A-unsafe, B-unsafe, …, Z-unsafe. Whether or not a location contains no pirate: A-safe, B-safe, …, Z-safe. Yes, using the intended interpretation, these are redundant with the previous ones. Some domain axioms below will formalize this. Propositions indicating the number of neighboring pirates, to a location: A-has-0, A-has-1, A-has-2, B-has-0, B-has-1, B-has-2, …, H-has-0, H-has-1, H-has-2, H-has-3, …, Z-has-0, Z-has-1. These are all true/false propositions; — there are no explicit numbers in the logic. A domain axiom below will assert that whenever (say) B-has-1 is true, then B-has-0 and B-has-2 are both false. There is no proposition A-has-3 — since location A has only two neighbors. Similarly, there is no proposition B-has-3. We could have chosen to include those, but under the intended interpretation they'd always be false. These propositions describe the state of the underlying board — the model — and not our particular view of it. Our particular view will be reflected in which formulas we'll accept as premises. So we'll accept A-has-2 as a premise only when A has been exposed and shows a 2.

The domain axioms Axioms asserting that the neighbor counts are correct: Count of 0: “A0”: A-has-0 B-safe G-safe … “H0”: H-has-0 G-safe J-safe P-safe … “Z0”: Z-has-0 Y-safe Count of 1: “A1”: A-has-1 B-safe G-unsafe B-unsafe G-safe … “H1”: H-has-1 G-safe J-safe P-unsafe G-safe J-unsafe P-safe G-unsafe J-safe P-safe … “Z1”: Z-has-1 Y-unsafe Count of 2: “A2”: A-has-2 B-unsafe G-unsafe … “H2”: H-has-2 G-safe J-unsafe P-unsafe G-unsafe J-safe P-unsafe G-unsafe J-unsafe P-safe … There aren't any such axioms for locations with only one neighbor. Count of 3: “H3”: H-has-3 G-unsafe J-unsafe P-unsafe … There aren't any such axioms for locations with only one or two neighbors. Axioms asserting that the propositions for counting neighbors are consistent: A-has-0 A-has-1 A-has-0 A-has-1 A-has-1 A-has-0 B-has-0 B-has-1 B-has-2 B-has-0 B-has-1 B-has-2 B-has-1 B-has-0 B-has-2 B-has-2 B-has-0 B-has-1 … H-has-0 H-has-1 H-has-2 H-has-3 H-has-0 H-has-1 H-has-2 H-has-3 H-has-1 H-has-0 H-has-2 H-has-3 H-has-2 H-has-0 H-has-1 H-has-3 H-has-3 H-has-0 H-has-1 H-has-2 … Axioms asserting that the safety propositions are consistent: A-safe A-unsafe, A-safe A-unsafe, … Z-safe Z-unsafe, Z-safe Z-unsafe. This set of axioms is not quite complete, as explored in an exercise. As mentioned, it is redundant to have both A-safe and A-unsafe as propositions. Furthermore, having both allows us to express inconsistent states (ones that would contradict the safety axioms). If implementing this in a program, you might use both as variables, but have a safety-check function to make sure that a given board representation is consistent. Even better, you could implement WaterWorld so that these propositions wouldn't be variables, but instead be calls to a lookup (accessor) functions. These would examine the same internal state, to eliminate the chance of inconsistent data. Using only true/false propositions; without recourse to numbers makes these domain axioms unwieldy. Later, we'll see how relations and quantifiers help us model the game of WaterWorld more concisely.