Спектр логік часткових предикатів, орієнтованих на композиційнo-номінативні моделі програм

Размещено на http://www.allbest.ru/

Київський національний університет імені Тараса Шевченка

УДК 004.42:510.69

Спектр логік часткових предикатів, орієнтованих на композиційнo-номінативні моделі програм

01.05.01 - теоретичні основи інформатики та кібернетики

АВТОРЕФЕРАТ

дисертації на здобуття наукового ступеня

доктора фізико-математичних наук

Шкільняк Степан Степанович

Київ 2010

Дисертацією є рукопис.

Робота виконана на кафедрі теорії та технології програмування Київського національного університету імені Тараса Шевченка.

Науковий консультант: доктор фізико-математичних наук, професор

НІКІТЧЕНКО Микола Степанович, Київський національний університет імені Тараса Шевченка, завідувач кафедри теорії та технології програмування.

Офіційні опоненти: академік НАН України, доктор фізико-математичних наук, професор ЛЕТИЧЕВСЬКИЙ Олександр Адольфович,

Інститут кібернетики імені В.М.Глушкова НАН України, завідувач відділом теорії цифрових автоматів; доктор фізико-математичних наук, професор КРИВИЙ Сергій Лук'янович,

Київський національний університет імені Тараса Шевченка, професор кафедри інформаційних систем; доктор фізико-математичних наук, старший науковий співробітник ЯДЖАК Михайло Степанович,

Інститут прикладних проблем механіки і математики імені Я.С.Підстригача НАН України, провідний науковий співробітник.

Захист відбудеться 9 грудня 2010 р. о 14 годині на засіданні спеціалізованої вченої ради Д 26.001.09 Київського національного університету імені Тараса Шевченка за адресою: 03127, Київ, пр. акад. Глушкова, 4д, факультет кібернетики, ауд. 40.

З дисертацією можна ознайомитися у Науковій бібліотеці імені М. Максимовича Київського національного університету імені Тараса Шевченка за адресою: 01033, Київ, вул. Володимирська, 58.

Автореферат розісланий “___” ______________ 2010 року

Вчений секретар спеціалізованої вченої ради В.П. Шевченко

гільбертівський предикат квазіарний

АНОТАЦІЯ

Шкільняк С. С. Спектр логік часткових предикатів, орієнтованих на композиційнo-номінативні моделі програм. - Рукопис.

Дисертація на здобуття наукового ступеня доктора фізико-математичних наук за спеціальністю 01.05.01 - теоретичні основи інформатики та кібернетики. - Київський національний університет імені Тараса Шевченка, Київ, 2010.

Метою дисертаційної роботи є побудова та дослідження класів логік часткових предикатів, орієнтованих на композиційнo-номінативні моделі програм. Досліджено семантичні властивості композиційно-номінативних логік квазіарних предикатів реномінативного й першопорядкових рівнів. Виділено й досліджено неокласичні логіки, близькі до класичної логіки предикатів - логіки еквітонних предикатів та їх розширення. Для неокласичних логік побудовано і досліджено числення гільбертівського типу та ґенценівського (секвенційного) типу, для них доведені теореми коректності й повноти, отримано важливі наслідки теореми повноти. Низка отриманих результатів є узагальненнями відомих тверджень класичної логіки. Запропоновано і досліджено різні формалізації відношення логічного наслідку для композиційно-номінативних логік часткових однозначних, тотальних та часткових неоднозначних квазіарних предикатів. На базі логіки квазіарних предикатів як основи побудови спеціальних логік запропоновано композиційно-номінативні модальні та темпоральні логіки, збудовано та досліджено логіки над ієрархічними номінативними даними. Результати роботи можуть застосовуватися при розробці інформаційних та програмних систем, зокрема, систем верифікації та специфікації програм.

Ключові слова: моделі програм, логіка, частковий предикат, логічний наслідок, семантика, числення, коректність, повнота.

АННОТАЦИЯ

Шкильняк С. С. Спектр логик частичных предикатов, ориентированных на композиционнo-номинативные модели программ. - Рукопись.

Диссертация на соискание ученой степени доктора физико-математических наук по специальности 01.05.01 - теоретические основы информатики и кибернетики. - Киевский национальный университет имени Тараса Шевченко, Киев, 2010.

Целью работы является построение и исследование классов логик частичных предикатов, ориентированных на композиционно-номинативные модели программ. Разработаны разнообразные логические системы, которые успешно используются в програмировании. Такие системы обычно базируются на классической логике предикатов. Но классическая логика имеет принципиальные ограничения, которые усложняют ее использование. Это мотивирует необходимость построения новых логик, болee адаптированных к потребностям программирования, что обуславливает важность и актуальность диссертации. Основой такого построения выбран общий для логики и программирования композиционно-номинативный подход.

На основе развития понятия данного выделены уровни абстракции рассмотрения, которые определяют интенсиональные (содержательные) модели композиционно-номинативных логик. Основное внимание уделено логикам номинативного уровня, в котором выделяются реноминативный и первопорядковые подуровни: кванторный, кванторно-эквациональный, функциональный, функционально-эквациональный. На этих уровнях данные имеют вид именного множества. Функции и предикаты, заданные на именных множествах, названы квазиарными. Предложен спектр композиционно-номинативных логик по уровню абстракции рассмотрения и по ограничениям на класс квазиарных предикатов. Классические первопорядковые логики являются частным случаем первопорядковых логик квазиарных предикатов. Исследованы композиции и композиционные системы квазиарных функций и предикатов на разных уровнях.

Исследованы на абстрактном уровне понятия алгебры, алгебраической системы, гомоморфизмов, предложена классификация таких гомоморфизмов. Рассмотрены алгебраические системы с квазиарными функциями и предикатами, названные неоклассическими, исследованы их гомоморфизмы. Для неоклассических логик (логик эквитонных предикатов) доказаны теоремы о гомоморфизмах и изоморфизмах. Они обобщают соответствующие теоремы классической логики.

Построены композиционно-номинативные логики квазиарных предикатов реноминативного и первопорядковых уровней. Описаны языки, исследованы семантические свойства логик таких уровней. Для формул предложены классическиподобные нормальные формы, доказаны теоремы о сведении формул к нормальным формам. Исследовано отношение логического следствия для множеств формул.

Выделены и исследованы неоклассические логики, по свойствам близкие к классической логике предикатов Это логики эквитонных квазиарных предикатов и их расширения: логики локально-эквитонных, эквисовместных и локально-эквисовместных предикатов. Они имеют большие выразительные возможности по сравнению с классической логикой и более широкие классы семантических моделей, при этом неоклассические логики сохраняют основные ее свойства.

