Диссертация (Автоматический логический вывод в интуиционистских логических исчислениях обратным методом Маслова), страница 10

Вхождение40В работах С. Ю. Маслова, С. К. Клини и Г. Е. Минца нет термина «полярность», однако введение такоготермина представляется удобным.50является положительным, если формула F не содержит вхождений такихподформул видаиливхождений.(различных), чтоВ, или содержит четное число такихпротивномслучаевхождениеявляетсяотрицательным41. Аналогично определяется полярность вхождений логическихсимволов (связок и кванторов).Например, формулавхождение подформулысодержит одно (отрицательное)и два вхождения подформулы, первое изкоторых — отрицательное, а второе — положительное.Будем использовать символьное обозначение полярности вхождений связоки кванторов в формулу, как в статье [39]. Пусть символсимволов , ,,,и .

Вхождение символавхождением типа(типаобозначает любой изв формулубудем называть), если оно является положительным(соответственно отрицательным) вхождением в формулу .2.2.4. Секвенции и секвенциальные исчисленияСеквенция — это формальное выражение вида(2.1)где,аи— конечные мультимножества формул.Левая часть секвенции (т. е.правая часть секвенции (т. е.Секвенциивида:) называется ее антецедентом, а) называется ее сукцедентом.вида (2.1) содержательно соответствует формула следующего.

Эту формулу, следуя [10], будемназывать формульным образом секвенциии обозначать.Символу выводимости « » назначается наивысший ранг по сравнению совсеми логическими операциями, т. е. он всегда имеет наиболее широкую областьдействия (см. соглашения в параграфе 1.2, позволяющие опускать скобки).41Другими словами, вхождение подформулы называется положительным (отрицательным), если онорасположено в области действия четного (соответственно нечетного) числа различных отрицаний и посылокимпликаций. Такое определение фигурирует в книге [14, с. 151].51Формула F входит в секвенцию S вида (2.1) (или принадлежит этойсеквенции), если F совпадает с одной из формулили.Аналогично для формул, входящих в антецедент (сукцедент) секвенции.Секвенция S содержит формулу F, если F входит в S.Пустьиподсеквенцией(пишетсяЗамкнутая— секвенции.), еслиисеквенция — секвенция,называется.содержащаятолькозамкнутыеформулы.Очищенная секвенция — такая секвенция, формульный образ которойпредставляет собой очищенную формулу.Секвенции вида (2.1), содержащие не более одной формулы в сукцеденте(когда), будем называть сингулярными.

Если же, то секвенцияназывается мультиплярной.Секвенциальноеисчисление — логическоеисчисление,выводимымиобъектами в котором являются секвенции.Односукцедентное исчисление — секвенциальное исчисление, в которомвыводимы только сингулярные секвенции. В многосукцедентном исчислениивыводимые секвенции могут содержать более одной формулы в сукцеденте.Свойствоподформульностидлясеквенциальныхисчисленийформулируется следующим образом: в выводе произвольной секвенции S каждаяформула, входящая в какую-либо секвенцию из этого вывода, являетсяподформулой некоторой формулы, входящей в S.Рассмотрим правило введения символав сукцедент из классическогоисчисления С. К. Клини G1 [13, с.

391]:В конкретном применении этого правила (в выводе по этому правилу)секвенция, стоящая над чертой, называется посылкой рассматриваемогоприменения правила, а секвенция под чертой называется его заключением. Явноуказанные формулыив посылке называются боковыми формулами, формула52из заключения называется главной формулой, а формулы, входящие в— параметрическимиформулами.Аналогичнодляправиливыводапроизвольного секвенциального исчисления.Теперь рассмотрим правила введения квантора существования в антецеденти квантора всеобщности в сукцедент из того же исчисления G1:Переменнаяназывается собственной переменной (применений) этихправил и должна удовлетворять так называемому ограничению на собственнуюпеременную42:свободна дляви не входит свободно в заключение. Оприроде этого ограничения см.

в § 18 книги [14].Вышеприведенные термины, определенные на примере исчисления G1, мыбудем использовать для всех рассматриваемых в работе исчислений, содержащиханалогичные ограничения на собственные переменные.Пусть— исчисление с ограничениями на собственные переменные(обозначим соответствующие правила введения кванторов какСобственными переменными выводапеременныелюбых применений правилВывод в исчислениив исчисленииии).будем называть, входящих в .обладает свойством чистоты переменных, еслиникакая переменная не входит в него одновременно свободно и связанно, и длякаждого применения правилаилисобственная переменнаяэтогоприменения входит лишь в секвенции, расположенные выше заключения. Еслипри этом соответствующий квантор является вырожденным, то переменнуювсегда можно выбрать так, чтобы она удовлетворяла этому условию [13, с. 399].В ряде доказательств мы будем пользоваться тем, что в выводе очищеннойсеквенции можно всегда переименовать переменные так, чтобы полученныйвывод обладал свойством чистоты переменных.

