 Rather than extending first order logic with dependence atoms \(\eqord(\vec x, y)\), independence logic (Grädel &amp; Väänänen 2013) extends it with independence atoms \(\vec x \mathop{\bot_{\vec z}} \vec y\), whose intended interpretation is “for any possible choice of \(\vec z\), the possible values of \(\vec x\) and \(\vec y\) are independent”—in other words, given any fixed choice of \(\vec z\), knowing the value taken by \(\vec x\) would not convey any information about the value taken by \(\vec y\). This is a notion of significant conceptual importance: for example, one may want to express that—if one does not know the encryption key—seeing the encrypted version of a message carries no information about the corresponding clear-text version. If \(x\) represents the encrypted message and \(y\) represents the plain-text one, then this corresponds to the condition \(x \mathop{\bot} y\), where \(\vec z\) in this case is empty. Similarly, if \(k\) represents the key then \(x \mathop{\bot} k\) represents the claim that the key cannot be inferred from the encrypted message; and the conjunction dependence atom \(\eqord(k, x, y)\) (which, as we will soon see, can be represented in independence logic) represents the claim that the plain-text message can be decoded given the encrypted message and the key.