Для логик полнототальных эквитонных предикатов соответствующего уровня построены формально-аксиоматические системы гильбертовского типа. Исследованы свойства построенных исчислений, доказаны теоремы корректности и полноты.

Для логик эквитонных предикатов соответствующего уровня построены системы генценовского типа - секвенциальные исчисления. Исследованы свойства таких исчислений, для них доказаны теоремы корректности и полноты. Получены важные следствия теоремы полноты (теорема компактности, теорема о существовании модели). Для логик эквитонных квазиарных предикатов доказаны интерполяционная теорема, теоремы об определимости. Полученные результаты обобщают известные результаты классической логики, в частности, теорему компактности и ее следствия, интерполяционную теорему Крейга, теорему Бета об определимости.

Исследованы композиционно-номинативные логики частичных однозначных, тотальных и частичных неоднозначных квазиарных предикатов. Для них предложены разные семантики и разные формализации отношения логического следования. Изучены свойства и определены соотношения между такими формализациями в разных семантиках. Это обобщает результаты Е.Д.Смирновой, полученные для пропозициональной логики, на случай логик квазиарних предикатов.

Построенные в работе композиционно-номинативные логики квазиарных предикатов служат основой для построения новых специальных логик. Это проиллюстрировано построением композиционно-номинативных модальных логик, в рамках которых выделены темпоральные композиционно-номинативные логики.

На базе логик квазиарных предикатов построены композиционно-номинативные логики частичных предикатов над иерархическими номинативными данными, ориєнтированные на описание свойств распостраненных в программировании отображений, заданных на данных со сложной структурой. Предложены семантические модели и языки таких логик, исследованы их свойства.

Результаты диссертационного исследования могут применяться при разработке информационных и программных систем, они используются при разработке систем верификации и спецификации программ. На основе результатов работы построена система автоматизированного доказательства теорем теории метаноминативных данных.

Ключевые слова: модели программ, логика, частичный предикат, логическое следствие, семантика, исчисление, корректность, полнота.

АBSTRACT

SHKILNIAK S.S. Spectrum of logics of partial predicates oriented on composition-nominative program models. - Manuscript.

Thesis for a doctor's degree of physics and mathematics by speciality 01.05.01 -- theoretical foundations of informatics and cybernetics. - Taras Shevchenko National University of Kyiv, Kyiv, 2010.

The purpose of this dissertation is the creation and investigation of various classes of logics of partial predicates oriented on composition-nominative program models. Semantic properties of composition-nominative logics of quasi-ary predicates of renominative and first-order levels are studied. Neoclassical logics such as logics of equitone predicates and their extensions are defined and investigated. They preserve main properties of classical predicate logic. For neoclassical logics, Hilbert and Gentzen (sequent) calculi are constructed and investigated, soundness and completeness theorems are proved, and important corollaries of completeness theorem are obtained. Many of the obtained results are generalizations of well-known statements of classical logic. Different formalizations of relation of logical consequence of composition-nominative logics of partial single-valued, total and partial ambiguous quasi-ary predicates are proposed and investigated.

Logics of quasi-ary predicates can be considered as a foundation for creation of specific logics. On their basis, composition-nominative modal and temporal logics are introduced, and logics over hierarchical nominative data are constructed and investigated. The results obtained in the dissertation can be used in program and information systems development, for program verification and specification systems.

Key words: program models, logic, partial predicate, logical consequence, semantics, calculus, soundness, completeness.

1. ЗАГАЛЬНА ХАРАКТЕРИСТИКА РОБОТИ

Актуальність теми. Бурхливий розвиток інформаційних технологій та їх проникнення в усі сфери діяльності людини роблять особливо актуальною задачу створення надійних та ефективних програмних систем. Успішне вирішення цієї задачі неможливе без широкого використання понять і методів математичної логіки.

Логіка тісно пов'язана з програмуванням із самого початку його виникнення. В рамках математичної логіки запропоновано перші формалізації уточнення поняття алгоритму, мови програмування базуються на тих чи інших уточненнях цього поняття. Апарат математичної логіки (алгебра логіки) ліг в основу схемотехніки комп'ютерів.

Подальший розвиток програмування і пов'язана з цим поява нових задач і проблем ведуть до залучення для їх розв'язку все нових понять і засобів математичної логіки (теорія доведень, інтуїціоністські, модальні, темпоральні, епістемічні, динамічні, програмні логіки тощо). Для розв'язання задач верифікації та специфікації програм плідним виявився апарат модальних і темпоральних логік. Таким чином, логіка набуває чітко окресленого прикладного аспекту. Результати, отримані в області математичної логіки, та задачі, які розв'язуються її засобами і методами, знаходять різноманітні й ефективні застосування в різних розділах програмування.

Логіко-алгебраїчний підхід до розв'язання проблем інформатики та програмування завжди був у центрі уваги Київської школи кібернетики. Започаткований В.М. Глушковим, він отримав подальший розвиток в роботах його соратників та учнів К.Л.Ющенко, П.І.Андона, А.В.Анісімова, Ю.В.Капітонової, О.А.Летичевського, В.Н.Редька, Г.О.Цейтліна та багатьох інших. Важливим кроком в цьому напрямі є розроблене В.Н. Редьком композиційне (експлікативне) програмування, яке успішно розвивається його учнями. Подальшим розвитком композиційного програмування є запропонований М.С. Нікітченком композиційно-номінативний підхід до побудови моделей програм і орієнтованих на них логік. Зазначений підхід дає можливість застосування побудованих моделей як в програмуванні, так і в логіці, що дозволяє природним чином поєднати логіку з програмуванням.

Таким чином, наявний глибокий і нерозривний зв'язок логіки й програмування. З одного боку, поняття і методи математичної логіки доводять свою ефективність при розв'язанні широкого кола задач інформатики й програмування. З іншого боку, таке використання індукує зворотний вплив програмування на логіку, вимагає зробити математичну логіку ближчою й адекватнішою до потреб програмування.

На даний момент розроблено дуже багато різноманітних логічних систем, які успішно використовуються в програмуванні. Такі системи звичайно базуються на класичній логіці предикатів. Ця логіка добре досліджена, вона має багатий досвід застосування. На основі класичної будуються спеціальні логіки, орієнтовані на вирішення тих чи інших конкретних задач програмування. Водночас поява нових застосувань логіки в інформатиці та програмуванні висвітила принципові обмеження класичної логіки предикатів, які ускладнюють її використання. Така логіка базується на традиційних математичних структурах однозначних тотальних скінченно-арних відображень, вона недостатньо враховує неповноту, частковість інформації про предметну область, її структурованість.

