Логика предикатов

СОДЕРЖАНИЕ Введение . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .3 Основные понятия . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .4 § 1. Логика предикатов с одним пе ременным . . . . . . . . . . . . . . . . . . . . . . . . . . . .5 § 2. Практика по решению проблемы разрешимости формул , содержащих предикаты от одного переменного . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .9 § 3. Поиск доказат ельств в натуральном интуиционистском исчислении предикатов с -символом и предикатом существования . . . . . . . . . . . . . . . . . . . .11 Литература . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .17 ВВЕДЕНИЕ Проблема разрешимости — эта проблема ставится для формул исчисления предик а тов , лишённых символов постоянных предметов и символов индивидуальных предикатов. В последующ ем изложении предполагается , что рассматриваемые формулы таковы (если не сделано специальных оговорок ). Каждая такая формула представляет собой определённое утверждение , истинное или ложное , когда оно относится к определённому полю M . Если такая формула ис тинна для некоторого поля M и некоторых предикатов , на нём определённых , мы будем называть её выполнимой. Если формула истинна для данного поля M и для всех предикатов , определённых на M , мы будем называть её тождественно истинной для поля M . Если формула истинна для всякого поля M и для всяких предикатов , будем называть её тождественно истинной или просто истинной. Формула называется ложной или невыполнимой , если ни для какого поля ни при к а ких замещениях предикатов она не является истинной . Легко показать , что если формула U тождественно истинна , то формула ложна , и наоборот . Постановка проблемы разрешимости для логики предикатов аналогична постановке этой п роблемы для алгебры высказываний . Её решение и является целью данной курсовой работы . Итак , проблема ставится следующим образом : дать эффективный способ для определения — является ли данная формула выполнимой или нет. Умея решать вопрос о выполнимости , мы тем самым сможем решать и вопрос об и с тинности любой формулы . В самом деле , если формула U истинна , то формула нев ы полнима , и обратно . Поэтому , доказав выполн имость или невыполнимость , мы тем с а мым проверим истинность U . Проблема разрешимости для логики предикатов является усилением проблемы разрешимости для исчис ления высказываний , так как все формулы исчисления высказываний входят в число формул логики предикатов . Однако в то время как решение проблемы разрешимости для исчисления высказываний никаких трудностей не представляет , проблема разрешимости для логики п р едикатов оказалась связанной с с е рьёзными трудностями. Современные исследования пролили свет на природу этих затруднений . В настоящее время представляется достаточно ясным , что решение этой проблемы в указанном смысле вообще невозможно . Иначе говоря , не мо жет существовать никакого конструктивного пр а вила , которое позволяло бы определять для любой формулы логики предикатов , является ли она тождественно истинной или нет . Для некоторых частных типов формул , однако , проблема разрешимости решается . Мы рассмотрим наиболее важный тип формул , для к о торых решение проблемы разрешимости может быть осуществлено , это формулы логики предикатов , зависящие от одного переменного. Основные понятия Пусть M - некоторое множество предметов и a , b , c , d - какие-то определённые предметы из этого множества . Тогда высказывания об этих предметах мы бу дем обозначать в виде P ( a ) , Q ( b ) , R ( c , d ) и т . д . P(a) обозначает высказывание о предмете a , Q(b) - высказывание о предмете b , R(c, d) - высказывание о предметах c и d и т.д. Такие высказывания могут быть как истинны , так и ложны , обозначаемые соотве т стве нно символами И и Л . Эти значения ставятся в соответствие определённым предметам или группам предметов. Пусть M - произвольное непустое множество , а x представляет собой произвольный предмет из этого множества . Тогда выражение F(x) обозначает высказывание, которое ст а новится определённым , когда x замещено определённым предметом из M . F(a) , F(b) , ... уже представляют собой вполне определённые высказывания . Например , если M натуральный ряд , то F(x) может обозначать : " x есть простое число ". Это неопределённое высказывание становится определённым , если x заменить нек о торым числом , например : "3 простое число ", "4 простое число " и т . д. Пусть S(x,y) обозначает : " x меньше y ". Это высказывание становится определённым , если x и y заменить числами : "1 мен ь ше 3", "5 меньше 2" и т . д. Так как с нашей точки зрения каждое определённое высказывание представляет с о бой И или Л , то выражение F(x) означает , что каждому предмету из M поставлен в соотве т ствие один из двух символов И или Л . Иначе говоря , F(x) представляет собой функцию , определённую на множестве M и принимающую только два значения И и Л . Таким же о б разом неопределённое высказывание о двух и более предметах H(x, y) , G(x, y, z) и т . д . предвтавляет собой функцию двух , трёх и т . д . переменных . При этом переменные x , y , z пробегают множество M , а функция принимает значения И и Л . Эти неопределённые в ы сказывания , или функции одного или нескольких переменных , мы будем называть логич е скими функциями или предикатами. Предикатом с одним переменным можно выразить свойство п редмета , например " x есть простое число ", " x - прямоугольный треугольник " и т.д. Все понятия , которые мы будем вводить , относятся всегда к некоторому произвол ь ному множеству M , которое мы будем называть полем . Элементы этого поля будем обозн а чать малыми латинскими буквами (иногда эти буквы мы будем снабжать индексами ). Бу к вы конца латинского алфавита x , y , z , u , v , x 1 , x 2 , ... обозначают неопределённые предметы поля . Их мы будем называть предметными переменными . Буквы начала алфавита a, b, c, a 1 , a 2 , ... обозначают определённые предметы поля . Их мы будем называть индивидуальными предметами или предметными постоянными . Большими латинскими буквами A , B , ..., X , A 1 , A 2 , ... мы будем обозначать переменные , принимающие значения И и Л . Их мы назовём переменными высказываниями . Мы будем также рассматривать и постоянные высказыв а ния . Их мы будем также обозначать большими латинскими буквами , как-нибудь отмече н ными или просто с дополнительной оговоркой. Большие латинские буквы и символы предикатов как индивидуальных предметов , так и от предметных переменных мы будем называть элементарными формулами . Мы будем говорить , что в формулах ( х ) U (х ) и ( х ) U (х ) кванторы ( х ) и ( х ) относятся к переменному х или что переменное х связано соо т ветствующим квантором. Предметное переменное , не связанное никаким квантором , мы будем называть св о бодным переменным. Формулы , в которых из операций алгебры высказываний име ются только операции , и , а знаки отрицания относятся только к элементарным предикатам и высказыв а ниям , будем называть приведёнными формулами. Приведённая формула называется нормальной , если она не содержит кванторов или если при образовании её из элементарных формул операции связывания квантором следуют за всеми операциями алгебры высказываний. Если две формулы U и B , отнесённые к некоторому полю M , при всех замещениях переменных предикатов , пер еменных высказываний и свободных предметных переменных соответственно индивидуальными предикатами , определёнными на M , индивидуальными высказываниями и индивидуальными предметами из M , принимают одинаковые значения И или Л , то мы будем говорить , что эти фо рмулы равносильны на поле M . Если две формулы равносильны на любых полях M , то мы будем их называть пр о сто равносильными . Нормальную формулу , равносильную некоторой формуле U , мы будем называть нормальной формой формулы U . § 1. Л огика предикатов с одним п еременным Мы будем рассматривать формулы логики предикатов , содержащие предикаты , к о торые зависят только от одного переменного . Логика , в которой употребляются только т а кие выражения , соответствует той , которая описана Аристотелем и вошла как традицио н ный элемент в систему гуманитарного образования . Известные формы высказываний этой логики и формы умозаключений , так называемые «модусы силлогизмов» , выражаются по л ностью в символике логики предикатов от одного переменного. Теорема . Если формула логики преди катов , содержащая только предикаты от одного переменного , выполнима на некотором поле M , то она выполнима на поле , содержащем не более элементов , где n - число предикатов , входящих в рассматрива е мую формулу. Пусть формула U (A 1 , ..., A n ), содержащая только символы предикатов A 1 , ..., A n , каждый из которых зависит от одного переменного , выполнима на некотором поле M . эту формулу мы можем предполагать представленной в нормальной форме , а все предметные переменные в ней связанными . В самом деле , какова бы ни была формула U , мы можем , произведя над ней преобразования , привести е ё к виду , в котором все кванторы предш е ствуют остальным символам формулы , при этом состав её предикатов и предметных пер е менных не изменяется . Если в U есть свободные предметные переменные , то можно связать их квантором общности. Итак , допустим , что U – но рмальная формула . Тогда мы можем представить её сл е дующим образом : ( x 1 )( x 2 )...( x p ) B ( A 1 , ..., A n , x 1 , ..., x p ), где каждый из символов ( x i ) обозначает квантор ( x i ) или ( x i ), а формула B ( A 1 , ..., A n , x 1 , ..., x p ) кванторов не содержит. В формуле B ( A 1 , ..., A n , x 1 , ..., x p ) все переменные x 1 , ..., x p входят в предикаты A 1 , ..., A n , и её можно записать в виде B ( A 1 ( ), ..., A n ( )), где i 1 , ..., i n – числа от 1 до p . Однако , будет удобнее пользоваться выражением B ( A 1 , ..., A n , x 1 , ..., x p ), если иметь в виду , что B является логической функцией предикатов A k , а каждый предикат A k зависит от какого-то одного переменного . Покажем , что если для некоторого поля M существуют индивидуальные предикаты ,..., , для которых формула U ( ,..., ) истинна , то эта формула истинна и на некотором подмножестве этого поля , содержащем не более элементов , так как иначе наше утве р ждение тривиально . Разобьём эл ементы множества M на классы следующим образом . Для каждой последовательности , содержащей n символов И и Л в произвольном порядке ( И , Л , Л , ..., И ,), существует часть (может быть , пустая ) множества M , содержащая те и только те элементы x , для которых после довательность значений предикатов ( x ), ( x ), ..., ( x ) совпадает с данной последовательностью символов И и Л . Обозначим через 1 , 2 , ..., n последовател ьность символов И и Л , где i представляет собой И или Л , а соотве т ствующий этой последовательности класс элементов x обозначим , , ..., . Некоторые из эти х классов могут оказаться пусты , так как может случиться , что для некоторой последовательности 1 , 2 , ..., n не существует такого элемента , для которого предикаты , , ..., принимают соответствующие значения 1 , 2 , ..., n . Вместе с тем к аждый элемент множества M принадлежит одному из классов , и различные классы общих элементов не имеют . Число всех классов (пустых и непустых ) равно числу послед о вательн остей 1 , 2 , ..., n , т . е . . Следовательно , число q непустых классов не пр е вышает . Выберем из каждого непустого класса по одному элементу и обозначим эти элементы a 1 , a 2 , ..., a q . М ножество всех этих элементов обозначим .докажем , что если формула U ( , .. ., ) истинна на поле M , то она истинна и на поле (так как – часть поля M , то предикаты определены на ). каждому элементу x поля M поставим в соответствие элемент из , принадлежащий тому же классу , чт о и х . В существует один и только один такой элемент . Элемент из , поставленный в соответствие х , обозначим ( х ). Можно сказать , что мы построили функцию , определённую на множестве M и принима ю щую значения из множества . Легко видеть , что имеет место следующая равносильность : ( х ) ( ( х )). Действительно , ( x ) принадлежит тому же классу , что и x . Н о , по определению , для элементов одного и того же класса каждый предикат принимает одно и то же знач е ние . Отсюда следует , что если в формуле U ( , ..., ) для каждого предметного переме н ного t заменить каждое выражение ( t ) через ( ( х )), то формула U ( , ..., ) пере й дёт в формулу ( , ..., ), равносильную первой . Написание формулы отличается от U только тем , что все предметные переменные x, y, z, … , u формулы U замещены соо т ветственно через ( х ), ( y ), ..., ( u ). Это следует из того , что по условию формула U ( , ..., ) содержит только предикаты , и поэтому всякое предметное переменное входит только под знаком одного из этих предикатов. Пусть R ( x, y, ..., u ) – предикат , определённый на поле M . Введём обозначение R ( x, y, ..., u ). Под этим выражением мы будем понимать предикат , зависящий от y, z, ..., u (или высказывание , если , y, z, ..., u отсутствуют ) и принимающий значение И , когда R ( y, z, ..., u ) имеет значение И для данных y, z, ..., u и для всех x , принадлежащих полю , и прин и мающий значение Л в противоположном случае . Введём также выражение R ( x, y, ..., u ), которое представляет собой предикат от y, ..., u и принимает значение И , когда R ( x, y, ..., u ) имеет значение И для y, ..., u и по крайней мере для одного значения x из поля , и значение Л в противоположном случае . Знаки и будем называть ограниченными кванторами . Если мы все переменные предиката R ( x, y, ..., u ) свяжем ограниченными ква н торами , например ... R ( x, y, ..., u ), то получим формулу , отнесённую к полю . покажем , что выражение ( x ) R ( ( х ) , y, ..., u ) равносильно выражению R ( x, y, ..., u ). Пусть ( x ) R ( ( х ) , y, ..., u ) имеет значение И. В таком случае R ( ( х ) , y, ..., u ) имеет значение И для данных y, ..., u и для каждого x . Но так как функция ( х ) пробегает всё поле , когда x пробегает поле M , то R ( x, y, ..., u ) имеет значение И для данных y, ..., u и для всех x из . В силу определения R ( x, y, ..., u ) также принимает значение И . Обра т н о , если R ( x, y, ..., u ) принимает значение И , то R ( x, y, ..., u ) имеет значение И для да н ных y, ..., u и для каждого x из . В таком случае выражение R ( ( х ) , y, ..., u ) имеет зн а чение И для данных y, ..., u и для каждого x из M , так как ( х ) для любого x принадлежит . Аналогичным образом можно показать , что выражения ( ) R ( ( х ) , y, ..., u ) и ( ) R ( x, y, ..., u ) также равносильны. Рассмотрим формулу U ( , ..., ), которую можно представить в форме ( x 1 )( x 2 )...( x p ) B ( , ..., , x 1 , ..., x p ). B ( , ..., , x 1 , ..., x p ) представляет собой предикат , определённый на поле M и зависящий от p переме н ных x 1 , ..., x p . Каждое из этих переменных входит в формулу B только через предикаты , ..., . С другой стороны , мы видели , что предикаты ( х ) и ( ( х )) равносильны . П о этому если в формуле B ( , ..., , x 1 , ..., x p ) мы заменим x i на ( х i ), то получим равносил ь ное выражение : B ( , ..., , x 1 , ..., x p ) B ( , ..., , ( x 1 ), ..., ( x p )). Отсюда сл едует , что ( x p ) B ( , ..., , x 1 , ..., x p ) ( x p ) B ( , ..., , ( x 1 ), ..., ( x p )). Далее можно заключить , что ( x p ) B ( , ..., , ( x 1 ), ..., ( x p )) B ( , ..., , ( x 1 ), ..., ( x p-1 ), x p ). Рассуждая аналогичным образом , мы получим ( x p-1 ) ( x p ) B ( , ..., , x 1 , ..., x p-1 , x p ) B ( , ..., , ( x 1 ), ..., ( x p-2 ), x p-1 , x p ) и , наконец , придём к следующему : ( x 1 )( x 2 )...( x p ) B ( , ..., , x 1 , ..., x p ) B ( , ..., , x 1 , ..., x p ). Пр авая часть последней равносильности , согласно смыслу символа , предста в ляет не что иное , как формулу ( x 1 )...( x p ) B ( , ..., , x 1 , ..., x p ), отнесённую к полю . Таким образом , мы доказали , что формула U ( , ..., ) сохраняет своё значение , если её отнести к полю , и теорема , таким образом , доказана. С л е д с т в и е . Если формула U , содержащая только предикаты , зависящие от о д ного переменного , является тождественно истинной для всякого поля , не превышающего элементов , где n – число предикатов в U , то формула U тождественно истинна (т . е . истинна для любого поля ). В самом деле допустим , что U не является тождественно исти н ной формулой . В таком случае её от рицание выполнимо на некотором поле . Так как также удовлет воряет условиям теоремы , то найдётся поле , содержащее не более элеме н тов , на котором формула выполнима . Следовательно , U не может быть истинной на этом поле , что противоречит условию . Итак , предположение , что U не является тожд е ственно истинной , приводит к противоречию , что и требовалось доказать. § 2. П рактика по решению п роблемы разрешимости формул , содержащих предикаты от одного переменного Доказанная (в предыдущем параграфе ) теорема позволяет решать проблему разр е шимости для формул , содержащих только предикаты , зависящие от одного переменного . Из следствия видно , что д ля того , чтобы установить , является ли формула U тождественно истинной или нет , достаточно проверить , является ли она тождественно истинной для вс я кого поля , содержащего не более чем элементов. Заметим , что достаточно проверить , является ли данная формула U тождественно истинной на поле , состоящем ровно из элементов . Это следует из т ого , что для формул рассматриваемого типа имеет место следующее : если формула U тождественно истинна на некотором поле , то она тождественно истинна на всякой его части. Рассмотрим произвольное поле , содержащее ровно элементов : , , ..., . Легко видеть , что всякая формула , имеющая вид : ( x ) B ( x ), отнесённая к данному полю , равносильна формуле B ( ) B ( ) ... B ( ). А формула , имеющая вид : ( x ) B ( x ), равносильна формуле B ( ) B ( ) ... B ( ). В таком случае произвольная формула U , отнесённая к полю , ..., , равн о сильна формуле , в которой все кванторы заменены операциями логического произвед е ния и логической суммы . Если в U входили только предикаты A 1 , ..., A n , зависящие от одн о го переменного , то представляет собой формулу , образованную только операциями а л гебры высказываний н ад выражениями A i ( x j ), 1 i n , 1 j . Так как предикаты A i ( x ) совершенно произвольны , то выражения A i ( x j ) представляют собой совершенно произвол ь ные высказывания . Формулу тогда можно рассматривать как формулу алгебры выск а зываний , у которой A i ( x j ) являются элементарными переменными высказываниями . Тогда вопрос о тождественной истинности U на поле , , ..., оказывается эквивалентным вопро су о тождественной истинности , как формулы алгебры высказываний с переме н ными высказываниями A i ( x j ). Заметим , что формула алгебра высказываний по существу не зависит от того , к а ковы элементы поля , ..., , а зависит только от их числа , так как если мы возьмём другое поле , ..., , то в произойдёт только перемен а обозначений переменных высказываний A i ( x j ) на A i ( x j ). В силу этого мы можем сказать , что если тождественно истинна , как форму ла алгебры высказываний , то формула U тождественно истинна на л ю бом поле из p элементов , и обратно . С другой стороны , был получен конструктивный сп о соб определять – является произвольная формула алгебры высказываний тождественно и с тинной или нет . Применяя этот критерий , мы можем установить , будет ли произвольная формула U , содержащая только предикаты от одного переменного , тождественно истинной на любом поле , содержащем p = элементов . В таком случае в силу высказанного выше положения мы можем решить также и вопрос о том , будет формула U тождественно исти н ной или нет . Разберём это конкретно на примерах. П Р И М Е Р 1 : Итак , пусть дана формула U , имеющая вид : ( x )[ P ( x ) ( P ( x ))], отнесённая к некоторому полю L . Для того , чтобы установить тождественную и с тинность этой формулы , нам достаточно проверить , является ли она тождественно исти н ной на поле , содержащем ровно элементов (см . выше ). В данном случае число предик а тов ( n ) равно 2, т.е . L может быть представлено как a 1 , a 2 , a 3 , a 4 . Легко видеть , что формула U равносильна : ( x )[ P ( x ) ( Q ( x ) P ( x ))], которая , отн е сённая к полю L , равносильна : [ P ( ) ( Q ( ) P ( ))] [ P ( ) ( Q ( ) P ( ))] [ P ( ) ( Q ( ) P ( ))] [ P ( ) ( Q ( ) P ( ))]. Таким образом , представляет собой формулу , образованную только операциями алгебры высказываний над выражениями P ( ) и Q ( ), где i = , т.е . её можно рассматр и вать как формулу алгебры высказываний , у которой P ( ) и Q ( ) являются элементарными переменными высказываниями . Значит , ответив на вопрос о тождественной истинности , мы сможем сказать , является ли формула U тождественно истинной или нет. является тождественно истинной в алгебре высказываний U также тожд е ственно истинная формула на поле , со держащем элементов . Это оэначает , что U тожд е ственно истинна. П Р И М Е Р 2 : Доказать , что формула U , отнесённая к некоторому полю L , пре д ставленная как [( х )( Q ( x )) P ( x )], является тождественно истинной. Для этого она должна быть тождественно истинной на поле , содержащем ровно элементов . В данном случае n = 2, т.е . L можно опять определить как a 1 , a 2 , a 3 , a 4 . Применяя равносильные преобразования над U , можем заключить её равносил ь ность формуле : ( х )[( Q ( x )) P ( x )], которая , отнесённая к полю L , равносильна : [( Q ( )) P ( )] [( Q ( )) P ( )] [( Q ( )) P ( )] [( Q ( )) P ( )]. Легко видеть , что , как и в предыдущем примере , представляет собой формулу , образованную только операциями алгебры высказываний над выражениями P ( ) и Q ( ), где i = , а поэтому её можно отнести к формулам алгебры высказываний , у которой P ( ) и Q ( ) являются элементарными переменными высказываниями . Является ли формула тождественно истинной ? Формула представляет собой дизъюнкции некоторых формул . Поэтому всякий раз , когда одна из них истинна , сама (по определению дизъюнк ции ) будет тождестве н но истинной . Составим таблицу истинности : P Q Q ( Q) P 0 0 1 0 1 0 1 1 1 0 1 0 0 1 1 1 1 0 1 1 Таким образом , формула ( Q ) P является выполнимой , следовательно , я в ляется тождественно истинной формулой в алгебре высказываний U также тождестве н но истинная формула на поле , содержащем элементов . Эт о означает , что U тождестве н но истинна. § 3. Поиск доказательств в натуральном интуиционистском и с числении предикатов с -символом и предикатом существования Существуют два типа систем натурального вывода : с прямым и непрям ым правилом удаления квантора существования . Прямое правило удаления квантора существования по существу формулируется с использованием языка с эпсилон-символом . Классическое и с числение предикатов с прямым правилом удаления квантора существования элегантно и является хорошей основой для организации систематической процедуры поиска доказ а тельств . Мною была предложена процедура поиска доказательств для классического исчи с ления предикатов с прямым правилом удаления квантора существования [7]. А.В. Смирнов и А.Е. Новодворский [3] реализовали ее на компьютере . Хотелось бы построить интуици о нистское исчисление предикатов с прямым правилом удаления квантора существования и на этой основе сформулировать алгоритм поиска доказательств . Однако на этом пути мы встречаемс я с определенными трудностями . Если мы заменим классические пропозици о нальные правила интуиционистскими , то в результате получим логическую систему , более богатую , нежели интуиционистское исчисление предикатов . Действительно , допустим , что имеет место xA(x). По правилу удаления квантора существования получим A( xA(x)). По правилу введения импликации будем иметь xA(x) A( xA(x)). Из последней формулы по правилу введения квантора существования получаем y( xA(x) A(y)). Запишем этот вывод формально 1 xA(x) допущение 2 A( xA(x)) у ; 1 3 xA(x) A( xA(x)) в ; 1-2 4 y( xA(x) A(y) в ; 3 Но как хорошо известно , последняя формула не доказуема интуиционистски . Анал о гично в этой системе може т быть доказан принцип конструктивного подбора Маркова Где в этих доказательствах неинтуиционистские шаги ? Ответ , видимо , неоднозн а чен . В книге [5] я предлагал наложить ограничения на непрямые правила вывода : потреб о вать , чтобы -термы не входили в устраняемые допущения и заключение . Однако это огр а ничение слишком стеснительно и неэлегантно . А.Г . Драгалин [1], а затем Д . Скотт ввели другое ограничение : в правилах введения квантора существования и удаления квантора общности мы д олжны потребовать , чтобы вводимый или исключаемый терм был не пуст . Это более изящное решение проблемы . В настоящей статье я предлагаю формулировку и н туиционистского исчисления предикатов с -символом и предикатом существован ия в виде субординатного вывода . Затем обсуждается проблема систематического поиска выводов в этом исчислении. Язык интуиционистского натурального исчисления с -символом N I строится с п о мощью д вух типов индивидных переменных : свободных - v,v1,v2,... и связанных - x,y,z,. . ., x1, x2, . . ., предикатных знаков , логических связок &, , , , знака абсурдности , предик а та существования , кванторов и , -символа , скобок и запятой . Одновременной инду к цией определяем п онятия квазитерма и квазиформулы . Термами и формулами являются квазитермы и кваиформулы , не содержащие свободных вхождений связанных переменных . Под подстановкой вместо свободной переменной v квазитерма t в квазиформулу или кв а зитерм имеется в виду замеще ние каждого вхождения свободной переменной v в квазитерм или квазиформулу квазитермом t. Подстановку будем обозначать Fv/t A и Fv/t t1. Подст а новка правильна , если ни одна связанная переменная , имеющая свободные вхождения в t не находится в области действи я кванторов или -оператора по этой переменной . Ниже мы будем иметь дело только с правильными подстановками . Отметим , что каждая подстановка терма правильна . Каждую формулу , начинающуюся с квантора мы можем представить в вид е xFv/xA и xFv/xA. Следуя Гильберту и Бернайсу , будем говорить , что терм t1 вл о жен в терм t2, если t2 имеет вид Fv/t1 t3, где подстановка , естественно , правильна . Напр и мер , терм xD(x) вложен в терм yA( xD(x), y). Квазитерм xB(x,y) подчинен квазитерму yA(y, xB(x,y) ),т.е . первый квазитерм имеет свободные вхождения связанной переменной , по которой образован второй терм . В дальнейшем мы будем иметь дело с выводами , п о сылки и заключение которых не будут содержать -термов . Поэтому в N I в выводы не б у дут входить формулы с подчиненными друг другу квазитермами. Вывод имеет вид субординатного вывода , при этом каждый вспомогательный вывод будет иметь не более одного допущения . Определим , что мы будем понимать под су борд и натной последовательностью формул (c-последовательность ), вхождением в нее формулы и ее последней формулой : 1. Пустая последовательность есть с-последовательность , она не имеет последней формулы и ни одна формула не входит в нее. 2. Если A формула , то A есть последовательность формул , A есть последняя форм у ла и формула A входит в нее. 3. Если есть с-последовательность и A формула , то A есть с-последовательность , A её последняя формул а и формула B входит в нее , если она входит в или графически равна A. 4. Если , и суть с-последовательности формул и A формула , то и суть с-последовательности , A их A A последняя формула и формула B в ходит в них , если она входит в или графически равна A. Будем говорить , что формула C непосредственно выводима из формулы A (A и B), если есть одно из правил прямого вывода ; формула C непосредственно выводима из п у стого множества формул , если C есть аксиома , т.е . имеет место правило . Теперь введем понятие натурального вывода для системы N I. 1. A есть вывод из последовательности посылок A, A входит в A и A есть его п о следняя формула. 2. Если A есть аксиома , то A есть вывод из пустой последовательнос ти посылок , A есть его последняя формула и входит в вывод. 3. Если есть вывод из последовательности посылок и A посылка , то есть вывод из последовательности посылок A, A есть его последняя формула и формула B входит в вывод , если B входит в или графически равно формуле A. 4. Если есть вывод из последовательности посылок , формула C непосредственно выводима из формул , входящих в ( или является аксиомой ), то есть вывод из последовательности посылок , C его последняя формула и B входит в вывод , если оно входит в или графически равно C. На применение правила введения квантора общности накладываем ограничение : если есть вывод из последовательности посылок , формула A(w) входит в вывод , но в формулы из не входит собственная п е ременная w, то xFw/x A(w) есть вывод из последовательности посылок . 5. Если есть вывод из последовательности посылок и есть вывод из посылок ,A и все формулы из входят в , B есть последняя формула , то есть вывод из посылок и A B есть его последняя формула. 6. Если есть вывод из посылок , есть вывод из посылок 1 ,A и есть вывод из посылок 2 ,B,формулы 1 и 2 входят в , формула C есть последняя формула и , то есть вывод из посылок и C есть его последняя формула. 7. Если есть вывод из последовательности посылок ,A и есть его последняя формула , то есть вывод из посылок и A есть его последняя формула. Чтобы определение вывода N C было полным необходимо сф ормулировать прямые правила вывода . Прежде всего есть правило тождественного перехода : из A выводима A, обозначим его буквой I. Остальные правила вывода подразделяются на правила введения и удаления логических констант . В приводимой ниже таблице правил вы в ода мы для полн о ты записываем и непрямые правила (хотя они сформулированы в определении вывода ). Кроме основных будем использовать в качестве официальных также два произво д ных правила е 1 и i2: и Теперь перейдем к процедуре писк а вывода . Поиск начинается с формулировки з а дачи : из посылок A1,...,An требуется вывести формулу В . Мы исходим из допущения , что ни посылки , ни заключение не содержат -символов и предиката существования . Не нар у шая общности м ожно также допустить , что они не содержат свободных переменных . Задача поиска вывода записывается в виде Это , естественно , не вывод . Построение ( поиск ) выво да совершается с помощью двух типов шагов : синтетических и аналитических . Синтетический шаг состоит в примен е нии некоторого прямого правила вывода . Аналитический шаг сводит задачу к подзадачам. Сформулируем аналитические и синтетические правила поиска выво да для импл и кации . Задача вывода формулы A B из некоторой последовательности посылок сводится к подзадаче построения вывода формулы B из того же множества посылок и дополнительн о го допущения A. Это аналитическое правило введен ия импликации . Мы его запишем в виде где n наибольший номер в первоначальной задаче . В анализе указаны официальные правила вывода (не правила поиска вывода ). Аналитическое правило удаления импликации состоит в сведении задачи вывода формулы C из формулы A B, стоящей выше знака выв о димости , к двум подзадачам : выводу формулы A из прежних посылок и выводу формулы C из прежних посыл ок и формулы B. Символически Синтетическое правило удаления импликации разрешает написатьвыше знака выв о димости формулу B, если формулы A и A B входят в фигуру заключения выше знака в ы водимости : Для симметрии можно сформулировать и синтетическое правило введения и мплик а ции : если в фигуру выше знака выводимости входит формула A, то непосредственно над знаком выводимости можно написать формулу B A. Однако формулу B надо указать д о полнительно . Символически Если в фигуру поиска вывода выше знака выводимости входит формула A и A стоит ниже знака выводимости , то знак выводимости выбрасывается - это правило исключения знака выводимости Если A стоит непосредственно над |-, то нижнее вхождение A и знак выводимости опускаются. Специфически интуиционистскими являются аналитические правила удаления и м плик ации , введение дизъюнкции , правило добавления заключения (вместо классического аналитического правила удаления отрицания ), а также правила для кванторов и , естестве н но , правило для предиката существования . При формулировке кванторных правил испол ь зуются вр еменные переменные , -термы и свободные переменные . К сожалению , мы не можем обойтись без свободных переменных и сформулировать правило введения квантора общности в виде если A( x 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.