Автор работы: Пользователь скрыл имя, 02 Декабря 2013 в 14:54, реферат
Формальные системы — это системы операций над объектами, понимаемыми как последовательности символов (т. е. как слова в фиксированных алфавитах); сами операции также являются операциями над символами. Термин «формальный» подчеркивает, что объекты и операции над ними рассматриваются чисто формально, без каких бы то ни было содержательных интерпретаций символов.
- логические символы (
- Ø – отрицание;
- Ù – логическое И (конъюнкция, логическое умножение);
- Ú – логическое ИЛИ (дизъюнкция, логическое сложение);
- ® (Þ) – импликация (если - то);
- « (º) – эквивалентность;
- кванторы переменных:
- $ – квантор существования;
- " – квантор всеобщности;
- вспомогательные символы: круглые скобки, запятые, +, - и т.п.
5. Кванторы
5.1. Историческая справка
Философы давно обращали внимание на логические операции, ограничивающие область истинности предиката, однако не выделяли их в отдельный класс операций. Так, Томас Гоббс считал, что они являются частями имен.
Хотя кванторно-логические конструкции широко используются как в научной, так и в обыденной речи, их формализация произошла только в 1879 г., в книге Фреге «Исчисление понятий». Обозначения Фреге имели вид громоздких графических конструкций и не были приняты. Впоследствии было предложено множество более удачных символов, но общепринятыми стали обозначения для квантора существования (перевёрнутая первая буква англ. Exists — существует), предложенное Чарльзом Пирсом в 1885 г., и для квантора общности, образованное Герхардом Генценом в 1935 г. по аналогии с символом квантора существования. Термины «квантор», «квантификация» также предложил Пирс.
Квантор — общее название для логических операций, ограничивающих область истинности какого-либо предиката и создающих высказывание. Чаще всего упоминают:
В математической логике приписывание квантора к формуле
называется связыванием или ква
5.2. Примеры использования кванторов.
Обозначим предикат «x делится на 5». Используя квантор общности, можно формально записать следующие высказывания (конечно, ложные):
следующим образом:
.
Следующие (уже истинные) высказывания используют квантор существования:
Их формальная запись:
.
Кванторы в математической логике:
(«При всех значениях утверждение верно»).
(«Существует при котором утверждение верно»).
Предметная переменная, входящая в формулу, называется свободной, если она не следует непосредственно за квантором и не входит в область действия квантора по этой переменной, все другие переменные, входящие в формулу, называются связанными. В пределе всякая формула без свободных переменных (замкнутая формула) является высказыванием, которое истинно или ложно, а всякая формула со свободными переменными задает некоторое отношение в предметной области, которую иногда называют областью интерпретации. Это отношение может быть истинно или ложно в зависимости от значений свободных переменных.
Правило отрицания кванторов — применяется для построения отрицаний высказываний, содержащих кванторы, и имеет вид:
6. Семантика логики предикатов первого порядка.
Терм - переменная, константа или функция (т.е. объект или его свойство).
Предикат (атомарная формула, атомарное предложение, атом) - отношение, устанавливающее связь между термами (параметрами). Предикат (в математической логике «атом») - простейший случай формулы, т.е. формула, которую нельзя расчленить на подформулы. Например, друзья(отец(андрей), коля) – отец Андрея и Коля являются друзьями. В этом предикате: друзья - предикатный символ, отец(андрей) – функция, коля – константа. Если параметр отец(андрей) был бы не функцией, а предикатом, то предикат друзья был бы предикатом второго порядка.
Количество термов в предикате называется арностью предиката.
Предикат с арностью, равной 0, обозначает событие, признак или свойство, относящееся ко всей предметной области, например, end.
Предикат с арностью, равной 1, обозначает свойство сущности, например, дом(кирпичный).
Формула (предложение, правило, правильно построенная формула) - это либо предикат (атом), либо одна из следующих конструкций: ØА, AÙB, AÚB, A®B, A«B, ("X) A и ($X) А, где A и B - формулы, а X - переменная. Результатом вычисления формулы является либо истина либо ложь.
Примеры формул:
мать(маша, X) Ù мать(маша, Y) ® брат(X, Y) Ú сестра(X, Y) – если Маша мать X и Y, то X является братом или сестрой Y.
человек(X) ® смертен(Х) – если X – человек, то он смертен.
Приоритет операций и кванторов при исчислении формул показан ниже
В скобках показаны операции (кванторы) с одинаковым приоритетом. Если в формуле используются операции (кванторы) с одинаковым приоритетом, то порядок исчисления слева-направо. Изменение порядка исчисления можно добиться за счет использования круглых скобок «( )».
Квантор существования $ указывает, что предложение истинно, по крайней мере, для одного значения переменной. Например, $X друзья(X, петя) – существует, по крайней мере, один субъект X, который является другом Пети.
Квантор всеобщности " указывает, что предложение истинно, для всех значений переменной. Например, "X человек(X) ® смертен(Х) – все люди смертны.
При комбинации кванторов очень важен порядок их использования, например:
- "X$Y любит(Х, Y) – любой Х любит хотя бы одного Y;
- "Y$X любит(Х, Y) – каждого Y любит хотя бы один Х;
- $X"Y любит(Х, Y) – существует такой Х, который любит всех;
- $Y"X любит(Х, Y) – существует такой Y, которого любят все;
- "X"Y любит(Х, Y) и "Y"Х любит(Х, Y) – все любят всех;
- $X$Y любит(Х, Y) – существует такой X, который любит хотя бы одного из Y;
- $Y$Х любит(Х, Y) – существует такой Y, которого любит хотя бы один X.
7. Исчисление предикатов
Исчисление предикатов первого порядка представляет собой исчисление высказываний, дополненное аксиомами , связанными с кванторами и дополнительными правилами вывода.
1. Алфавит исчисления предикатов состоит из предметных переменных х1 , х2, ..., предметных констант а1, а2, ..., предикатных букв P11, Р21, ..., Рjk... и функциональных букв f11, f21,..., fjk, ..., а также знаков логических связок Ú, Ù,¬,→, кванторов , и скобок (,).
Верхние индексы предикатных и функциональных букв указывают число аргументов, их нижние индексы служат для обычной нумерации букв. Переменные высказывания в исчисление предикатов вводятся либо непосредственно как пропозициональные буквы А1, А2, ..., либо как 0-местные предикаты P10, Р20, ..., т. е. как предикаты без предметных переменных.
2. Формулы. Понятие формулы определяется в два этапа.
а) предметные переменные и константы являются термами;
б) если fn — функциональная буква, a t1,…, tn — термы, то fn(t1,…, tn) — терм.
2)Формулы:
а) если Рп — предикатная буква, a t1,…, tn — термы, то Рп(t1,…, tn) — формула; все вхождения предметных переменных в формулу вида Рп(t1,…, tn)называются свободными;
б) если F1 ,F2 — формулы, то формулами являются ¬F, (F1→ F2),
(F1 Ú F2) ,(F1 Ù F2); все вхождения переменных, свободные в F1 ,F2, являются свободными и в указанных четырех видах формул;
в) если F(x) — формула, содержащая свободные вхождения переменной х, .то "xF(x) и $xF(x) — формулы; в этих формулах все вхождения переменной х называются связанными; свободные вхождения остальных переменных в F остаются свободными.
3. Аксиомы исчисления предикатов делятся на две группы :
1) аксиомы исчисления высказывани
Первая из них непосредственно использует все логические связки:
Система аксиом I:
I 1. A → (B → A);
I 2. (A → B) → ((A → (B → C)) → (A → C));
I 3. (A Ù B) → A;
I 4. (A Ù B) → B;
I 5. A → (B → ( A Ù B));
I 6. A → (A Ú B));
I 7. B → (A Ú B));
I 8. (A → C) → ((B → C) → (( A Ú B) → C));
I 9. (A → B) → ((A → ¬B) → ¬A);
I 10. ¬ ¬A → A
Другая система использует только две связки ¬ и →; при этом сокращается алфавит исчисления (выбрасываются знаки Ù , Ú) и , соответственно, определение формулы. Операции Ù , Ú рассматриваются не как связки исчисления высказываний, а как сокращения (употреблять которые удобно, но не обязательно) для некоторых его формул: A Ú B заменяет ¬А → В, A Ù B заменяет ¬(A → ¬B). В результате система аксиом становится намного компактнее.
Система аксиом II :
II 1. A → (B → A);
II 2. (A → (B → C)) → ((A → B) → (A → C));
II 3. (¬A → ¬B) → ((¬A → B) → A).
Приведенные системы аксиом равносильны в том смысле, что порождают одно и то же множество формул.
2) две предикатные аксиомы:
P1. "xF(x) → F(y);
Р2. F(y) → $xF(x).
В этих аксиомах F(x) — любая формула, содержащая свободные вхождения х, причем ни одно из них не находится в области действия квантора по у; формула F(y) получена из F(x) заменой всех свободных вхождений I на у.
Чтобы пояснить существенность требования к вхождениям х в F, рассмотрим в качестве F(x) формулу $уР(у,х), где это требование нарушено: свободное вхождение х находится в области действия $у. Подстановка этой формулы в аксиому Р1 дает формулу "х$уР(у, х) → $уР(у, у). Если ее проинтерпретировать на множестве N натуральных чисел с предикатом Р «быть больше», то получим высказывание: «если для всякого х найдется у, больший x то найдется у, больший самого себя». Посылка этой импликации истинна на N, а ее заключение ложно, и, следовательно, само высказывание ложно.
4. Правила вывода:
Правила вывода позволяют из данной системы аксиом получать другие истинные формулы исчисления высказываний. Назовем формулу исчисления высказываний ложной, если ее отрицание истинно. Будем обозначать истинные формулы буквой R, ложные - F.
К основным правилам вывода относятся два:
1) Правило заключения (Modus Ponens)
Если A и (A → B) – выводимые формулы, то B также выводима. Это предложение можно записать в виде
A,A→B
B
2) Правило подстановки
Пусть некоторая формула A содержит переменное высказывание А. Тогда, заменив высказывание А всюду, где оно встречается, любой формулой B , получим истинную формулу. Это предложение записывается в виде
A (А)
A (B)
Формула называется выводимой в исчислении высказываний, если ее можно получить, применяя правила вывода к аксиомам исчисления высказываний. Утверждение, что формула B выводима, записывают так:
├ B
Процесс получения формул из аксиом исчисления высказываний называется формальным выводом. Формальный вывод состоит из указания того, какие правила, в каком порядке и к каким формулам применяется для выведения данной формулы.
В исчислении предикатов первого порядка (узком исчислении предикатов) два правила вывода (подстановки и заключения) исчисления высказываний дополняют еще тремя правилами:
Заключение
Формальная система представляет собой совокупность чисто абстрактных объектов (не связанных с внешним миром), в которой представлены правила оперирования множеством символов в чисто синтаксической трактовке без учета смыслового содержания (или семантики).
Информация о работе Формальные системы.Исчисление предикатов