Таким чином, на перший план виходить проблема побудови нових, програмно-орієнтованих логічних формалізмів, що зумовлює актуальність дисертаційного дослідження. Основою такої побудови в дисертаційній роботі вибрано спільний для логіки і програмування композиційно-номінативний підхід. На базі цього підходу в роботі побудовано й досліджено класи логік часткових предикатів, орієнтованих на композиційно-номінативні моделі програм.

Зв'язок роботи з науковими програмами, планами, темами. Дисертаційна робота виконувалась у відповідності до плану наукових досліджень кафедри теорії та технології програмування Київського національного університету імені Тараса Шевченка в межах таких науково-дослідних тем: "Дослідження універсальних та спеціалізованих прикладних логік" (1996-2000, ДР № 0197U003444), "Логіко-математичні та програмологічні засоби інформаційних технологій" (2001-2005, ДР № 0101U002163), "Розробка конструктивних математичних формалізмів для інтелектуальних систем прийняття рішень, обробки знань, еталонування мов сучасних СУБД і CASE-засобів" (2006-2010, ДР № 0106U005856), "Формальні специфікації програмних систем" (2008-2009, ДР № 08U002463).

Мета і задачі дослідження. Метою дисертаційної роботи є побудова та дослідження спектру логік часткових предикатів, орієнтованих на композиційно-номінативні моделі програм. Відповідно до сформульованої мети, в дисертації ставляться такі задачі:

- на основі спільного для логіки й програмування композиційно-номінативного підходу побудувати й дослідити класи логік часткових предикатів на різних рівнях абстрактності й загальності;

- дослідити семантичні властивості композиційно-номінативних логік квазіарних предикатів реномінативного й першопорядкових рівнів;

- виділити й дослідити неокласичні логіки, близькі до класичної логіки предикатів;

- для неокласичних логік побудувати й дослідити числення гільбертівського типу та ґенценівського (секвенційного) типу;

- дослідити різні формалізації відношення логічного наслідку для композиційно-номінативних логік часткових однозначних, тотальних та часткових неоднозначних квазіарних предикатів;

- проілюструвати можливості логіки квазіарних предикатів побудовою на її основі спеціальних логік: композиційно-номінативних модальних логік, а також логік, орієнтованих на опис поширених в програмуванні відображень над даними із складною структурою.

Об'єктом дослідження дисертаційної роботи є програмно-орієнтовані логічні системи.

Предмет дослідження - логічні формалізми, орієнтовані на моделі програм.

Методи дослідження - логіко-математичні. В дисертаційній роботі використовуються методи математичної логіки, апарат універсальних алгебр, композиційно-номінативний підхід до побудови моделей програм та орієнтованих на них логік.

Наукова новизна одержаних результатів. В дисертаційній роботі вперше побудовані та досліджені нові логіки, орієнтовані на композиційно-номінативні моделі програм:

- виділено рівні розгляду, які визначають інтенсіональні моделі композиційно-номінативних логік; вперше запропоновано спектр таких логік за рівнем абстракції розгляду та за обмеженнями на клас квазіарних предикатів;

- побудовано нові композиційно-номінативні логіки квазіарних предикатів реномінативного та першопорядкових рівнів: кванторного, кванторно-екваційного, функціонального, функціонально-екваційного; досліджено семантичні властивості логік відповідного рівня;

- виділено та досліджено логіки, близькі до класичної - неокласичні логіки еквітонних предикатів; запропоновано та досліджено їх розширення;

- для логік повнототальних еквітонних предикатів відповідного рівня вперше побудовано та досліджено числення гільбертівського типу, для них доведено теореми коректності та повноти;

- для логік еквітонних квазіарних предикатів відповідного рівня вперше побудовано та досліджено числення секвенційного типу, для них доведено теореми коректності й повноти;

- вперше досліджено композиційно-номінативні логіки часткових однозначних, тотальних та часткових неоднозначних квазіарних предикатів, для них запропоновано різні семантики та різні формалізації відношення логічного наслідку; досліджено властивості таких відношень в різних семантиках;

- збудовані в роботі нові логіки квазіарних предикатів є основою для побудови спеціальних логік; на їх базі запропоновано нові композиційно-номінативні модальні та темпоральні логіки, побудовано та досліджено нові логіки над ієрархічними номінативними даними, орієнтовані на опис властивостей відображень, визначених на даних із складною структурою.

Практичне значення одержаних результатів. Побудовані в дисертаційній роботі неокласичні логіки зберігають основні закони класичної логіки предикатів, тому дозволяють використовувати багатий досвід її застосування при істотному розширенні класу семантичних моделей та збільшенні виразних можливостей. Водночас неокласичні логіки ближчі до програмування і тому більше адаптовані до його потреб. Запропоновані в роботі композиційно номінативні логіки квазіарних предикатів є основою для побудови спеціальних логік. На підтвердження цього в роботі будуються композиційно-номінативні модальні та темпоральні логіки, які орієнтовані на опис і моделювання інформаційних та складних динамічних систем, а також логіки над ієрархічними номінативними даними, які дають змогу більш адекватно описувати властивості поширених в програмуванні відображень, визначених на даних із складною структурою.

Результати досліджень за темою дисертації можуть застосовуватися при розробці інформаційних та програмних систем, зокрема, вони використовуються при розробці систем верифікації та специфікації програм. На основі результатів даної дисертаційної роботи побудована система автоматизованого доведення теорем теорії метаномінативних даних (див.також [27, 36]).

Результати дисертаційного дослідження впроваджені в навчальний процес факультету кібернетики Київського національного університету імені Тараса Шевченка. Методологічні та теоретичні результати дисертаційної роботи покладені в основу нормативних курсів "Математична логіка" та "Прикладна логіка", вони використовуються в нормативних курсах "Теорія алгоритмів", "Математична логіка та теорія алгоритмів", "Теорія програмування". Результати дисертаційного дослідження практично втілені, зокрема, в підручнику та навчальних посібниках,,.

Результати досліджень за темою дисертації використані при проведенні науково-дослідної роботи Ф3/03-99 за темою "Дослiдження і розробка формальних методiв для моделювання комп'ютерних систем керування складними динамiчними об'єктами з критичними режимами функцiонування" в Інституті програмних систем НАН України (1999-2001).

