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 is dependent on all the sailors in all the chain of commands 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: The superior of a command link commands the inferior of the link.
- Axiom: The superior and inferior of a command link are not the same (nobody commands themself).
- Axiom: Some (but not all) sailors are commanded by another sailor.
- Axiom: Some (but not all) sailors command another sailor.
- Axiom: A seaman commands no other sailor.
- Theorem: A seaman is never the superior of a command link.
- Theorem: Every seaman is commanded by some other sailor.
- Theorem: If a sailor commands another sailor, then the first sailor is not a seaman.
- Axiom: A sailor is an admiral iff no other sailor commands 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: Some admirals command some other sailors.
- Theorem: If a sailor is not a admiral then there is another sailor who commands 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 spirals).
- 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 command 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.
- Ensure that the axioms are consistent using an ATP system.
- Prove the theorems using an ATP system.
Answers