Учебник. Никифоров А. Л. Логика и теория аргументации
 Скачать 1.04 Mb.
|
Изучив материалы темы, Вы сможете: понять, что такое исчисление предикатов; применять метод аналитических таблиц для обоснования об- щезначимости формул исчисления предикатов; перечислить правила редукции; уяснить смыл свободных и связанных переменных; записать предложение, используя язык исчисления предикатов. Исчисление предикатов – раздел математической логики, исследующий операции с высказываниями, расчленёнными на субъект и предикат. Алфавит языка логики предикатов образуется присоедине- нием к алфавиту языка логики высказываний следующих знаков: а) квантор всеобщности (читается – все, всякий, каков бы ни был и т.д.); квантор существования (читается – некоторые, хо- тя бы один, существует и т.д.). б) предметные или индивидные переменные ; в) символы n-местных (n= 1, 2…) предикатов, или n-местные предикатные буквы. Символы одноместных предикатов и т.д. В предикатных буквах верхний индекс указывает число их (аргументных) мест, а нижние индексы служат для различения предикатных букв с одинаковым числом мест. Определение предикатной формулы. 1. а) пропозициональная буква есть формула; б) выражение, состоящее из n-местной предикатной бук- вы с приписанной справа n-членной последовательностью пред- метных переменных, есть формула; 2. а) если А, В – формулы, то каждое из следующих выра- жений: A, (A&B), (AvB), (A→B) есть также формула; б) если А – формула, х – предметная переменная, то каж- дое из следующих выражений и есть формула. в) выражение считается формулой тогда, и только тогда, когда оно может быть построено в соответствии с пп. 1-2. Из определения непосредственно следует, что формула ло- гики высказываний является частным случаем формулы логики предикатов, или предикатной формулы. Формулы, определяемые в п. 1, определения предикатной формулы, называются элементарными. Например, формулы: p, Gx, Rxy, Vxyz – элементарные фор- мулы. Элементарная формула с одноместной предикатной буквой, например, формула Gx, читается: «х обладает свойством G», или «G от х»; элементарная формула с двухместной предикатной бук- вой, например, Rxy читается: «х находится в отношении R к y», или «R от x, y»; элементарная формула с трёхместной предикат- ной буквой, например, Vxyz может быть прочитана: «x, y, z нахо- дятся в отношении V», или «V от x, y, z» и т.п. Иногда переменные, стоящие после предикатной буквы, за- ключают в скобки и разделяют запятыми. Так, вместо Vxyz можно было бы написать V (x, y, z). Кроме того, элементарные формулы с двухместными предикатными буквами записываются так: пер- вую переменную ставят перед предикатной буквой, а вторую – после неё. Например, вместо Rxy пишут xRy. При построении выводов и доказательств средствами логи- ки предикатов основную роль играют понятия свободных и свя- занных вхождений переменных в формуле. Определение свободных и связанных вхождений переменных в формуле F. 1. F есть элементарная формула: а) в F нет ни свободных, ни связанных переменных, если F – пропозициональная буква; б) в F все вхождения переменных свободны, если F не явля- ется пропозициональной буквой. 2. F не есть элементарная формула: а) формулу F можно представить в одном из следующих ви- дов: A, A&B, AvB, A→B, тогда в F свободны (соотв. связаны) те, и только те, вхождения переменных, которые происходят от сво- бодных (соотв. связанных) вхождений переменных в А или В; б) формулу F можно представить в одном из видов – , , тогда в F: 1) все вхождения переменной х связаны; 2) вхож- дения остальных переменных свободны (соотв. связаны), если они происходят от свободных (соотв. связанных) вхождений пе- ременных в А. Вхождение переменной х в формулу F связано, если в F оно находится в подформуле, начинающейся квантором или , за которым непосредственно следует переменная х и о котором го- ворят в данном случае, что он связывает переменную х. Например, в формуле все вхождения переменной х связаны; первое и последнее вхож- дения переменной y свободны, остальные вхождения переменной y связаны; все вхождения переменной z свободны, единственное вхождение переменной связано. Параметрами формулы называют те переменные, которые имеют свободные вхождения в данной формуле. В нашем приме- ре параметрами формулы являются y, z. Применяя логический аппарат к анализу обычных рассуж- дений и к решению логических задач, важно научиться записы- вать предложения обычного языка с помощью логической симво- лики. Пример. Запишем на языке логики предикатов предложение: «Ни один человек не бессмертен». Получаем формулу: Читается: каков бы ни был х, если х человек, то неверно, что он бессмертен. Пример. Запишем на языке логики предикатов предложение: «Всякий студент изучает какую-нибудь науку». Получаем фор- мулу: Как и в логике высказываний в логике предикатов сущест- вуют общезначимые формулы или законы логики. Общезначимая формула исчисления предикатов – тождественно-истинная, все- гда-истинная формула исчисления предикатов. Иначе можно ска- зать, это выражения, из которых при любой подстановке значе- ний свободных переменных получаются истинные высказывания. Приведём некоторые общезначимые формулы исчисления предикатов: 1. ; 2. ; 3. ; 4. ; 5. A↔ A; 6. ; 7. ; 8. , где х не входит свободно в А; 9. ; 10. , где х не входит свободно в В; 11. ; 12. , где х не входит свободно в А; 13. ; 14. ,где х не входит свободно в А; 15. ; 16. ; 17. , где х не входит свободно в А; 18. , где х не входит свободно в А; 19. A; 20. ; 21. ; 22. A ; 23. ; 24. ; 25. ; 26. ; 27. , где х не входит свободно в А; 28. , где х не входит свободно в В; 29. , где х не входит свободно в А. Для обоснования общезначимости формул и наличия отно- шения логического следования существует, так называемый ме- тод аналитических таблиц. Аналитической таблицей называется конечная или беско- нечная последовательность строк , …, в которой каждая строка содержит конечное число списков формул языка логики предикатов. Каждая последующая строка получается из предшествующей заменой какого-нибудь списка формул на один или два новых списка формул на основании некоторого правила редукции. Список формул называется замкнутым, если в его составе имеется некоторая формула С и её отрицание С. Аналитическая таблица называется замкнутой, если она содержит конечное число строк и каждый список формул, нахо- дящийся в последней строке таблицы, является замкнутым. Формула А общезначима (╞ А), если и только если сущест- вует замкнутая аналитическая таблица, первая строка которой содержит единственный список формул, состоящий из одной формулы – формулы A. Из формул логически следует формула В ( ╞ В), если существует замкнутая аналитическая таблица, первая строка которой содержит единственный список формул, состоящий из формул , B. Правила редукции: Γ, Α&Β, Δ [&] Γ, Α, B, Δ Γ– последовательность (возможно, пустая) формул, предшест- вующих Α&Β, а Δ – последовательность (возможно, пустая) фор- мул, следующих за Α&Β. Γ‚(A&B)‚Δ [&] Γ‚Α‚Δ|Γ‚Β‚Δ Γ‚ΑvB‚Δ [v] Γ‚Α‚Δ|Γ‚B‚Δ Γ‚(AvB)‚Δ [v] Γ‚A‚Β‚Δ Γ‚Α→B‚Δ [→] Γ‚A‚Δ|Γ‚B‚Δ Γ‚(A→Β)‚Δ [→] Γ‚Α‚Β‚Δ Γ‚Α‚Δ [] Γ‚Α‚Δ Γ‚ ‚Δ [ ] , Γ‚ ‚Α(t)‚Δ где А(t) – результат замены всех свободных вхождений α в А на произвольный замкнутый терм t. Γ‚ ‚ Δ [ ] Γ‚Α(k)‚Δ где Α(k) – результат замены всех свободных вхождений α в А на предметную константу k, которая не содержится в верхнем спи- ске. Γ‚ ‚Δ [ ] Γ‚A(k)‚Δ где Α(k) – результат замены всех свободных вхождений α в А на предметную константу k, которая не содержится в верхнем спи- ске. Γ‚ ‚ Δ [ ] Γ‚ ‚Α(t)‚Δ где А(t) – результат замены всех свободных вхождений α в А на произвольный замкнутый терм t. Рассмотрим на примере метод построения аналитических таблиц. Пример. Обоснуем общезначимость формулы Строим аналитическую таблицу: [ →] [ ] [ ] [ ] [ ]. Аналитическая таблица представляет собой некоторую по- следовательность шагов, которая представляет собой рассужде- ние от противного. Поэтому в первой строке таблицы записыва- ется формула, противоречащая исходной формуле. Последняя строка должна содержать противоречие, то есть формулу С и её отрицание С. В нашем примере единственный формульный спи- сок последней строки содержит формулу вместе с её отри- цанием , поэтому аналитическая таблица замкнута и фор- мула общезначима. В строке 3 мы при- меняем правило [ ] и заменяем свободные вхождения в переменной х на предметную константу а. В строке 4 применяем правило [ ], переменную у, стоящую за в формуле заменяем константой, не встречающейся в единст- венном списке формул строки 3, то есть любой константой, кро- ме а, скажем b. Потом применяем правило [ ] , в результате должна сохраниться формула и добавиться формула , где t – любой замкнутый терм. В формульном списке стро- ки 4 содержатся два замкнутых терма – константы а и b. Выбира- ем из них b, так как это поможет нам достигнуть цели – получения в формульном списке формул вида С и С. Применяя правило [ ], сохраняем формулу и к списку формул добавляем , где t – произвольный замкнутый терм. Заменя- ем t на константу а. В ряде случаев построенная аналитическая таблица может свидетельствовать о необщезначимости некоторой формулы А или о том, что из не следует логически В. Это имеет место в том случае, когда первая строка таблицы включает един- ственный список, состоящий из формулы Α (или из формул , B), а сама таблица незамкнута, но содержит ко- нечное число строк и к формульным спискам последней строки нельзя применить никакое правило редукции. Контрольные вопросы: 1. Дайте определение классическому исчислению предикатов. 2. Что такое свободные и связанные переменные? 3. Как можно обосновать общезначимость формулы исчисле- ния предикатов? 4. Какую роль выполняют кванторы всеобщности и существо- вания в формулах исчисления предикатов? 5. Дайте определение предикатной формулы. 6. При каких условиях аналитическая таблица считается замк- нутой? Тема 10. ТЕОРИЯ ДЕДУКТИВНЫХ РАССУЖДЕНИЙ Изучив материалы темы, Вы сможете: уяснить смысл и значение теории дедуктивных рассуждений; понять, что такое система натурального вывода; объяснить разницу между системой естественного вывода ло- гики высказываний и системой естественного вывода логики предикатов; дать определение кратной импликации; знать правила логического следования, правила построения прямого доказательства, правила построения косвенного дока- зательства и кванторные правила вывода; Исследование рассуждений, их видов и способов осуществ- ления входит в число основных задач логики. В общем случае под рассуждением понимают процедуру последовательного по- шагового перехода от одних высказываний, принятых в качестве исходных, к другим высказываниям. Каждый шаг этого процесса осуществляется на основе некоторого правила, называемого пра- вилом вывода. Последнее высказывание, полученное в данном процессе, называется заключением рассуждения. Дедуктивными являются лишь те рассуждения, в которых между высказываниями, принятыми в качестве исходных, и за- ключением сохраняется отношение логического следования. Теория дедуктивных рассуждений отвечает на вопрос, как строятся рассуждения дедуктивного типа. Процедуры дедукции, как теоретического метода исследо- вания имеют большое значение при построении научного знания. В зависимости от степени прояснённости дедуктивных связей между отдельными утверждениями теорий различают несколько их типов. К первому типу относятся содержательные теории. В их составе дедукция если и используется, то лишь для связи не- которых отдельных положений теории. При этом исходные ут- верждения в рассуждениях представляют собой некоторые до- пущения, называемые посылками. Посылки не обязаны быть ис- тинными, а потому любое предложение, которое дедуцируется с их использованием, считается не истинным, а условно истинным: заключительное предложение истинно при условии, что посылки являются истинными. Примерами логических содержательных теорий являются логики высказываний и предикатов. Другой тип составляют формализованные теории. К их чис- лу относятся теории, содержание которых взаимосвязано и де- дуктивно выводится из некоторых первоначально принятых ис- ходных утверждений. Последние называются аксиомами, а сами теории носят название аксиоматизированных теорий. Так как ак- сиомы представляют собой истинные высказывания о некоторой предметной области, все другие положения, дедуцируемые из них, тоже считаются истинными. Кроме формализованных теорий, можно выделить формаль- ные теории. В отличие от формализованных теорий, в которых специально не выделяются средства дедукции, и в силу этого многие дедуктивные шаги осуществляются на интуитивном уровне, в формальных теориях структурируется не только само знание, но и способы его получения. К формальным теориям от- носятся исчисление высказываний и исчисление предикатов пер- вого порядка. Задача этих логических теорий – описание обыч- ных процедур рассуждения, используемых в теоретической дея- тельности людей. Причём рассуждения, которые строятся в дан- ных исчислениях, будут формальными рассуждениями, состоя- щими в выведении одних формул из других формул. Каждое та- кое формальное рассуждение можно трактовать как модель раз- личных содержательных рассуждений, имеющих ту же самую ло- гическую структуру. Исчисление высказываний и исчисление предикатов перво- го порядка являются разновидностями натурального вывода. Си- стема натурального вывода – система классической логики, ко- торая не содержит аксиом и основывается только на правилах вывода. Когда в обычных рассуждениях мы выводим следствия из посылок, подыскиваем посылки (гипотезы), из которых может быть выведено некоторое предложение, находим доказательства или опровержения и т. п., то во всех этих случаях наши рассуж- дения развёртываются в соответствии с правилами логического следования. Как формы выражения логических законов, тождественно- истинные формулы, или логические тождества, используются для обоснования правил логического следования. С точки зрения са- мой процедуры их обоснования особое значение имеет способ представления формул в виде так называемых кратных имплика- ций. Кратной импликацией называется формула вида …( ) …) (*) Формула (*) читается так: если , то С. Члены кратной импликации, обозначенные в (*) посредст- вом называются антецедентами, а член С – консек- вентом При n=1 имеем схему однократной (обычной) импликации ; при n=2 – схему двукратной импликации ; при n=3 – схему трехкратной импликации и т.д. При n=0 считаем, что формула построенная по схеме (*) кратной импликации, совпадает с формулой С. В этом случае мы имеем дела с так называемой нулькратной, или, как ещё говорят «вырожденной» импликацией. Таким образом, нулькратная им- пликация содержит консеквент и не содержит антецедентов. Любую формулу независимо от того, содержит она знак им- пликации в качестве главного логического знака или нет, можно рассматривать как кратную импликацию. Важно уметь анализировать формулу с помощью схемы кратной импликации. Этот анализ может иметь различную глу- бину, в зависимости от того, какие части анализируемой форму- лы рассматриваются в качестве антецедентов и кон- секвента С в схеме кратной импликации. Так, формулу ((p→q)&(q→r))→(p→r) Можно рассматривать в качестве однократной импликации, т.е. как построенную по схеме в этом случае мы в качестве берём формулу ((p→q)&(q→r)), а в качестве С (p→r). Но если в качестве взять ((p→q)&(q→r)), в качестве p и в качестве С r, то формула ((p→q)&(q→r))→(p→r) рассматривается теперь уже как двукратная импликация, т.е. как формула вида Для данной формулы неосуществим более тонкий анализ по схеме кратной импликации. Но возможен ещё более грубый ана- лиз, если всю анализируемую формулу рассматривать в качестве С, т.е. в качестве нулькратной импликации, не учитывая того, что она содержит знак импликации в качестве главного логического знака. Между тем формулу pv(q&(p→r)) можно рассматривать только в качестве нулькратной импликации. При анализе формулы по схеме кратной импликации следу- ет обращать внимание на расположение скобок. Так, каждая из приводимых ниже формул ((p→r)→p)→r, (p→q)→(p→q) может быть представлена в виде , но только вторая – в виде Таким образом, проанализировать формулу F по схеме кратной импликации значит, для данной формулы подобрать схему …( ) …) с некоторым подходящим значением n и каждому , С поставить в соответствие подформулы формулы F так, что заме- няя , С сопоставленными им подформулами, мы сно- ва получаем анализируемую формулу. Анализ формулы F по схеме кратной импликации мы назо- вём предельным, если букве С в этой схеме ставится в соответст- вие подформула формулы F, не содержащая знака → в качестве главного логического знака. В силу естественно сложившихся методов рассуждения при осуществлении процедуры обычного (неформального доказа- тельства), особенно в математике и других точных науках, дока- зываемые предложения, или тезисы доказательства, приводят как правило, к форме условного предложения. Их называют теоре- мами. В теореме различают условие (или допущения) – часть, сто- ящую после слова «если» и перед словом «то», и заключение – часть стоящую после слова «то». Как явствует из способа чтения кратной импликации, формула такого вида является аналогом ус- ловного предложения; причём её антецеденты отвечают пунктам условия, а консеквент – заключению данного предложения. В свою очередь выше описанный анализ формулы по схеме крат- ной импликации служит аналогом процедуры выявления в дока- зываемом предложении условий и заключения. С помощью табличного метода легко убедиться, что кратная импликация истинна во всех случаях, кроме того, когда каждый из её антецедентов истинен, а консеквент ложен. Кратная импли- кация тождественно-истинна тогда и только тогда, когда во всех строках её таблицы, где каждому антецеденту приписывается ло- гическое значение «истинно», консеквенту приписывается то же значение. Тождественно-истинная кратная импликация определяет не- которое правило логически корректного перехода, иначе говоря, правило логического следования, от посылок, имеющих структу- ру её антецедентов, к заключению, имеющему структуру её кон- секвента. Логические рассуждения способствуют применению крите- рия практики для проверки гипотез посредством проверки выво- димых из них следствий и дальнейшему превращению гипотез в теории. Правила следования играют также известную роль в по- дыскании гипотез и в процессах научного объяснения, поскольку возможно «применение» дедуктивных правил в обратном поряд- ке – от заключения к посылкам. В логике правила следования записываются в виде фигур рассуждения С которые читаются так: из следует С. Члены называются посылками, а член С называется заклю- чением данной фигуры. Не всякая фигура такого вида является правилом следования. Определение правила логического следования. Фигура С называется корректной фигурой, или правилом следования, если формула вида …( ) …) есть логическое тождество. Таким образом, для проверки корректности некоторой фи- гуры рассуждения, нужно образовать кратную импликацию, сде- лав посылки фигуры антецедентами, а заключение фигуры – кон- секвентом этой импликации, и выяснить, является ли полученная этим путём формула тождественно-истинной. Применяя правила следования, мы можем из исходных формул, называемых посылками, или допущениями, получать но- вые формулы, логически следующие из исходных, путём по- строения последовательностей формул, в которых каждая форму- ла или является посылкой, или же следует из предшествующих формул по одному из правил следования. Такого рода последовательности формул называются фор- мальными выводами. Они служат в логике моделями, на которых изучаются закономерности обычных логических рассуждений. Пример. Приводимая ниже последовательность формул 1. p→(q→r) – посылка; 2. p&q – посылка; 3. p – УК (2); 4. q→r – МП (1,3); 5. q – УК (2); 6. r – МП (4,5) есть вывод из исходных формул (посылок) 1-2 формулы 6 (заключения данного вывода), при построении которого исполь- зуются правила УК и МП. Для того чтобы придать точный смысл описательной харак- теристики логической структуры обычных рассуждений была со- здана логическая система, получившая название система есте- ственного вывода или натуральное исчисление. В рамках данного исчисления можно строить формальные доказательства, структу- ра которых возможно точно передаёт логическое строение обыч- ных рассуждений. Опишем систему естественного вывода, которую обозначим буквой N. Основные правила системы N содержат: Правила логического следования: A A→B – модус поненс (МП); B A B – введение конъюнкции (ВК); A&B A&B – удаление конъюнкции (УК); A A&B – удаление конъюнкции (УК); B A – введение дизъюнкции (ВД); AvB B – введение дизъюнкции (ВД); AvB AvB A→C B→C – удаление дизъюнкции. C Правила построения прямого доказательства: Прямое доказательство формулы (кратной импликации) ви- да …( ) …) строится согласно следующей процедуре. На любом шаге построения можно написать: 1) одну из формул в качестве допущения; 2) формулу, следующую из ранее написанных формул по одному из правил логического следования; 3) ранее доказанную формулу. Прямое доказательство данной формулы считается постро- енным, если в соответствии с пп. 1)-3) получена последователь- ность формул оканчивающаяся формулой С. Пример. Ниже построено доказательство формулы (p→q)→((p&r)→(q&r)) Доказательство. 1. p→q – допущение; 2. p&r – допущение; 3. p – УК (2); 4. r – УК (2); 5. q – МП (1,3); q&r – ВК (4,5). Непронумерованная последняя строка означает, что доказа- тельство закончено. Ещё один пример. Надо доказать формулу q→q Доказательство. q – допущение. Введя в качестве допущения формулу, совпадающую с ан- тецедентом доказываемой импликации, мы сразу же заканчиваем доказательство, потому что консеквент доказываемой имплика- ции совпадает с её антецедентом, а, прямое доказательство за- канчивается получением последовательности формул, оканчи- вающейся формулой, совпадающей с консеквентом доказывае- мой формулы. Эту формулу мы можем использовать в процессе доказа- тельства других формул. Например. Следует доказать формулу (pvq)→((p→q)→q) Доказательство. 1. pvq – допущение; 2. p→q – допущение; 3. q→q – ранее доказанная формула (р.д.ф.); q – УД (1, 2, 3). Для формулировки ещё одного правила построения доказа- тельства потребуется следующее понятие. Назовём две формулы противоречащими, если одна из них может быть получена из дру- гой приписыванием слева знака . Правила построения косвенного (апагогического) дока- зательства. Косвенное доказательство формулы (*) строится согласно следующему предписанию. На любом шаге построения можно написать: 1) одну из формул в качестве допущения; 1а) формулу противоречащую формуле С; 2) формулу, следующую из ранее написанных форм по одному из правил логического следования; 3) ранее доказанную формулу. Косвенное доказательство формулы (*) считается построен- ным, если в соответствии с пп. 1)-3), включая и п. 1а), получена последовательность формул, содержащая пару противоречащих формул и оканчивающаяся одной из них. Пример. Докажем формулу q→(q&p) Доказательство. 1. q – допущение; 2. q&p – допущение косв. док-ва; 3. q – УК (2) Противоречие: 1,3. Пример. Докажем формулу (p→p)→p Доказательство. 1. p→p – допущение; 2. p – допущение косв. док-ва; 3. p – МП (1,2); Противоречие: 2, 3. Пример. Докажем формулу (p→q)→((p→q)→p) Доказательство 1.p→q – допущение; 2. p→q – допущение; 3. p – допущение косв. док-ва; 4. q – МП (1,3); 5. q – МП (2,3); Противоречие: 4, 5. Доказательство в системе N связано с конечной системой, или совокупностью доказательств, упорядоченных некоторым ес- тественным образом. Завершая описание системы N, мы введём следующее опре- деление доказуемой формулы. Формула называется доказуемой формулой, или логической теоремой (системы N), если можно построить доказательство данной формулы (по правилам систе- мы N). Кроме того, мы принимаем следующее определение знака эквивалентности: Оно означает, что выражение, стоящее слева от знака (знака ра- венства по определению), рассматривается как сокращённая за- пись выражения, стоящего справа от этого знака. Согласно дан- ному определению, если в формуле имеется вхождение выраже- ния из правой части данного определения, то его можно заменять на вхождение выражения из его левой части (и наоборот). Из определения знака ↔ непосредственно следует, что пра- вила A→B B→A – введение эквивалентности (ВЭ) A↔B A↔B – удаление эквивалентности (УЭ); A→B A↔B – удаление эквивалентности (УЭ) B→A представляют собой частные случаи правил ВК и УК. Логические средства, используемые в исчислении высказы- ваний для построения рассуждений, являются слишком бедными, чтобы с их помощью можно было описать всё многообразие раз- личных приёмов, применяемых в процедурах дедукции в кон- кретных науках и повседневной жизни. Эти средства ограничены бедностью языка исчисления высказываний, в котором простые предложения трактуются как не имеющие внутренней структуры. С этой точки зрения язык исчисления предикатов обладает гораз- до большими выразительными возможностями и позволяет ана- лизировать и изучать такие рассуждения, которые зависят от внутренней структуры простых предложений. В исчислении предикатов сохраняются все правила вывода исчисления высказываний, но к ним теперь надо присоединить новые правила, позволяющие оперировать с кванторами. Кванторные правила вывода: – введение всеобщности (ВВ); - удаление всеобщности (УВ); введение существования (ВС); – удаление существования (УС). С А, С – формулы, x, y – переменные, - результат корректной подстановки y в А вместо х. Ограничения на применение правил «введения всеобщно- сти» и «удаление существования». 1. При построении доказательства правило введения все- общности применяется, если выполняются следующие условия: а) собственная переменная данного правила не входит сво- бодно в формулы, написанные ранее в качестве допущений; б) собственная переменная не входит свободно в формулу, обозначенную в схеме правила посредством . 2. При построении доказательства правило «устранение су- ществования» применяется, если выполняются следующие усло- вия: а) собственная переменная данного правила не входит сво- бодно в формулы, ранее написанные в качестве допущений; б) собственная переменная не входит свободно ни в форму- лу, обозначенную посредством , ни в формулу, обозначенную посредством С, в схеме правила УС (т.е. ни в левую посылку, ни в заключение данного правила). Покажем, как строится доказательство формулы логики предикатов. Пример. Следует доказать в системе естественного вывода логики предикатов формулу Доказательство. 1. – допущение; 2. – допущение; 3. A→B – УВ (1); 4. A – УВ (2); 5. В – МП (3,4); – ВВ (5). Пример. Следует доказать в системе естественного вывода логики предикатов формулу Доказательство. 1. – допущение; 2. – допущение; 3. A→B – УВ (1); 4. B – УС (2,3); – ВС (4). Хотя исчисление предикатов представляет собой семантиче- ски полную логическую теорию, оно не является разрешимой теорией. Для исчисления предикатов не существует эффективно- го метода, позволяющего ответить на вопрос, доказуема или нет произвольная формула данного исчисления. Контрольные вопросы: 1. В чём разница между формальными и формализованными теориями? 2. Дайте определение системы естественного вывода. 3. Что такое кратная импликация? 4. Какие ограничения существуют на применение правил «введения всеобщности» и «удаления существования»? 5. Как соотносятся вывод и доказательство? 6. В чём состоит отличие между построением прямого доказа- тельства и построением косвенного доказательства? 7. Что такое антецедент и консеквент? 8. В чём заключается преимущество исчисления предикатов по отношению к исчислению высказываний? |