Особистий внесок здобувача. Всі результати, які складають суть дисертаційної роботи, отримані здобувачем самостійно. З робіт, виконаних із співавторами, на захист виносяться тільки результати, отримані особисто здобувачем.

Апробація результатів дисертації. Матеріали дисертаційного дослідження доповідалися та обговорювалися на наукових семінарах Київського національного університету імені Тараса Шевченка, Інституту програмних систем НАН України, Національного університету "Києво-Могилянська Академія". Основні результати роботи доповідалися на таких наукових конференціях та симпозіумах:

- Міжнародні науково-практичні конференції з програмування УкрПрог '2002, УкрПрог '2004, УкрПрог '2006, УкрПрог '2008, УкрПрог '2010;

- Міжнародні конференції "Теоретичні й прикладні аспекти побудови програмних систем" TAAPSD '2004, TAAPSD '2005, TAAPSD '2006, TAAPSD '2007, TAAPSD '2009;

- Міжнародні конференції "Dynamical systems modelling and stability investigation" (Київ, 2001, 2003, 2005, 2007, 2009);

- Міжнародні конференції "Problems of decision making under uncertainties" (2003-2010);

- Second St.Peterburg Days of Logic and Computablity (St.Peterburg, 2003);

- International conference "Computer science and information technologies" (Yerevan, Armenia, 2005);

- International conference "Electronic computers and informatics ECI 2006" (Koљice-Herlany, Slovakia, 2006),

- 10th International Conference on Informatics "Informatics 2009" (Koљice-Herlany, Slovakia, 2009);

- International Workshop "Automata, algorithms and information technologies" (Київ, 2010).

Публікації. Основні результати дисертаційної роботи викладено в 32 статтях [1-32] у наукових фахових виданнях, затверджених ВАК України. Серед цих робіт 15 опубліковано без співавторів. Результати досліджень за темою дисертації відображені, зокрема, в тезах міжнародних конференцій та симпозіумів [33-39].

Структура та обсяг роботи. Дисертаційна робота складається із вступу, шести розділів, висновків, списку використаних джерел (189 посилань, 16 с.) та двох додатків (доведення технічних тверджень та теорем, 39 с.). Робота містить 2 рисунки. Загальний обсяг дисертації складає 293 стор., повний текст роботи (із додатками та списком використаних джерел) має обсяг 348 стор.

2. ОСНОВНИЙ ЗМІСТ

У вступі обґрунтовано актуальність роботи, сформульовано мету та основні задачі дослідження. Зроблено огляд літератури за темою дисертації, наведено основні результати, отримані здобувачем, відзначено їх наукову новизну. Надано відомості про практичне значення роботи та апробацію результатів дисертації.

В першому розділі роботи досліжуються композиційно-номінативні моделі логічних систем, орієнтованих на задачі програмування. Мотивовано необхідність перебудови логіки в семантико-синтаксичному стилі та обгрунтовано провідну роль алгебраїчних і композиційно-номінативних аспектів для побудови нових логік, орієнтованих на дослідження програм. Обгрунтовано вибір спільного для логіки і програмування композиційно-номінативного підходу як основи такої побудови.

На базі розвитку поняття даного виділено рівні розгляду, які визначають інтенсіональні моделі композиційно-номінативних логік. Запропоновано спектр таких логік за рівнем абстракції розгляду та за обмеженнями на клас квазіарних предикатів. Досліджено композиційні системи квазіарних функцій та предикатів на різних рівнях.

Аспекти, пов'язані з алгебраїчним поданням моделей предметних областей, а саме з засобами конструювання (композиціями) та методами їх опису, є одними з найважливіших для побудови нових логік, орієнтованих на потреби програмування. Тому для такої побудови велике значення має дослідження фундаментального поняття алгебри. В розділі дано узагальнені визначення на абстрактному рівні понять алгебри, алгебраїчної системи, гомоморфізмів алгебр і алгебраїчних систем, запропонована класифікація таких гомоморфізмів. Визначаються неокласичні алгебраїчні системи з квазіарними функціями та предикатами, алгебраїчні системи з доданою сигнатурою.

В підрозділі 1.1 розглядаються основні аспекти логік, орієнтованих на дослідження програм, та проблема програмно-орієнтованої перебудови класичної логіки.

Обмеження класичної логіки предикатів мотивують необхідність побудови нових логік, більше орієнтованих на потреби програмування.

Для уточнення основних аспектів логік, орієнтованих на дослідження програм, зроблено стислий розгляд з семантичного погляду основних конструкцій традиційних мов програмування та їх формалізації. На цій основі можна зробити висновки, які є основоположними для побудови програмно-орієнтованих логік, вони визначають провідну роль для цих логік алгебраїчних та композиційно-номінативних аспектів.

По-перше, формалізація здійснюється на базі різних видів алгебр даних та програмних алгебр (алгебр функцій). По-друге, побудова складних даних із простіших відбувається на основі відношень іменування (номінативних відношень), а побудова складних функцій, що задають семантику програм (програмних функцій), відбувається за допомогою композицій. По-третє, фундаментальними властивостями програмних функцій є їх еквітонність та монотонність.

Основою побудови нових логік є спільний для логіки і програмування композиційно-номінативний підхід. Він опирається на загальнометодологічний принцип розвитку як сходження від абстрактного до конкретного і базується на таких основних принципах: інтегрованості інтенсіональних та екстенсіональних аспектів, пріоритетності семантики над синтаксисом, композиційності, номінативності.

Згідно цього підходу програмні поняття формалізуємо за допомогою композиційно-номінативних систем. Центральним поняттям логіки є поняття предиката. З математичного погляду предикати - це функції, значеннями яких є істиннісні значення. Тому класи предикатів можна задавати композиційно-номінативними системами. Це дозволяє подавати і вивчати логічні та програмні системи в єдиному стилі.

В підрозділі 1.2 розглядаються інтенсіональні аспекти логічних понять. Виділення у висловленнях двох складових - форми та змісту (синтаксису та семантики) - веде до уточнення поняття логіки як абстрактної логіки моделей світів. Її задаємо як об'єкт (IM, EM, Frm, I, |=, |- ), де IM - інтенсіональна модель світу, EM - клас одиничних екстенсіональних моделей, Frm - клас формул мови, I - клас відображень інтерпретації формул в екстенсіональних моделях, |= - клас істинних формул, |- - клас вивідних формул (теорем). Інтенсіональна модель займає провідну позицію, вона специфікує логіку згідно рівня абстракції та індукує мову логіки.

