Call two axioms equivalent if they imply the same set of theorems. I am interested in decidability of so defined equivalence. In this generality the problem is obviously undecidable since it can be used to decide Entscheidungsproblem. So I am interested in cases where Entscheidungsproblem is decidable, particularly in case of monadic axioms (i.e. axioms containing only monadic functional and predicate symbols).


Any information about this would be appreciated.


Thank you for your time,
Levon



Equivalence of monadic axioms
The comment showed that decidability of axiom equivalence is implied by decidability of pure logic. (I.e. to decide if $\Theta$ and $\Theta'$ are equivalent, it is equivalent to decide if $\vdash \Theta \leftrightarrow \Theta'$. Conversely, if one can decide axiom equivalence, then one can decide pure logic. Namely, $\vdash \Theta$ iff the axiom $\Theta$ is equivalent to $\top$.


