Set-theoretic decidability results for modal theorem proving