Hi. I love this proof generator, and feel almost ashamed to ask for a feature. Also, not sure what barriers there might be to it in terms of coding. But I wonder about adding a variable domain semantics as an option for the modal logic part.

What I've done so far, if I want to use it for metaphysics and want to assume an actualist metaphysics, is to just use "E" as a predicate for "actually exists" and then added in conjuncts like "Ea" where appropriate.

I wonder whether either (A) a variable domain semantics could be run in the background, or else (B) if that would be difficult to code or take up a lot of computing resources, if there's any algorithmic way to add in conjuncts that essentially say "x actually exists" in the background so as to get an equivalent result out of a constant domain semantics. I confess I haven't really thought that through, but thought I'd at least raise the question for discussion.