Expressing Second-order Sentences in Intuitionistic Dependence Logic

TL;DR

This paper proves that intuitionistic dependence logic is expressively equivalent to second-order logic at the sentence level, establishing a bidirectional translation between them.

Contribution

It demonstrates that every intuitionistic dependence logic sentence can be translated into second-order logic and vice versa, confirming their equivalence.

Findings

Equivalence of intuitionistic dependence logic and second-order logic for sentences

Bidirectional translation between the two logics

Strengthens understanding of the expressive power of intuitionistic dependence logic

Abstract

Intuitionistic dependence logic was introduced by Abramsky and Vaananen (2009) as a variant of dependence logic under a general construction of Hodges' (trump) team semantics. It was proven that there is a translation from intuitionistic dependence logic sentences into second order logic sentences. In this paper, we prove that the other direction is also true, therefore intuitionistic dependence logic is equivalent to second order logic on the level of sentences.