Для рассматриваемых в работе42В англоязычных источниках употребляется термин «eigenvariable condition».53исчислений это можно обосновать с помощью тех же рассуждений, что и вдоказательствах лемм 37 и 38 из § 78 книги [13].Логическими правилами секвенциального исчисления называются правилавведения логических символов в антецедент и сукцедент (например, упомянутоевыше правило введенияв сукцедент). Кроме того, секвенциальные исчислениямогут содержать специальные структурные правила.

Например, правилоутончения в сукцеденте для исчисления G1 выглядит следующим образом:а правило сокращения в антецеденте выглядит так:2.2.5. Специальные термины для исчислений обратного метода сунификацией: –атомы, –формулы и –секвенцииСоглашение 2.1. В дальнейшем изложении (если явно не указано иное)обозначает замкнутую очищенную формулу логики первого порядка, которая несодержитвырожденныхкванторовпропозициональные связки , , ,ивкоторуювходяттолькои символы кванторов , .Как отмечено в работе [68], произвольную замкнутую формулу логикипервого порядка можно привести к очищенному виду с помощью переименованиясвязанных переменных.

Вырожденные кванторы из формулы можно удалить.Также в произвольной формуле можно устранитьследующих стандартных определений:где— некоторый пропозициональный атом.,ис использованием54Определяемые ниже понятия зависят от конкретной формулы , поэтому вназваниях терминов явно указан символ . Таким образом, используется стильнаименования терминов, характерный для работ С. Ю. Маслова.–атом — это вхождение атомарной подформулы в .–секвенция43 — это секвенция специального вида:(2.2)где— отрицательныевхожденияподформул44— положительные вхождения подформул вв;и;— подстановки произвольных термов вместо переменных (термымогутсодержатьпредметныеконстантыформальным выражениям видавидаифункциональныесимволы);содержательно соответствуют формулы.Сами выражения вида, где— вхождение подформулы в , аподстановка термов вместо переменных, будем называтьэтомантецедентисукцедент–секвенции—–формулами.

Припредставляютсобоймультимножества45 –формул.Обычно в записи видаформулумы не будем заключать в скобки.При этом в терминах соглашений из параграфа 1.2 ранг операции « » выше рангавсех логических операций, но ниже ранга символа выводимости « ».43В статье [44] термину « –секвенция» соответствует термин «секвенция с подстановками». Первый изтерминов представляется более удачным, так как в его названии явно фигурирует формула , от которой зависитопределение секвенции.44В статьях [44] и [116] вместо понятия вхождения подформулы использовалось понятие свободнойподформулы, как в [68]. Однако впоследствии выяснилось, что изложение в терминах вхождений подформулявляется более корректным, а также позволяет избежать ряда типичных ошибок. Для наглядности поясним, чтопри программной реализации вхождение подформулы можно интерпретировать как объект, в котором вместе ссамой подформулой хранится информация о том месте, где эта подформула входит в формулу .45Как и в работе [68], использование в секвенциях мультимножеств вместо обычных множествобусловлено техническими соображениями: это позволяет упростить некоторые доказательства (например,доказательство леммы 2.15 и доказательство полноты стратегии поглощения).55В дальнейшем термин «секвенция» может использоваться вместо термина« –секвенция», если тип секвенции понятен из контекста.— –секвенцияПусть–секвенциипеременныхвида(2.2).Тогдамножество, обозначаемое каксвободных— это множество.Аналогичным образом определяется множество переменных –секвенции, обозначаемоеЕсли.обозначает –секвенцию— подстановка, допустимая для , то.Такие же обозначения действуют и для мультимножеств –формул.Примером –секвенциибудемназывать любую секвенцию, гдеподстановка, допустимая для .

Если при этом, топримером –секвенции . Фактически –секвенция—называется основными ее основной примерявляются двумя формами записи одной и той же секвенции.Пусть— –секвенции, а секвенцииисоответственно.подсеквенциейназывается подсеквенциейи— основные примеры), если(иявляется.Остальные определения из пункта 2.2.4 аналогичным образом переносятсяна случай –секвенций.Записьполучается изобозначает нормальную форму–секвенции, котораясужением областей определения всех входящих в нееподстановок: каждая –формула–формулазаменяется –формулойназывается правильной, если.и.–секвенцияназывается правильной, если каждая входящая в нее–формула является правильной.56Будем говорить, что формулавыводима в секвенциальном исчислении ,если в этом исчислении выводима секвенцияметода с унификацией — –секвенция(а для исчислений обратного).2.3. Универсальная методика построения логических исчислений,подходящих для применения обратного методаВ работе [68] для построения исчислений обратного метода предлагаетсяиспользовать «универсальный рецепт» автоматического логического вывода, идеикоторого прослеживаются еще в работах С.