You are here

The domain axioms

17 June, 2015 - 09:57
Available under Creative Commons-ShareAlike 4.0 International License. Download for free at

Many of our axioms correspond directly, albeit much more succinctly, with those (Section 6.5.2: The domain axioms) of the propositional model. In addition, we have axioms that specify that our neighbor and equality relations are self-consistent.

Axioms asserting that the neighbor relation is anti-reflexive and symmetric:

  • x :(¬nhbr (x, x))
  • x :(∀y : (nhbr (x, y) ⇒ nhbr (y, x)))

Axioms asserting that "=" truly is an equality relation, i.e., it is reflexive, symmetric, and transitive.

  • x :(x = x)
  • x :(∀y : ((x = y) ⇒ (y = x)))
  • x :(∀y :(∀z : ((x = y) ∧ (y = z) ⇒ (x = z))))

Axioms asserting that the neighbor counts are correct. Each of these is of the form "if location x has n neighboring pirates, then there are n distinct unsafe neighbors of x, and any other distinct neighbor x is safe." We use the equality relation to specify the distinctness of each neighbor.

  • \\ \forall x:(has0(x)\Rightarrow \forall y:(nhbr(x,y)\Rightarrow safe(y)))
  • \forall x:(has1(x)\Rightarrow \exists a:(nhbr(x,a)\wedge \dashv safe(a)\wedge \forall y:(nhbr(x,y)\wedge(a\neq y)\Rightarrow safe(y) )))
  • \forall x : (has2 (x) \Rightarrow \exists a :(\exists b : (nhbr (x, a) \wedge nhbr (x, b) \wedge (a = b) \wedge ¬safe (a) \wedge \dashv safe (b) \wedge \forall y : (nhbr (x, y) \wedge (a\neq y)\Rightarrow unsafe(y))))
  • \forall x : (has3 (x) \Rightarrow \exists a :(\exists b :(\exists c : (nhbr (x, a) \wedge nhbr (x, b) \wedge nhbr (x, c) \wedge (a = b) \wedge (a = c) \wedge (b = c) \wedge \dashv safe (a)

In addition, we want the implications to go the opposite way. Otherwise, each of has0, has1, has2, and has3 could always be false, while still satisfying the above! For brevity, we elide the details in the following list:

  • x :(∀y : (nhbr (x, y) ⇒ safe (y)) ⇒ has0 (x))
  • x :(... ⇒ has1 (x))
  • x :(... ⇒ has2 (x))
  • x :(... ⇒ has3 (x))

Axioms asserting that the neighbor counts are consistent. While redundant, including axioms like the following can be convenient.

  • x : (has0 (x) ¬ (has1 (x)has2 (x)has3 (x)))
  • x : (has1 (x) ¬ (has0 (x)has2 (x)has3 (x)))
  • x : (has2 (x) ¬ (has0 (x)has1 (x)has3 (x)))
  • x : (has3 (x) ¬ (has0 (x)has1 (x)has2 (x)))

Note that this set of axioms is not quite complete, as explored in an exercise (Exercise 4.4.22).