 Proofs of SDL-ish formulas are then just K-proofs of the corresponding modal formulae involving  “\(d\)”.[35]  It is well-known that all theorems of SDL are derivable in Kd and conversely, that if some formula in the language of SDL is not a theorem of SDL, then its translation following the Kangerian reduction is also not a theorem of  Kd.[36]  In addition to containing all theorems of SDL, we note a few theorems that are specific to Kd because of the non-overlapping syntactic ingredients, \(d, \Box\), and \(\Diamond\):