Студопедия  
Главная страница | Контакты | Случайная страница

АвтомобилиАстрономияБиологияГеографияДом и садДругие языкиДругоеИнформатика
ИсторияКультураЛитератураЛогикаМатематикаМедицинаМеталлургияМеханика
ОбразованиеОхрана трудаПедагогикаПолитикаПравоПсихологияРелигияРиторика
СоциологияСпортСтроительствоТехнологияТуризмФизикаФилософияФинансы
ХимияЧерчениеЭкологияЭкономикаЭлектроника

Формальной системы

Читайте также:
  1. Amp;C) популяционные и экосистемы.
  2. CAD/CAM-системы в ТПП
  3. CALS-технологий и единая интегрированной системы управления вуза
  4. I. Общие симптомы заболеваний пищеварительной системы.
  5. I. Понятие, типы и принципы денежной системы.
  6. II. Исследование В-системы иммунитета.
  7. II. Основные элементы денежной системы.
  8. III Рекомендации к написанию курсовой работы по дисциплине «Коррекционно-педагогические системы воспитания и обучения детей дошкольного возраста».
  9. III. Особенности денежной системы РК.
  10. IV. Анатомия органов сердечно-сосудистой системы

В предыдущей лекции рассматривались тождественно истинные фор-

мулы. Если перед нами конкретная формула, то вычисляя таблицу ис-

тинности или КНФ формулы, мы можем определить, будет ли она тож-

дественно истинной. Такие методы позволяют провести проверку на тож-

дественную истинность конкретной формулы, но не дают представления

об общем устройстве, обозрении всех тождественно истинных формул.

Исчисление высказываний — раздел математической логики, изучаю-

щий построение всех тождественно истинных формул. В этом разделе мы

получим более глубокое понимание природы таких формул. Исчисление

высказываний будет построено в виде формальной системы. Понятие

формальной системы необходимо не только в исчисление высказываний.

В дальнейшем и другой раздел математической логики «Теории первого

порядка» будет построен в виде формальной системы. Формальная си-

стема отражает синтаксические аспекты математической теории, т.е. ее

символы, формулы, аксиомы, правила вывода. Приведем точные опреде-

ления трех составных частей формальной системы.

Первая часть формальной системы — ее язык. Чтобы определить

язык формальной системы нужно задать символы этого языка и его фор-

мулы. Если сравнить язык формальной системы с русским языком, то по-

лучим аналогию символов и формул с буквами и словами в русском язы-

ке.

Однако символы формальной системы могут быть произвольными

знаками, например, знаками &, ∗, +. Единственное требование — неде-

лимость символа (символ не имеет частей, из которых составлен) и воз-

можность его распознания в один прием.

Последовательность символов языка называется выражением это-

го языка. Число символов в выражении – длина выражения. Аналогия

в естественном языке: слово насос имеет длину 5. Одно выражение мо-

жет входить в другое. Например, выражение ма имеет два вхождения в

выражение математика. Замена первого вхождения ма на выражение

на выражение на дает выражение натематика.

Не все выражения в естественном языке являются осмысленными

словами. Точно также в формальной системе лишь часть выражений счи-

тается формулами. В каждой формальной системе свои правила обра-

 

зования формул. Как уже отмечалось, язык формальной системы задан

если определены символы этого языка и его формулы.

Вторая часть формальной системы— аксиомы. Задать аксиомы озна-

чает выделить некоторые формулы формальной системы, присвоив им

название аксиомы.

Третья часть формальной системы — правила вывода. Они имеют

вид

A 1, A 2 ,..., An

B

, (7)

где A 1, A 2 ,..., An и B – формулы формальной теории. При этом формулы

A 1, A 2 ,..., An называются посылками правила вывода, а B его заключе-

нием.

Правила указывают способ для получения теорем. Вначале все аксио-

мы объявляются теоремами. Из этого начального списка теорем получа-

ются новые теоремы с помощью правил вывода. Если уже установлено,

что A 1, A 2 ,..., An – теоремы и имеется правило вывода (7) с посылками

A 1, A 2 ,..., An, то его заключение добавляется в список теорем. Тем са-

мым получаем следующее определение теоремы формальной системы.

1. Любая аксиома формальной системы F является ее теоремой.

2. Если A 1, A 2 ,..., An – теоремы и A 1 ,A 2 ,...

B – правило вывода, то B

теорема.

3. То, что формула A является теоремой устанавливается несколькими

применениями правил 1 и 2.