Подальший розвиток веде до композиційно-номінативних логік (КНЛ). На цьому рівні модель світу задається певним класом D станів, які назвемо даними, класом предикатів Pr, заданих на станах світу, та операторами (композиціями) породження нових предикатів. Екстенсіональна модель задається як предикатна композиційна система (D, Pr, C). Така система задає дві алгебри: алгебру (алгебраїчну систему) даних (D, Pr) та алгебру предикатів (Pr, C), терми якої трактуються як формули мови логіки. Центральним тут є поняття композиції, адже саме композиції визначають універсальні методи побудови предикатів, виступаючи ядром логіки певного типу.

Інтенсіональні моделі КНЛ в першу чергу задаються рівнями розгляду даних. Розвиток поняття даного веде до трьох базових рівнів: D.W (дане як ціле), D.P (дане як структуроване), D.H (дане як ієрархічне). Кожен з них розпадається три підрівні: A (абстрактний), C (конкретний), S (синтетичний). Звідси 9 рівнів розгляду даних:

D.W.A; D.W.C; D.W.S; D.P.A; D.P.C; D.P.S; D.H.A; D.H.C; D.H.S.

КНЛ будуємо за семантико-синтаксичною схемою. Це означає наступне.

1. Спочатку задаємо інтенсіональні (змістовні) моделі логік. Такі моделі найперше визначаються рівнями розгляду даних, тому для їх задання фіксуємо рівень абстракції розгляду. Інтенсіональні моделі індукують мову логіки відповідного рівня.

2. Будуємо відповідні розглянутому рівню екстенсіональні моделі, які задають семантичні аспекти логік, - предикатні композиційні системи.

3. Будуємо формально-аксіоматичні логічні числення, які задають синтаксичні аспекти логік. Основні їх типи - формальні системи гільбертівського типу і системи ґенценівського типу (секвенційні числення, системи натурального виведення).

В підрозділі 1.3 запропоновано спектр композиційно-номінативних логік за рівнем абстракції розгляду та за обмеженнями на клас квазіарних предикатів.

Згідно з композиційно-номінативним підходом, побудову логік починаємо з гранично-абстрактних рівнів, поступово їх конкретизуючи.

Пропозиційний рівень. На рівні D.W.A дані трактуються гранично абстрактно, як "чорні скриньки". Предикати мають вигляд A {T, F}, де A - сукупність абстрактних даних, {T, F} - множина істиннісних значень. Базові композиції: Клінієві і .

Сингулярний рівень. На рівні D.W.C дані трактуються гранично конкретно, як "білі" скриньки. На цьому рівні фіксується єдиний клас даних. Для сингулярних логік М.С.Нікітченком збудована інфінітарна алгебра сингулярних композицій Кліні.

На наступному рівні абстракції D.P. дані розглядаються як сукупності. Рівням D.P.А та D.P.С відповідають спеціальні логіки, які вимагають окремого дослідження.

Номінативний рівень. На рівні D.P.S дані розглядаються як "сірі" скриньки, побудовані з "білих" і "чорних". Такі дані називаються номінатами. Номінативний рівень є дуже багатим і розпадається на низку підрівнів. Найважливішим є підрівень однозначних номінатів - іменних множин (ІМ). V-іменна множина (V-ІМ) над A - це довільна однозначна функція : VA. Тут A і V трактуємо як множину предметних імен і множину предметних значень. Клас всіх V-ІМ над A позначимо VA. Можна виділити підкласи скінченних V-ІМ та повних V-ІМ - тотальних функцій VA.

Функцію вигляду f : VA А назвемо V-квазіарною функцією на A.

Функцію вигляду Р : VA {T, F} назвемо V-квазіарним предикатом на A.

Класи V-квазіарних функцій і V-квазіарних предикатів на A позначаємо FnА і PrA.

КНЛ рівня іменних множин будемо називати логіками квазіарних предикатів.

На рівні ІМ далі виділяємо реномінативний рівень та першопорядкові рівні: кванторний, кванторно-екваційний, функціональний, функціонально-екваційний.

Реномінативний рівень. Найабстрактнішими серед логік номінативного рівня є реномінативні. На цьому рівні можна перейменовувати компоненти даних, що дає змогу ввести нову композицію реномінації R. Базові композиції: , , R.

Кванторний рівень. На цьому рівні можна застосовувати квазіарні предикати до всіх предметних значень, що дозволяє ввести композиції квантифікації x та x. Базовими композиціями логік кванторного рівня є , , R, x.

Кванторно-екваційний рівень. Тут можна ототожнювати й розрізняти значення предметних імен за допомогою спеціальних 0-арних композицій - параметризованих за іменами предикатів рівності =ху . Базові композиції: , , R, x, =ху .

Функціональний рівень. На цьому рівні маємо розширені можливості формування нових аргументів для функцій та предикатів. Це дає змогу ввести композицію суперпозиції S Для роботи з окремими компонентами даних виділяємо спеціальні 0-арні композиції - функції деномінації (розіменування) 'x, xV. При їх введенні реномінації моделюємо за допомогою суперпозицій. Базові композиції: , , S x, 'x.

Функціонально-екваційний рівень. На додаток до можливостей функціонального рівня, тут можна ототожнювати й розрізняти предметні значення, що дає змогу ввести спеціальну композицію рівності = . Базові композиції: , , S x, 'x, =.

На рівні D.H дані розглядаються як ієрархічні. Виродженим рівням D.H.А та D.H.С відповідають спеціальні логіки, які вимагають окремого дослідження.

Ієрархічно-номінативний рівень. На рівні D.H.S дані можна розглядати як ієрархічні номінати. Вони будуються індуктивно із множини предметних імен та множини предметних значень. Ієрархічно-номінативний рівень дуже багатий, зроблено лише перші кроки його дослідження. Можна виділити такі його початкові підрівні:

- логіки над даними із складними іменами (вони описані в підрозділі 6.2);

- логіки над структурованими даними;

- логіки над скінченними ієрархічними даними (логіки номінативних даних).

Для логік квазіарних предикатів вже не виконуються деякі закони класичної логіки, тому клас квазіарних предикатів варто обмежити. Перше обмеження - це еквітонність, яка означає збереження прийнятого значення при розширенні даних, вона притаманна предикатам класичної логіки. Ця властивість дуже важлива для програмування. Друге обмеження, теж притаманне класичній логіці - визначеність предиката на кожному повному даному. Ця властивість називається повнототальністю.

