 The problem of deciding whether a dependence logic sentence is valid (that is, true in all models) is non-arithmetical, and in fact complete with respect to the \(\Pi_2\) class of the Levy hierarchy. Nonetheless, the proof theory of dependence logic has been studied. In particular, in (Kontinen &amp; Väänänen 2013), a sound and complete proof system has been developed for the problem of finding the first order consequences of a dependence logic theory.