A negative modality, like knows(a) P, demands that all accessible worlds have P true. A positive modality, like eventually P, means at least one accessible world has P true. How does one know if a proposition is true at a world? Non-modal propositions can be checked normally. We can always look at what propositions are true in a given model, and look at what models validate a given axiom. So a model of a set of modal axioms is a collection of logical worlds and an accessibility relation between them. This notion of one world following the next can be wrapped up in a relation (called the accessibility relation), so that the statement eventually P to be true at world w exactly when P is true at a world related to w.
We model eventually P as P being true in at least one of the worlds that might eventually follow your current one. The axiom above describes a property of how those states are related to each other: that for any state (t, PRESSED, c), there is a state (t + k, b, HALTED) that you might later find yourself in. That is, if a world is a triple of time, button state, and computer state, then at state (t, b, c) there are some states (s, b', c') that we might later find ourselves in. But to understand that eventually statement we must be able to think about what will happen at future times. This proposition might true at some points in time and not others (“if the button were pressed right now, the computer will eventually halt”), so our possible worlds must include a timestamp of some sort.
Suppose we now want to reason instead about the behavior of this system over time, using the modal axiom: For example, the set is a model of that axiom. A model of this axioms is a set of such worlds where the implication above is true. So a world must contain a pair of button and computer state: (PRESSED, HALTED) is a world, as is (UNPRESSED, RUNNING). To decide whether this sentence is true or false, we'd need to know whether or not the button is pressed or not, and whether the computer is halted or now. To give you an example, let's go back this axiom for describing the behavior of a computer system: Generally, a world is all the information needed to definitively decide whether a proposition is true or false. Or, in the logic of knowledge, I use the knows(a) modality to describe all the worlds that a thinks might be the real one. For example, in the logic of time I described in my last post, if right now it is time t, I can use the eventually modality to describe all the worlds that might exist at later times. In fact, hypothetical reasoning is itself a modality, though that's for a later time. It also proved vital for applications such as the Brouwer–Heyting–Kolmogorov provability semantics for intuitionistic logic, for introducing justification into formal epistemology and tackling its logical omniscience problem, and for introducing self reference into combinatory logic and lambda-calculi.The fundamental insight of models for modal logic is that modal logic is for describing hypothetical worlds. This approach led to comprehensive provability semantics for a broad class of modal logics. Gödel's use of modal logic to describe provability, gave the first exact semantics of modality. There are two major ideas that dominate the landscape of modal logic application in mathematics: Gödel's provability semantics and Tarski's topological semantics.
Mathematics is one of modal logic's oldest application areas. Propositional modal logic offers a new paradigm of applying logical methods: instead of using the traditional languages with quantification to describe a structure, an appropriate quantifier-free language with additional logic operators that represent the phenomenon at hand, is used. Mathematics normally finds a proper language and level of abstraction for the study of its objects. This chapter presents a wide variety of mathematical techniques developed over decades of studying the intricate details of modal logic. Formal modal logic is mostly mathematical in its methods, regardless of area of application.
0 kommentar(er)
