Учебные материалы по информатике

О.В. Новиков

В современной теории определимости выделяют две основополагающие идеи: установление равнообъемности синтаксического и семантического понятий определимости для первопорядковых языков и теорий и идея о тесной взаимосвязи между определимостью и выводимостью. Это позволяет свести ряд важных проблем определимости к стандартным проблемам теории логического вывода. В этом отношении исключительно важным достижением явилось установление Крейгом интерполяционной теоремы, из которой легко выводится теорема Бета о преобразовании неявных определений в явные, имеющая широкие приложения в логике и методологии науки. Это дает возможность свести вопрос о существовании (поиске) определяющей формулы а к вопросу о существовании (поиске) вывода без α: по доказательству теоремы Бета и теоремы Крейга можно сформулировать алгоритм, дающий по доказательству ∀x(Px~ P1x) в E ⋃E1 определяющую формулу α .

Нами проведены два доказательства интерполяционной теоремы (для классического и интуиционистского исчислений), в которых реализованы две различные поисковые идеологии, позволяющие находить определяющую формулу способами, достаточно эффективными для компьютерной реализации. Для проведения первого доказательства формулируется классическое первопорядковое секвенциальное исчисление, такое, что предки формул антецедента (сукцедента) некоторой фигуры заключения находятся только в антецеденте (сукцеденте) посылок. Это достигается прежде всего отказом от фигур для отрицания (вместо этого для каждого логического знака сформулированы левая и правая фигуры «в чистом виде» и под знаком отрицания). Такого ряда формулировка позволяет свести все фигуры заключения в четыре группы, для каждой из которых (а также для пяти основных секвенций) ввести и обосновать весьма простые интерполяционные правила. Имея доказательства А → В и применяя интерполяционные правила на каждом шаге от аксиом к заключению, находим интерполяционную формулу X. Как частный случай такого поиска находится определяющая формула а , она и есть интерполяционная формула для Е1 Рх → Е 1 ⊃ Р1х.

Второе доказательство проводится в стандартном сформулированном интуиционистском секвенциальном исчислении G генценовского типа. Идеология поиска (разработана Клини для классического исчисления) такова. Если дано доказательство секвенции Е → F в G, то мы можем разбить его вертикально на две части. Мы получим E-часть, вычеркивая из каждой секвенции все предки вхождения F в конечную секвенцию, и F-часть, вычеркивая все предки Е. Разумеется, в общем случае ни E-часть, ни F-часть не будут доказательствами. Но можно исправить обе части или одну из них, превратив их в доказательства и используя при этом некоторые существенные черты их строения. Эти исправления делаются путем восстановления минимума из того, что было отсечено от этой части во время операции разбиения и не может не быть сохранено для доказательства и удаления одновременно того, что оказывается лишним в отсутствие другой части. Ключ к тому, что необходимо для восстановления F-части или E-части до F-доказательства или E-доказательства, дается рассмотрением поведения аксиом из данного доказательства во время операции разбиения. Далее формулируются аналоги интерполяционных правил для каждой фигуры заключения. При исправлении Е-части и F-части или одной из них мы работаем шаг за шагом соответственно секвенциям, которые встречаются при спуске вниз по данному доказательству Е → F в G, и «собираем» интерполяционную формулу из восстановленных аксиом в соответствии с «интерполяционными» правилами.

В двух предлагаемых доказательствах находят реализацию различные поисковые идеологии. Первая состоит в усложнении исчисления для простоты формулировки и применения поисковых правил. Вторая — в усложнении самой поисковой процедуры для возможности работы в стандартном исчислении. Эффективность каждой идеологии зависит от прикладного характера той или иной компьютерной реализации, использующей возможность «автоматизировать» поиск определяющей формулы   

Вестник Московского университета