Тоже самое можно выразить иначе. Считаем аксиомы теоремами ша-

га 1. Обозначим множество теорем шага 1 через F 1. Назовем теоремами

шага m все теоремы шага m − 1 и все заключения правил вывода (7), где

A 1, A 2 ,..., An теоремы шага m − 1. Рассмотрим F = F 1 ∪ F 2 ∪ F 3 ∪....

Формула A —теорема тогда и только тогда, когда A ∈ F. Любая теорема

имеет наименьший номер шага n, на котором она получена. Мы можем

доказывать различные утверждения для теорем индукцией по числу n.

Построение исчисления высказываний. Рассмотрим исчисление

высказываний как формальную систему, построенную в 3 шага.

Шаг 1. Определим язык исчисления высказываний. Для этого зада-

дим символы и формулы. Символами исчисления высказываний являют-

ся.

 

1. Латинские буквы a, b,..., z, A, B..., Z и буквы с индексами, штри-

хами и т.п.

2. Символы и .

Формулы определяются следующим образом.

1. Буквы является формулами.

2. Если U и V – формулы, то ¬U и ∨UV – формулы.

3. То, что выражение A является формулой, устанавливается несколь-

кими применениями правил 1) и 2).

Это определение можно сформулировать иначе. Буквы считаем фор-

мулами шага 1. Назовем формулами шага n все формулы шага n − 1 и

формулы ¬U и ∨UV, где U и V формулы шага n − 1. Пусть Fi —множе-

ство формул шага i и F = F 1 ∪F 2 ∪.... Выражение A является формулой

тогда и только тогда, когда A ∈ F. Мы можем доказывать различные

утверждения для формул индукцией по наименьшему шагу n, на котором

получена формула.

Шаг 2. Зададим аксиомы исчисления высказываний.

Мы рассмотрим всего лишь один вид аксиомы – пропозициональные

аксиомы. Они имеют вид

¬A ∨ A, (8)

где A – произвольная формула.

Шаг 3. Зададим 4 правила вывода исчисления высказываний. Они

имеют следующий вид, где A, B, C – произвольные формулы.

Правило расширения

A

B ∨ A

(9)

Правило сокращения

A ∨ A

A

(10)

Правило ассоциативности

A ∨ (B ∨ C)

(A ∨ B) ∨ C

(11)

Правило сечения.

A ∨ B, ¬A ∨ C

B ∨ C

(12)

 

В исчислении высказываний обычно вместо слова «теорема» употреб-

ляется слова «выводимая формула». То, что формула A является выво-

димой формулой, записывается в виде

_ A

Приведем некоторые пояснения к приведенным определениям. Вместо

привычной записи U∨V использовалась запись ∨UV. Хотя в дальнейшем

мы применяем запись U ∨ V, но всегда подразумеваем вместо нее запись

∨UV. При определении формулы не использовались скобки.Оказывает-

ся, что мы сможем обойтись без употребления скобок. Для наглядности

мы будем использовались скобки, например, записывать (A∨B). Однако

под этой записью понимаем A ∨ B.

Запись F = A 1 ∨ A 2 ∨... ∨ An подразумевает правостороннюю рас-

становку скобок, а именно, сборку формулы F в виде F = A 1 (A 2

... (An− 1 ∨ An)).

При определении формулы мы не использовали также знаки , , .

Определяемые символы. В математике и других дисциплинах посто-

янно встречаются символы, которые служат для обозначения некоторой

последовательности символов. Это определяемые символы. Обозревая

формулу с определяемыми символами мы должны представить ее как

формулу с исходными символами, которая получена заменой определя-

емых символов на то, что они изображают. Введем следующие определя-

емые символы

→, ∧, ↔

• A → B является обозначением для ¬A ∨ B,

• A ∧ B является обозначением для (¬A∨ ¬B),

• A ↔ B является обозначением для (A → B) (B → A).

Отметим еще раз, что обозревая формулу с определяемыми символами

мы должны представить на ее месте формулу с исходными символами.

Например, длина формулы A → B равна 4, так как в нее входит 4 символа

¬, A, ∨, B, а не 3 символа A, →, B.




Дата добавления: 2015-01-12; просмотров: 56 | Поможем написать вашу работу | Нарушение авторских прав




lektsii.net - Лекции.Нет - 2014-2024 год. (0.013 сек.) Все материалы представленные на сайте исключительно с целью ознакомления читателями и не преследуют коммерческих целей или нарушение авторских прав