Реферат: Логика предикатов (WinWord 2000)
МИНИСТЕРСТВО ОБРАЗОВАНИЯ РОССИЙСКОЙ ФЕДЕРАЦИИ
КЕМЕРОВСКИЙ ГОСУДАРСТВЕННЫЙ УНИВЕРСИТЕТ
Юридический факультет
Кафедра философии
РЕФЕРАТ
ПО ЛОГИКЕ
на тему:
"Логика предикатов"
Выполнил: студент гр. Ю-993
Грибанов Ю.Ю.
Проверил:
Овчаров А.А.
Кемерово 1999
СОДЕРЖАНИЕ
Введение . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . .3
Основные понятия . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . .4
§1. Логика предикатов с одним переменным . . . . . . . . . . . . . . .
. . . . . . . . . . . . .5
§2. Практика по решению проблемы разрешимости формул, содержащих
предикаты от одного переменного . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . .9
§3. Поиск доказательств в натуральном интуиционистском исчислении
предикатов с (-символом и предикатом существования. . . . . . . . . . .
. . . . . . . . .11
Литература . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . .17
ВВЕДЕНИЕ
Проблема разрешимости — эта проблема ставится для формул исчисления
предикатов, лишённых символов постоянных предметов и символов
индивидуальных предикатов. В последующем изложении предполагается, что
рассматриваемые формулы таковы (если не сделано специальных оговорок).
Каждая такая формула представляет собой определённое утверждение,
истинное или ложное, когда оно относится к определённому полю M.
Если такая формула истинна для некоторого поля M и некоторых предикатов,
на нём определённых, мы будем называть её выполнимой.
Если формула истинна для данного поля M и для всех предикатов,
определённых на M, мы будем называть её тождественно истинной для поля
M.
Если формула истинна для всякого поля M и для всяких предикатов, будем
называть её тождественно истинной или просто истинной.
ложна, и наоборот.
Постановка проблемы разрешимости для логики предикатов аналогична
постановке этой проблемы для алгебры высказываний. Её решение и является
целью данной курсовой работы. Итак, проблема ставится следующим образом:
дать эффективный способ для определения — является ли данная формула
выполнимой или нет.
, мы тем самым проверим истинность 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, x1, x2, ...
обозначают неопределённые предметы поля. Их мы будем называть
предметными переменными. Буквы начала алфавита
a, b, c, a1, a2, ...
обозначают определённые предметы поля. Их мы будем называть
индивидуальными предметами или предметными постоянными.
Большими латинскими буквами
A, B, ..., X, A1, A2, ...
мы будем обозначать переменные, принимающие значения И и Л. Их мы
назовём переменными высказываниями. Мы будем также рассматривать и
постоянные высказывания. Их мы будем также обозначать большими
латинскими буквами, как-нибудь отмеченными или просто с дополнительной
оговоркой.
Большие латинские буквы и символы предикатов как индивидуальных
предметов, так и от предметных переменных мы будем называть
элементарными формулами.
Мы будем говорить, что в формулах
((х) U(х) и ((х) U(х)
кванторы ((х) и ((х) относятся к переменному х или что переменное х
связано соответствующим квантором.
Предметное переменное, не связанное никаким квантором, мы будем называть
свободным переменным.
, а знаки отрицания относятся только к элементарным предикатам и
высказываниям, будем называть приведёнными формулами.
Приведённая формула называется нормальной, если она не содержит
кванторов или если при образовании её из элементарных формул операции
связывания квантором следуют за всеми операциями алгебры высказываний.
Если две формулы U и B, отнесённые к некоторому полю M, при всех
замещениях переменных предикатов, переменных высказываний и свободных
предметных переменных соответственно индивидуальными предикатами,
определёнными на M, индивидуальными высказываниями и индивидуальными
предметами из M, принимают одинаковые значения И или Л, то мы будем
говорить, что эти формулы равносильны на поле M.
Если две формулы равносильны на любых полях M, то мы будем их называть
просто равносильными.
Нормальную формулу, равносильную некоторой формуле U, мы будем называть
нормальной формой формулы U.
§1. Логика предикатов с одним переменным
Мы будем рассматривать формулы логики предикатов, содержащие предикаты,
которые зависят только от одного переменного. Логика, в которой
употребляются только такие выражения, соответствует той, которая описана
Аристотелем и вошла как традиционный элемент в систему гуманитарного
образования. Известные формы высказываний этой логики и формы
умозаключений, так называемые «модусы силлогизмов», выражаются полностью
в символике логики предикатов от одного переменного.
элементов, где n - число предикатов, входящих в рассматриваемую
формулу.
Пусть формула U(A1, ..., An), содержащая только символы предикатов A1,
..., An, каждый из которых зависит от одного переменного, выполнима на
некотором поле M. эту формулу мы можем предполагать представленной в
нормальной форме, а все предметные переменные в ней связанными. В самом
деле, какова бы ни была формула U, мы можем, произведя над ней
преобразования, привести её к виду, в котором все кванторы предшествуют
остальным символам формулы, при этом состав её предикатов и предметных
переменных не изменяется. Если в U есть свободные предметные переменные,
то можно связать их квантором общности.
Итак, допустим, что U – нормальная формула. Тогда мы можем представить
её следующим образом:
(( x1)(( x2)...(( xp) B(A1, ..., An, x1, ..., xp),
где каждый из символов (( xi) обозначает квантор ((xi) или ((xi), а
формула
B(A1, ..., An, x1, ..., xp)
кванторов не содержит.
В формуле B(A1, ..., An, x1, ..., xp) все переменные x1, ..., xp входят
в предикаты A1, ..., An, и её можно записать в виде
)),
где i1, ..., in – числа от 1 до p. Однако, будет удобнее пользоваться
выражением
B(A1, ..., An, x1, ..., xp),
.
Покажем, что если для некоторого поля M существуют индивидуальные
предикаты
,
(x) совпадает с данной последовательностью символов И и Л.
n
i представляет собой И или Л, а соответствующий этой последовательности
класс элементов x обозначим
.
. Выберем из каждого непустого класса по одному элементу и обозначим эти
элементы
a1, a2, ..., aq.
.
Легко видеть, что имеет место следующая равносильность:
(х)).
, и поэтому всякое предметное переменное входит только под знаком одного
из этих предикатов.
Пусть R (x, y, ..., u) – предикат, определённый на поле M. Введём
обозначение
R (x, y, ..., u).
, и принимающий значение Л в противоположном случае. Введём также
выражение
R (x, y, ..., u),
будем называть ограниченными кванторами. Если мы все переменные
предиката R (x, y, ..., u) свяжем ограниченными кванторами, например
R (x, y, ..., u),
. покажем, что выражение
(х), y, ..., u)
равносильно выражению
R (x, y, ..., u).
.
Аналогичным образом можно показать, что выражения
) R (x, y, ..., u)
также равносильны.
), которую можно представить в форме
, x1, ..., xp).
, x1, ..., xp)
(хi), то получим равносильное выражение:
(xp)).
Отсюда следует, что
(xp)).
Далее можно заключить, что
(xp)) (
(xp-1), xp).
Рассуждая аналогичным образом, мы получим
, x1, ..., xp-1 , xp) (
(xp-2), xp-1, xp)
и, наконец, придём к следующему:
, x1, ..., xp) (
, x1, ..., xp).
, представляет не что иное, как формулу
, x1, ..., xp),
.
, и теорема, таким образом, доказана.
выполнима. Следовательно, U не может быть истинной на этом поле, что
противоречит условию. Итак, предположение, что U не является
тождественно истинной, приводит к противоречию, что и требовалось
доказать.
§2. Практика по решению проблемы разрешимости формул,
содержащих предикаты от одного переменного
элементов.
элементов. Это следует из того, что для формул рассматриваемого типа
имеет место следующее: если формула U тождественно истинна на некотором
поле, то она тождественно истинна на всякой его части.
. Легко видеть, что всякая формула, имеющая вид:
((x) B(x),
отнесённая к данному полю, равносильна формуле
).
А формула, имеющая вид:
x) B(x),
равносильна формуле
).
, как формулы алгебры высказываний с переменными высказываниями Ai(xj).
элементов. В таком случае в силу высказанного выше положения мы можем
решить также и вопрос о том, будет формула U тождественно истинной или
нет.
Разберём это конкретно на примерах.
П Р И М Е Р 1: Итак, пусть дана формула U, имеющая вид:
P(x))],
элементов (см. выше). В данном случае число предикатов (n) равно 2,
т.е. L может быть представлено как { a1, a2, a3, a4 }.
))].
, мы сможем сказать, является ли формула U тождественно истинной или
нет.
элементов. Это оэначает, что U тождественно истинна.
П Р И М Е Р 2: Доказать, что формула U, отнесённая к некоторому полю L,
представленная как
P(x)],
является тождественно истинной.
элементов. В данном случае n = 2, т.е. L можно опять определить как {
a1, a2, a3, a4 }.
EM???????†???????????????–????????†???–????????†???–????????†??????????
????–????????†???????????????–????????†???
тождественно истинной?
(по определению дизъюнкции) будет тождественно истинной. Составим
таблицу истинности:
P
0 0 1 0 1
0 1 1 1 0
1 0 0 1 1
1 1 0 1 1
элементов. Это означает, что 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), если
.
Теперь введем понятие натурального вывода для системы 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.
|