Класична логіка є логікою скінченно-арних тотальних предикатів. До неї найближчі догіки повнототальних еквітонних предикатів. Вони зберігають основні закони класичної логіки при істотному розширенні класу семантичних моделей. Водночас такі логіки та класична логіка не є ідентичними. Визначальною властивістю логік квазіарних предикатів, що істотно відрізняє їх від класичної, є можливість для формули бути залежною від нескінченної множини предметних імен.

Логіки еквітонних предикатів підпорядковуються основним законам класичної логіки, проте для них уже не діють деякі правила виведення (modus ponens), порушуються певні властивості класичної логіки. Логіки еквітонних і повнототальних еквітонних предикатів названі неокласичними через їх близькість до класичної логіки.

Узагальненням еквітонних є локально-еквітонні предикати. Для них вимагається збереження значення при розширенні даних лише на скінченну кількість компонент.

Логіки, орієнтовані на такі особливості предметних областей, як неповнота наявної інформації, базуються на класах предикатів, визначених на даних з неповною інформацією. Такими є еквісумісні та локально-еквісумісні предикати. Еквісумісність означає, що за можливості розширення різних даних (сумісність даних) до одного більшого значення предиката на таких даних мають збігатися. При локально-еквісумісності вимагаємо збереження значень лише для розширень скінченною інформацією.

При переході від логік повнототальних еквітонних до логік еквітонних предикатів, від них до логік локально-еквітонних та логік еквісумісних предикатів, а далі до логік локально-еквісумісних предикатів, ми отримуємо все ширші класи семантичних моделей. Такі логіки мають більші виразні можливості порівнянно із класичною логікою, водночас ці логіки зберігають основні її закони.

Спектр КНЛ за обмеженнями на клас квазіарних предикатів наведено на рис.1.2.

В підрозділі 1.4 визначаються і досліджуються композиції та композиційні системи квазіарних функцій і предикатів на різних рівнях розгляду. Наводяться основні властивості введених композицій.

Введемо необхідні для подальшого викладу визначення.

Областю істинності та областю хибності предиката Р на множині D назвемо множини

T(P) = {dD | P(d) = T} та F(P) = {dD | P(d) = F}.

Предикат P виконуваний, якщо T(P) .

Предикат P неспростовний, або частково істинний, якщо F(P) = .

Вводимо функцію im : VA2V так: im() = {vV | va для деякого aA}.

Визначаємо ¦Х = {va | vX}, де ХV. Замість ¦(V\{х}) пишемо ¦-х.

Визначаємо 12 = 2 (1¦(V \ im(2))). Параметричну операцію реномінації r: VА VA задаємо так: r() = [v1(x1),...,vn(xn)](¦(V\{v1,...,vn})).

Композиції пропозиційного рівня подібні до відповідних класичних логічних зв'язок, але ми враховуємо частковість предикатів, це фактично сильні Клінієві зв'язки.

На реномінативному рівні вводимо композицію реномінації R: PrА PrА. Зазначену композицію визначаємо через операцію реномінації: R(P)(d) = r((P)(d)).

На кванторному рівні з'являються композиції квантифікації x тa x. Наведемо визначення композиції x: T(xP) = {dVA | Р(dxa) = T для деякого aA},

F(xP) = {dVA | Р(dxa) = F для всіх aA}.

На кванторно-екваційному рівні вводимо спеціальні 0-арні композиції - параметризовані за іменами предикати рівності =xy . Вони визначаються такою умовою:

=ху (d) = T, якщо d(x) = d(y); =ху (d) = F, якщо d(x) d(y); інакше =ху (d).

На функціональному рівні вводимо нову композицію суперпозиції.

Нехай FА - довільний клас функцій вигляду f : VAR. (n+1)-арна параметрична композиція суперпозиції S: FА (FnА)n FА задається такою умовою:

S(f, g1, ..., gn)(d) = f([v1g1(d),...,vngn(d)](d¦(V\{v1,...,vn}))).

Далі розглядаємо суперпозиції двох типів: (FnA)n+1 FnA та PrA (FnA)n PrA.

