Please see the image below which represents an algebraic definition of the Dolev Yao Closure. From reading around, it appears this is BAN logic and that the lines mean "If you believe the above statement is true, then you must believe the lower statement is also true."
Is this accurate and why do the statements appear in the order they do?
The order of the statements is not important. It may help to mentally translate $\mathcal{DY}(M)$ as “information that you should believe that an adversary can trivially compute starting from an initial set of known data $M$”. The rules should then feel intuitively true.
The axiomatic (first) rule can be thought of as “the adversary can trivially compute the initial set of data”.
The algebraic (second) rule can be thought of as “the adversary can trivially compute an algebraic expression consisting of values that they know”.
The composition (third) rule can be thought of as “the adversary can compute any function within the logical model of a set of values that they know”.
The projection (fourth) rule can be thought of as “if the adversary knows a pair of data values, then they can compute the individual data values”.
The symmetric decryption (fifth) rule can be thought of as “if the adversary knows a symmetrically encrypted ciphertext and the key used to encrypt it, then they can compute the corresponding plaintext”.
The asymmetric decryption (sixth) rule can be thought of as “if the adversary knows a public key encrypted ciphertext and the corresponding private key, then they can compute the corresponding plaintext”.
The open signature (seventh) rule can be thought of as “if the adversary knows the signature of piece of message digest, then they can compute the message digest”.
The Dolaev-Yao closure of an initial set of data $M$ should then be thought of as the set of data that an adversary can easily compute based on these rules.
