The Naval Chain of Command
A naval chain of command describes the relationships between sailors of different ranks, showing
how commands transfer from one sailor to another.
If a sailor of higher rank commands a sailor of inferior rank, then there is a
command link from the superior of the command link to the inferior of
the command link.
Admirals are those sailors who are not commanded by any other sailor.
Seamen are those sailors who do not command any other sailor.
A sequence of command links from a sailor to a sailor to a sailor, etc, forms a chain of
command that starts at the superior of the first link of the sequence and ends at the
inferior of the last link of the sequence.
A chain of command is total if it starts at an admiral.
An admiral depends on all the sailors in all the chains of command that lead from
the admiral.
Chains of command can be encoded in typed first order logic, and various theorems can then be
proved.
(Hint: The words in italics are types or functions or predicates in the encoding.)
Here the axioms of the system are given in English, interspersed with theorems that can be proved
from the preceding axioms.
- Axiom: A sailor gives a command to another sailor iff there is a command link such that the
first sailor is the superior of the command link and the second sailor is the inferior of the
command link.
- Axiom: The superior and inferior of a command link are not the same (nobody gives commands
to themself).
- Axiom: Some (but not all) sailors give commands to some other sailors.
- Axiom: Some (but not all) sailors are given commands by some other sailors.
- Axiom: A seaman does not give commands to other sailors.
- Axiom: Every seaman is given commands by some other sailors.
- Theorem: A seaman is never the superior of a command link.
- Theorem: Every seaman is given commands by some other sailor.
- Theorem: If a sailor gives commands to some other sailors, then the first sailor is not
a seaman.
- Axiom: A sailor is an admiral iff no other sailor gives commands to him/her.
- Theorem: If someone is an admiral then there is no command link such that the admiral
is the inferior of the command link.
- Theorem: If an admiral gives a command to some other sailor, then the other sailor is the
inferior of a command link from the admiral to the sailor.
- Theorem: If a sailor is not a admiral then there is another sailor who gives commands to
him/her.
- Axiom: For every chain of command, the start of the chain is the superior of some command
link, and (only) one of the following holds:
(i) the inferior of the command link is the end of the chain of command,
xor (ii) there is a shorter chain of command (shorter by one command link) from the inferior
of the command link to the end of the whole chain of command.
- Axiom: There is no chain of command from a sailor back to themself (no command loops).
- Axiom: A total chain of command starts at an admiral.
- Axiom: Every sailor is in some total chain of command, i.e.,
(i) the sailor is the admiral start of the total chain of command, or
(ii) the sailor is at the end of the total chain of command, or
(iii) there is a non-total chain of command from an admiral at the start of the total chain
of command to the sailor, and another non-total chain of command from the sailor to
the sailor at the end of the total chain of command.
- Theorem: The sailor at the end of a total chain of command does not give commands to the
admiral at the start of the chain of command.
- Theorem: If a sailor is a seaman, then there is a total chain of command from an admiral
to that seaman.
- Axiom: Given two sailors, the first depends on the second iff there is a chain of command
from the first to the second.
- Theorem: If a sailor is not an admiral then there is an admiral that depends on the sailor.
- Theorem: An admiral depends on all sailors (except him/herself) in all total chains of
command that start at the admiral.
You must ...
- Formulate the types, axioms, and theorems in TPTP TFF syntax.
- Check the syntax and types of the formulae.
- Ensure that the axioms are consistent using an ATP system.
- Prove the theorems using an ATP system.
Answers