На цьому рівні задаємо множину NfА = {'v | vV} спеціальних 0-арних композицій - функцій деномінації (розіменування). Вони визначаються умовою 'v(d) = d(v).

На функціонально-екваційному рівні додатково вводимо композицію рівності = : FnAFnAPrA, яка визначається такою умовою: = (f, g)(d) = T, якщо f(d) = g(d), = (f, g)(d) = F, якщо f(d) g(d); = (f, g)(d), якщо f(d) або g(d).

Композиції , , R x зберігають еквітонність і повнототальність V-квазіарних предикатів (теореми 1.1 та 1.2), композиції S та = зберігають еквітонність і повнототальність V-квазіарних функцій та предикатів (теорема 1.3).

В підрозділі наводяться основні властивості композицій R, x, x, S, = .

В підрозділі 1.5 вивчаються абстрактні та неокласичні алгебри.

Абстрактна алгебра - це пара A = (A, FA), де A - довільна множина (носій алгебри), а FA - довільна множина однозначних часткових функцій вигляду f : AA.

Виділивши 2-елементну множину Bool = {T, F}, приходимо до визначення абстрактної алгебраїчної системи (абстрактної АС) - пари вигляду A = (A, FnAPrA), де FnA - функції вигляду AA, PrA - функції вигляду ABool.

Визначаються гомоморфізми абстрактних алгебр та абстрактних АС, пропонується їх класифікація. Описуються найважливіші типи таких гомоморфізмів.

Далі визначаються абстрактні алгебри та алгебраїчні системи з доданою сигнатурою - Z-алгебри та Z-АС, для них задаються різні типи гомоморфізмів.

Композиційна предикатна система (VА, FnAPrА, C) визначає композиційну предикатну алгебру (FnAPrА, C) та алгебру (АС) даних (A, FnAPrA). Такі алгебри даних назвемо алгебраїчними системами з квазіарними функціями та предикатами, або неокласичними алгебрами (неокласичними АС).

Зв'язок алгебри даних і композиційної алгебри відбувається шляхом виділення та позначення в алгебрі даних базових функцій та предикатів, із яких за допомогою композицій будуються складніші. Виділяємо множини BF базових функцій, BP базових предикатів, множини Fs та Ps для їх позначення. Множину FsPs назвемо сигнатурою. Задаємо бієктивне I : FsPs BFBP. Таке I задає бієкції Fs BF та Ps BP.

При зафіксованому наборі базових композицій відображення I фактично прив'язує АС (A, FnAPrA) до мови сигнатури FsPs та перетворює її на об'єкт вигляду A = ((A, FnAPrA), I). Далі I продовжується до відображення J інтерпретації основних об'єктів мови (термів та формул) на множині FnAPrA. Пару ((A, FnAPrA), I) назвемо неокласичною алгеброю (неокласичною АС) з доданою сигнатурою.

АС з доданою сигнатурою є інтегрованими семантичними моделями, які пов'язують мову логіки відповідного рівня із неокласичними алгебрами даних.

Другий розділ дисертаційної роботи присвячений дослідженню композиційно-номінативних логік пропозиційного та реномінативного рівнів.

В підрозділі 2.1 описана композиційно-номінативна логіка пропозиційного рівня. Визначені семантичні моделі та мова пропозиційної логіки, наведені основні її семантичні властивості. Традиційна інтерпретація пропозиційних формул задається за допомогою істиннісних оцінок, це веде до поняття тавтології. Множина істинних формул пропозиційної логіки збігається з множиною тавтологій. Визначаються відношення тавтологiчного наслiдку |=t, тавтологiчної еквiвалентностi t , логічного наслiдку для множин формул, наводяться їх основні властивості.

В наступних підрозділах описана та досліджена композиційно-номінативна реномінативна логіка (РНЛ). Визначені семантичні моделі та мова, досліджені семантичні властивості РНЛ. Запропоновано нормальні форми для формул РНЛ Введено та досліджено поняття субтавтології. Субтавтології є істинними формулами РНЛ. Введено поняття системи розширень, доведена теорема про розширення.

Для РНЛ повнототальних еквітонних предикатів побудовано та досліджено формально-аксіоматичні системи гільбертівського типу - реномінативні неокласичні числення, для них доведено теореми коректності та повноти. Визначено та досліджено відношення логічного наслідку для множин формул. На цій основі будуються секвенційні числення РНЛ, для них доводяться теореми коректності та повноти.

В підрозділі 2.2 досліджуються семантичні властивості РНЛ. Семантичними моделями РНЛ є композиційні системи квазіарних предикатів (VA, PrA, C), де C задається базовими композиціями , , R. Алфавіт мови РНЛ складається із символів базових композицій, множини Ps предикатних символів (сигнатура мови), множини V предметних імен. Множина Fr формул мови визначається індуктивно.

1) Кожний предикатний символ (ПС) є формулою; такі формули атомарні.

2) Нехай та - формули. Тоді , Ф, - формули.

Позначимо nm() множину всіх предметних імен, які фігурують у символах реномінації формули , () - множину всіх предикатних символів формули .

Моделями мови РНЛ вважаємо АС з доданою сигнатурою ((A, PrA), I), які позначаємо (A, I). Вони пов'язують мову РНЛ із АС даних. Тотальне однозначне відображення I : Ps Pr визначає відображення інтерпретації формул J : FrPrA:

1) J(р) = I(p) для кожного рPs.

2) J() = (J()), J() = (J(), J()), J= R(J()).

Наведемо базові визначення, які формулюються однаково для логік кожного із номінативних рівнів. Предикат J() позначаємо A .

(частково) істинна при інтерпретації на A = (A, I), або A-неспростовна, якщо A - (частково) істинний предикат. Цей факт позначимо A |= .

усюди (частково) істинна, або неспростовна (це позначаємо |= ), якщо - A-неспростовна при інтерпретації на кожній моделі мови A.

виконувана при інтерпретації на A = (A, I), якщо A - виконуваний предикат.

Формула виконувана, якщо виконувана при інтерпретації на деякій A.

Ім'я xV строго неістотне для формули , якщо для кожної моделі мови A = (A, I) для довільних dVA та a, bA маємо A(dxa) = A(dxb) = A(d¦-х).

Ім'я xV неістотне для формули , якщо для кожної моделі мови A = (A, I) для довільних dVA та a, bA маємо A(dxa) A(dxb) та A(dxa) A(d¦-х).

Символом тут позначаємо слабку рівність (рівність з точністю до визначеності).

є логiчним наслiдком , що позначимо |= , якщо усюди істинна.

та логiчно еквiвалентнi, що позначимо , якщо |= та |= .

є слабким логiчним наслiдком , що позначимо ||= , якщо для кожної моделі мови A = (A, I) з умови A |= випливає A |= .

Формули та строго еквiвалентнi в моделі мови A, що позначимо ATF , якщо T(A) = T(A) та F(A) = F(A), тобто A та A - один і той же предикат.

Формули та логiчно строго еквiвалентнi, що позначимо TF , якщо ATF для кожної моделі мови A.

Множина формул є логічним наслідком множини формул в моделі мови A, що позначаємо |=А , якщо .

є логічним наслідком (позначаємо |= ), якщо |=А для всіх моделей мови A.

На рівень РНЛ переносяться поняття тавтології, відношень |=t та t .

Наводяться основні властивості відношень |=t , t, |=, ||=, , TF , |= .

Відмінність логік еквітонних та повнототальних еквітонних предикатів виявляється ще на пропозиційному рівні. Наводяться приклади, які заперечують modus ponens і засвідчують нетранзитивність еквіваленції для деяких семантичних моделей логіки еквітонних предикатів. Причина цього - нетранзитивність слабкої рівності.

Наведемо основні властивості формул, пов'язані з композицією реномінації.

RТ) RTF R() - згортка тотожної пари імен у реномінації.

R) R() TF R() - R -дистрибутивність.

R) R() TF R() R() - R-дистрибутивність.

RR) R(R()) TF R() - згортка реномінацій.

RSN) Нехай ім'я у строго неістотне для формули . Тоді R() TF R().

RN) Нехай ім'я у неістотне для формули . Тоді |= R() R().

RП) Якщо |= , то |= R().

Важливою для виконання еквівалентних перетворень формул є семантична теорема еквiвалентностi. Можна сформулювати дві різновидності цієї теореми.

Теорема 2.3. Нехай формула ' отримана з замiною деяких входжень формул 1,..., n на 1,..., n вiдповiдно. Якщо |= 11, ..., |= n n, то |= '.

Теорема 2.3S. Нехай формула ' отримана з заміною деяких входжень формул 1, ..., n на 1, ..., n вiдповiдно. Якщо 1 TF 1, ..., n TF n, то TF '.

