Feature Request: Variable Domain Semantics

[beaubranson]

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.

[wo]

Thanks for the friendly words.

I haven't given much thought to supporting variable domains, although I agree it could be useful. One problem is that this opens up a number of further choice points: if we don't want the CBF to be valid, we need to revise the underlying quantificational logic into some kind of free logic (either a positive or a negative or a nonvalent version -- there are good reasons for all three options).

My hope was that I don't need to get into this because one can simulate variable domains with constant domains, in the way you suggest.

I'm not sure what the algorithmic method is you are suggesting. Is the idea that there could be a button or something that adds 'Et' for every term t and that adds restrictions into all quantifiers, turning (Ax)Fx into (Ax)(Ex -> Fx) etc.?