Першопорядковi композиційно-номінативні логіки з предикатами слабкої та строгої рівності

Abstract

Досліджено нові програмно-орієнтовані логіки часткових предикатів з операцією (композицією) предикатного доповнення, такі логіки названо LC. Для першопорядкових LC запропоновано низку відношень логічного наслідку та відношень логічного наслідку за умови невизначеності. Досліджено властивості цих відношень, встановлено співвідношення між ними. Для відношень типів |=T та |=F доведено теорему про елімінацію умов невизначеності. Для запропонованих відношень описано умови їх гарантованої наявності, наведено властивості декомпозиції формул та елімінації кванторів.

В работе исследованы новые программно-ориентированные логические формализмы – композиционно-номинативные логики с предикатами равенства и композицией предикатного дополнения, такие логики названы LCE. Можно выделить предикаты слабого равенства и строгого равенства. Отсюда получаем LCE с предикатами слабого равенства, их назовем LCEw, и LCE с предикатами строгого равенства, их назовем LCEs. LCE можно рассматривать на первопорядковом уровне и реноминативном уровне. Рассмотрены композиционные алгебры LCE, исследованы свойства их композиций, описаны первопорядковые языки этих логик. Основное внимание сосредоточено на исследовании свойств, связанных с предикатами равенства и композицией предикатного дополнения. Введен и исследован ряд отношений логического следствия в первопорядковых LCE, рассмотрены их особенности. В частности, установлена определенная вырожденность LCEw, для которой корректным оказывается только отношение неопровержимого логического следствия в условиях неопределенности. Подробное исследование в LCE отношений логического следствия в условиях неопределенности будет проведено в последующих роботах. Свойства отношений логического следствия в LСE является семантической основой построения соответствующих исчислений секвенциального типа. Такое построения тоже планируется осуществить в последующих роботах.

Development of the new software-oriented logical formalisms is a topical problem. The paper introduces logics of partial predicates with predicate complement and equality predicates, we denote them LCE. They extend logics of quasiary predicates with equality and logics with predicate complement. The composition of the predicate complement is used in Floyd-Hoare program logics’ extensions on the class of partial predicates. We define predicates of weak equality and of strong equality. Thus, LCE with predicates of weak equality (denoted by LCEw) and LCE with predicates of strong equality (denoted by LCEs) can be specified. LCE can be studied on the first order and renominative levels. We consider composition algebras of LCE, investigate properties of their compositions and describe first order languages of such logics. We concentrate on the properties related to the equality predicates and the composition of the predicate complement.