Важливою властивістю, фактично індукованою еквітонністю композицій та вірною для загального випадку логіки квазіарних предикатів, є

Теорема 2.4 (про розширення). Нехай АС однієї сигнатури A = (А, IА) і В = (А, IВ) та формула такі, що для всіх р() та dVA з умови рA(d) випливає рВ(d) = рA(d). Тоді для довільного dVA з умови A(d) випливає В(d) = A(d).

Нехай A = (А, IА) і В = (А, IВ) - АС однієї сигнатури. В назвемо системою розширень для A, якщо для всіх рPs, dVA з умови рA(d) випливає рВ(d) = рA(d).

Наслідок 2.5. Нехай В = (А, IВ) - система розширень для АС A = (А, IА). Тоді для довільних формули та dVA з умови A(d) випливає В(d) = A(d).

Для кожної АС A із еквітонними предикатами можна збудувати систему повнототальних розширень В із еквітонними повнототальними предикатами.

Для формул РНЛ еквітонних предикатів встановлено (теорема 2.5) критерій неістотності предметних імен: xV неістотне для для кожного vV |= .

Далі в підрозділі вивчаються нормальні форми для формул РНЛ. Формула нормальна (знаходиться в нормальній формі), якщо всі символи реномінації у не мають тотожних перейменувань та застосовуються тільки до предикатних символів.

Використовуючи R, R, RR та RТ, для кожної формули будується нормальна формула така, що |= . Така названа нормалізантою формули .

Формула - субтавтологія, якщо її нормалізанта - тавтологія.

Субтавтології є істинними формулами РНЛ: - субтавтологія |= .

Аналогом теореми еквівалентності для множин формул є теорема заміни еквівалентних. Для логіки еквітонних предикатів ця теорема формулюється так:

Теорема 2.9. Нехай . Тоді: , |= , |= та |= , |= , .

Для загального випадку квазіарних предикатів теорема формулюється так:

Теорема 2.9S. Нехай TF . Тоді: , |= , |= та |= , |= , .

В підрозділі 2.3 для РНЛ повнототальних еквітонних предикатів запропоновано та досліджено формально-аксіоматичні системи гільбертівського типу - реномінативні неокласичні числення. Розглядаються приклади виведень в цих численнях. Для них доводяться синтаксичні варіанти семантичних тверджень підрозділу 2.2, формулюється і доводиться теорема дедукції (теорема 2.14).

Для реномінативних числень доведені їх коректність та повнота:

Теорема 2.15. Для кожного реномінативного числення T маємо T |- T |= .

Наслідком теореми повноти є розв'язність реномінативних числень (теорема 2.16).

В підрозділі 2.4 для РНЛ збудовано формально-аксіоматичні системи ґенценівського типу. Секвенції трактуються як множини специфікованих спеціальними символами |- та -| формул в стилі запису семантичних таблиць Бета.

Для побудованих RBN-числень справджуються:

Теорема 2.18 (коректності). Нехай секвенція |--| вивідна. Тоді |= .

Теорема 2.19 (повноти). Нехай |= . Тоді секвенція |--| вивідна.

В третьому розділі досліджуються першопорядкові логіки квазіарних предикатів. Низка доведених в розділі теорем узагальнюють відповідні теореми класичної логіки.

Визначено мови та досліджено семантичні властивості першопорядкових логік відповідного рівня. Запропоновано та досліджено нормальні форми для формул таких логік. Вивчені питання, пов'язані з неістотністю предметних імен. Досліджено властивості відношення логічного наслідку для множин формул логік відповідного рівня.

Введено поняття гомоморфізму та ізоморфізму для неокласичних алгебраїчних систем із доданою сигнатурою, визначено різновидності гомоморфізмів. Для логік еквітонних предикатів доведено теореми про гомоморфізми та ізоморфізми. Такі теореми є узагальненням відповідних теорем класичної логіки предикатів.

Запропоновано та досліджено розширення логік еквітонних предикатів. Це логіки локально-еквітонних, еквісумісних і локально-еквісумісних предикатів. Властивості цих логік в цілому аналогічні відповідним властивостям логіки еквітонних предикатів, вони зберігають основні закони класичної логіки, тому їх відносимо до неокласичних. Водночас такі логіки мають істотно ширші класи семантичних моделей.

В підрозділі 3.1 вивчаються логіки кванторного рівня, або чисті композиційно-номінативні логіки. Семантичними моделями ЧКНЛ є композиційні системи квазіарних предикатів кванторного рівня (VA, PrA, C), де C задається базовими композиціями , , R, x. Алфавіт мови ЧКНЛ складається із символів базових композицій, множини Ps предикатних символів (сигнатура мови), множини V предметних імен. Множина Fr формул мови ЧКНЛ визначається індуктивно.

1) Кожний предикатний символ є формулою; такі формули атомарні.

2) Нехай та - формули. Тоді , Ф, , x - формули.

Моделями мови ЧКНЛ вважаємо АС з доданою сигнатурою ((A, PrA), I). Вони пов'язують мову ЧКНЛ із АС даних. Тотальне однозначне відображення I : Ps Pr природним чином визначає відображення інтерпретації формул J : FrPrA:

1) J(р) = I(p) для кожного рPs.

2) J() = (J()), J() = (J(), J()), J= R(J()), J(x) = x(J()).

Для логік квазіарних предикатів наводяться пов'язані з кванторами властивості, подібні до відповідних властивостей класичної логіки. Водночас для загального випадку логік квазіарних предикатів не завжди справджуються властивості |=x, x ||= , |= x; існують формули , для яких |= x та | x.

З іншого боку, для логік еквітонних предикатів (як і для для класичної логіки) маємо властивості, які невірні для загального випадку логіки квазіарних предикатів:

- |= x, |= x, x ||= , |= x |=;

- |= x |= x |= x |= x;

Для ЧКНЛ справджуються теореми еквiвалентностi та заміни еквівалентних, теорема 2.4 про розширення:

Для формул мови ЧКНЛ вводяться поняття вільного та зв'язаного входження нижнього імені символа реномінації, квазівільних імен, квазізамкненої формули.

Квазізамкнені формули є синтаксичними аналогами замкнених формул класичної логіки предикатів, проте семантичними аналогами таких формул їх вважати не можна. Справа в тому, що до складу формули можуть входити предикатні символи, для яких множини істотних імен нескінченні. Для логіки квазіарних предикатів квазізамкнені формули необов'язково інтерпретуються як константні предикати.

...