I understand that when folks say “modal logic” in this context, they’re generally referring to model logics that implicitly quantify over poorly-defined spaces. However, that’s not what all modal logics are like, and so I hate to see them maligned with a broad brush.
Consider, say, dynamic logic), which I actually use as a tool in my research on program analysis. When my set of “actions” are statements in a well-defined programming language, I can mechanically translate any dynamic logic statement into a non-modal, first-order statement. I almost never do this, because the modal viewpoint is usually clearer and closer to the way we actually think about programs.
Equivalently: you can use whatever logical operators you like, if you can define the operator’s meaning without reference to the operator. It can help you say what you’re trying to say, rather than spending all of your time with low-level details. It’s like a higher-level programming language, but with math.
I understand that when folks say “modal logic” in this context, they’re generally referring to model logics that implicitly quantify over poorly-defined spaces. However, that’s not what all modal logics are like...
Consider my eyes opened.
Equivalently: you can use whatever logical operators you like, if you can define the operator’s meaning without reference to the operator.
This is my problem with the modal logics I have encountered—bad or unclear definitions of the modal operators.
I understand that when folks say “modal logic” in this context, they’re generally referring to model logics that implicitly quantify over poorly-defined spaces. However, that’s not what all modal logics are like, and so I hate to see them maligned with a broad brush.
Consider, say, dynamic logic), which I actually use as a tool in my research on program analysis. When my set of “actions” are statements in a well-defined programming language, I can mechanically translate any dynamic logic statement into a non-modal, first-order statement. I almost never do this, because the modal viewpoint is usually clearer and closer to the way we actually think about programs.
Equivalently: you can use whatever logical operators you like, if you can define the operator’s meaning without reference to the operator. It can help you say what you’re trying to say, rather than spending all of your time with low-level details. It’s like a higher-level programming language, but with math.
Consider my eyes opened.
This is my problem with the modal logics I have encountered—bad or unclear definitions of the modal operators.