Modal Expansion Of Basic Propositional Logic

Basic propositional logic is a non-classical logic which is different from classical propositional logic and intuitionistic propositional logic. Compared to the classical propositional logic, basic propositional logic has a1which means always false, and the definitions of negation and implication are different from classical propositional logic. The truth-value of an implication depended on a specific transitive relation. Negation is no longer a truth-value transform as in classical propositional logic, the negation of a proposition is defined as the proposition implies⊥.Added to basic propositional logic the axiom p∧(p→q)→q, it can be the logical expansion of intuitionistic propositional logic; added to this intuitionistic propositional logic the axiom p∨-p,it can be the logical expansion of classical propositional logic. As classical propositional logic and intuitionistic propositional logic, basic propositional logic also has modal expansion, which can be used for the studies of necessarily, possibly and its related concepts. These are basically the same with the intuitionistic propositional logic. The difference between these two logics is the definition of implication, in basic propositional logic the specific relationship contains correspondence is a transitive relation, while in intuitionistic propositional logic the specific relationship contains correspondence is a reflexive and transitive relation. The differences between basic propositional logic and intuitionistic propositional logic is also due to the relation is reflexive or not. Because the relationship among the basic proposition logic, classical proposition logic and intuitionistic propositional, one can define the modal extension of basic proposition logic, learning from the classical modal logic and intuitionistic modal logic.Not as in classical modal logic, the operators of necessarily and possibly have no duality in the modal extension of basic proposition logic. So we should define the operators of necessarily and possibly separately. We need a new relation for defining the necessarily operator. But if we only use this relation to define the necessarily operator, we can find some formulas which contain necessarily operator are not valued with monotonicity, which is actually a property of basic proposition logic. In order to solve this problem I redefine the necessarily operator by the relation of the implication and the relation of the modality. After doing these I get an extension of basic proposition logic which has two axioms and one transformation rule contain necessarily operator. We also need a new relation for defining the possibly operator, but it has the same problem as the definition of necessarily operator. In order to solve this problem I add a requirement between the relation of the implication and the relation of the modality. After doing these I get an extension of basic proposition logic which has two axioms and one transformation rule contain possibly operator. Do all of the work above, I get the extension of basic proposition logic which has two axioms and one transformation rule contain necessarily operator, and has two axioms and one transformation rule contain possibly operator, which called MPL.There are some important differences between MPL and intuitionistic modal logic system. Ⅰ choice a most famous intuitionistic modal logic system which was constructed by Fischer Servi for compare with MPL system. Then I find that three axioms in Fischer Servi’s system are not valid in MPL system. Besides, consider with model theory I find some properties and theorems of model and frame which in classical modal logic, basic propositional logic and intuitionistic modal logic are also hold in MPL, if someone change the part of modal logic into special form which apply to MPL.Consider with those three axioms except axiom K contain both necessarily operator and possibly operator, in this paper I try to define necessarily operator and possibly operator by separating the relation of modality. This method is relevant to algebra. Using this method one can get a modal extension of basic proposition logic which contains both necessarily operator and possibly operator, and its model corresponds to a special Heyting algebra. This kind of Heyting algebra can also corresponds to a modal of this modal logic. Because of this corresponding relationship, I try to transform some concepts and properties which in model theory and algebra into the extension of basic proposition logic, containing reduction, embedding, isomorphism.