We summarize the details of how we
choose to model WaterWorld boards
in propositional logic:
exactly what propositions we make up,
and the formal domain axioms which capture the game's rules.
The board is fixed at 6×4,
named AA,…,ZZ (with I and O omitted).
There are a myriad of propositions for WaterWorld,
which can be grouped:
-
Whether or not a location contains a pirate:
A-unsafeA-unsafe, B-unsafeB-unsafe, …, Z-unsafeZ-unsafe.
-
Whether or not a location contains no pirate:
A-safeA-safe, B-safeB-safe, …, Z-safeZ-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-0A-has-0, A-has-1A-has-1, A-has-2A-has-2,
B-has-0B-has-0, B-has-1B-has-1, B-has-2B-has-2,
…,
H-has-0H-has-0, H-has-1H-has-1, H-has-2H-has-2, H-has-3H-has-3,
…,
Z-has-0Z-has-0, Z-has-1Z-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-1B-has-1 is true, then B-has-0B-has-0 and B-has-2B-has-2 are both false.
There is no proposition A-has-3A-has-3 — since location AA
has only two neighbors.
Similarly, there is no proposition B-has-3B-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-2A-has-2 as a premise
only when AA has been exposed and shows a 2.
Axioms asserting that the neighbor counts are correct:
-
Count of 0:
- "A0":
(A-has-0→(B-safe∧G-safe))(A-has-0→(B-safe∧G-safe))
- …
- "H0":
(H-has-0→(G-safe∧J-safe∧P-safe))(H-has-0→(G-safe∧J-safe∧P-safe))
- …
- "Z0":
(Z-has-0→(Y-safe))(Z-has-0→(Y-safe))
-
Count of 1:
- "A1":
(A-has-1→((B-safe∧G-unsafe)∨(B-unsafe∧G-safe)))(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)))(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))(Z-has-1→(Y-unsafe))
-
Count of 2:
- "A2":
(A-has-2→(B-unsafe∧G-unsafe))(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)))(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))(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 neighbor count propositions; are consistent:
- (A-has-0∨A-has-1)(A-has-0∨A-has-1)
- (A-has-0→¬A-has-1)(A-has-0→¬A-has-1)
- (A-has-1→¬A-has-0)(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-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-1→(¬B-has-0∧¬B-has-2))
- (B-has-2→(¬B-has-0∧¬B-has-1))(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-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-1→(¬H-has-0∧¬H-has-2∧¬H-has-3))
- (H-has-2→(¬H-has-0∧¬H-has-1∧¬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))(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),
- (¬A-safe→A-unsafe)(¬A-safe→A-unsafe),
- …
- (Z-safe→¬Z-unsafe)(Z-safe→¬Z-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 a bit redundant to have both
A-safeA-safe and A-unsafeA-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.
We'll see later how
relations and
quantifiers
help us model the game of WaterWorld more concisely.