Навигация
Если a есть вывод из последовательности посылок G,A и ^ есть его последняя формула, то
33981
знак
2
таблицы
0
изображений
7. Если a есть вывод из последовательности посылок G,A и ^ есть его последняя формула, то
есть вывод из посылок G и ØA есть его последняя формула.
Чтобы определение вывода NeC было полным необходимо сформулировать прямые правила вывода. Прежде всего есть правило тождественного перехода: из A выводима A, обозначим его буквой I. Остальные правила вывода подразделяются на правила введения и удаления логических констант. В приводимой ниже таблице правил вывода мы для полноты записываем и непрямые правила (хотя они сформулированы в определении вывода).
Кроме основных будем использовать в качестве официальных также два производных правила Éе1 и Éi2:
и 
Теперь перейдем к процедуре писка вывода. Поиск начинается с формулировки задачи: из посылок A1,...,An требуется вывести формулу В. Мы исходим из допущения, что ни посылки, ни заключение не содержат e-символов и предиката существования. Не нарушая общности можно также допустить, что они не содержат свободных переменных. Задача поиска вывода записывается в виде
Это, естественно, не вывод. Построение ( поиск ) вывода совершается с помощью двух типов шагов: синтетических и аналитических. Синтетический шаг состоит в применении некоторого прямого правила вывода. Аналитический шаг сводит задачу к подзадачам.
Сформулируем аналитические и синтетические правила поиска вывода для импликации. Задача вывода формулы AÉB из некоторой последовательности посылок сводится к подзадаче построения вывода формулы B из того же множества посылок и дополнительного допущения A. Это аналитическое правило введения импликации. Мы его запишем в виде
где n наибольший номер в первоначальной задаче. В анализе указаны официальные правила вывода (не правила поиска вывода). Аналитическое правило удаления импликации состоит в сведении задачи вывода формулы C из формулы AÉB, стоящей выше знака выводимости, к двум подзадачам: выводу формулы A из прежних посылок и выводу формулы C из прежних посылок и формулы B. Символически
Синтетическое правило удаления импликации разрешает написатьвыше знака выводимости формулу B, если формулы A и AÉB входят в фигуру заключения выше знака выводимости:
Для симметрии можно сформулировать и синтетическое правило введения импликации: если в фигуру выше знака выводимости входит формула A, то непосредственно над знаком выводимости можно написать формулу BÉA. Однако формулу B надо указать дополнительно. Символически
Если в фигуру поиска вывода выше знака выводимости входит формула A и A стоит ниже знака выводимости, то знак выводимости выбрасывается - это правило исключения знака выводимости
Если A стоит непосредственно над |-, то нижнее вхождение A и знак выводимости опускаются.
Специфически интуиционистскими являются аналитические правила удаления импликации, введение дизъюнкции, правило добавления заключения (вместо классического аналитического правила удаления отрицания), а также правила для кванторов и, естественно, правило для предиката существования. При формулировке кванторных правил используются временные переменные, e -термы и свободные переменные. К сожалению, мы не можем обойтись без свободных переменных и сформулировать правило введения квантора общности в виде
если A(exùA(x)), то "xA(x).
Помимо перечисленных в таблице правил поиска вывода, имеются также два правила удаления знака ú-:
,
правило введения произвольной формулы
и, наконец, правило глобальной подстановки вместо временных переменных термов: во всем дереве поиска вывода разрешается заменить все вхождения временной переменной на терм.
В отличие от классической логики интуиционистские правила не обратимы. Поэтому не безразличен порядок применения правил поиска вывода. Например, пусть требуется из AÚB вывести BÚA. Если мы начнем решать задачу, применив сначала аналитическое правило введения дизъюнкции, то мы придем в тупик и не решим решаемую задачу. Однако задача последовательности применения правил поиска вывода решаема. По существу система аналитических правил есть иная формулировка логистического секвенциального исчисления. С.К. Клини [2] исследовал проблему перестановочности применений логических правил для интуиционистской логики. Опираясь на его результаты, мы можем разбить правила на следующие группы:
1.Правила удаления |- ;
2.Синтетические правила и аналитические правила введения конъюнкции, импликации, отрицания, квантора общности, аналитическое правило удаления дизъюнкции;
3.Аналитическое правило введения квантора существования;
4.Аналитические правила удаления импликации и отрицания;
5.Аналитическое правило введения дизъюнкции;
6.Правило введения произвольной формулы.
В каждом вспомогательном выводе отдается предпочтение правилам группы с меньшим номером. Если порядок применения правил нарушается, то поиск вывода может не дать искомого результата.
В отличие от классической логики, для поиска выводов в которой имеется одна фигура, в предложенной системе поиска для интуиционистской логики имеется правила “или”-ветвления. Это требует разработки новых программных средств по сравнению с классической логикой
ЛИТЕРАТУРА:1. Асмус В. Ф. Проблема интуиции в философии и математике. — М.: Мысль, 1965.
2. Новиков П. С. Элементы математической логики. — М.: Государственное издательство физико-математической литературы, 1959.
3. Овчаров А. А. Интуиция в модальной логике. — Кемерово: Кузбассвузиздат, 1997.
4. Овчаров А. А. Введение в идеал-реалистическую теорию интуицию. Логика социальных изоморфов. — Кемерово: Кузбассвузиздат, 1999.
5. Целищев В. В., Карпович В. Н., Поляков И. В. Логика и язык научной теории. — Новосибирск: Наука, 1982.
Похожие работы
... эти формулы равносильны на поле M. Если две формулы равносильны на любых полях M, то мы будем их называть просто равносильными. Нормальную формулу, равносильную некоторой формуле U, мы будем называть нормальной формой формулы U. §1. Логика предикатов с одним переменным Мы будем рассматривать формулы логики предикатов, содержащие предикаты, которые зависят только от одного переменного. ...
... которых утверждается или отрицается нечто о явлениях действительности. Повествовательные предложения по своему логическому значению выражают истину либо ложь. Алфавит языка логики предикатов отражает семантические категории естественного языка и включает следующие виды знаков (символов): 1) a, b, c, … - символы для единичных имен предметов; их называют предметными постоянными (константами); 2) ...
... , которые используются при доказательстве теорем вручную, системы автоматического доказательства для фразовых форм используют единственное правило вывода — принцип резолюций, — впервые описанное Робинсоном ([Robinson, 1965]). Рассмотрим следующий пример из исчисления высказываний. В дальнейшем прописными буквами Р, Q, R,... будут обозначаться отдельные фразы, а строчными греческими U, ф и £ ...
... и отрицательное по качеству. Частноутвердительное суждение — суждение, частное по количеству и утвердительное по качеству. Частноотрцательное суждение — суждение, частное по количеству и отрицательное по качеству. В логике принято сокращенное обозначение суждений по их объединенной классификации. Cуждения обозначаются следующими буквами: А — общеутвердительное, Е — общеотрицательное, I — ...
0 комментариев