Composition nominative modal logics of partial non-monotone predicates and their calculi

Abstract

We consider new program-oriented logical formalisms of modal type – pure first-order composition nominative modal logics of partial predicates without monotonicity restriction. For such logics we specify semantic models and languages and investigate interactions of modal compositions with renominations and quantifiers. A consequence relation for two formulas in a given state is introduced and generalized to a logical consequence relation for two sets of formulas specified with states. We describe properties of a logical consequence relation for sets of formulas specified with states and properties of modalities elimination for various reachability relations. Sequent type calculi are proposed for general transitional and temporal modal logics of non-monotone predicates. We define various types of the calculi for different reachability relations and specify their basic sequent forms and sequent closure conditions. We give a step-by-step description of a deriving process (building of a sequent tree) by the introduced calculi. For these calculi we prove the soundness theorem and the theorem about existence of a counter-model for a non-closed path in a sequent tree. The counter-model is obtained using the Hintikka sets method. The proof of the completeness theorem is based on the theorem about existence of a counter-model.

Problems in programming 2017; 2: 24-39