Понятие о формальных системах

1. Лекция 11. Понятие о формальных системах

Содержание лекции:
1.
2.
3.
Определение формальной системы
Понятия языка и метаязыка
Примеры формальных систем
Понятие о формальных системах
© Н.М. Светлов, 2006-2010
1/19

2. Литература

1. Определение формальной
системы
Формальную систему образуют:
Алфавит
Синтаксис
Аксиоматика
• Рекурсивно
перечислимый
набор
произвольных
символов
• Рекурсивно
перечислимое
непустое
множество
правил
построения
формул (слов) из
символов
алфавита
• Конечное
непустое
множество
формул (слов),
называемых
аксиомами
Понятие о формальных системах
© Н.М. Светлов, 2006-2010
Множество
продукционных
правил
• Должно быть
рекурсивно
перечислимым и
не пустым
3/19

3. 1. Определение формальной системы

Формальная система – это неинтерпретированное исчисление, предполагающее подразделение
символьных последовательностей на классы
теорем и нетеорем
Исчисление – это основанный на чётко
сформулированных правилах формальный
аппарат оперирования со знаками определённого
вида, позволяющий дать исчерпывающе точное
описание некоторого класса задач
Понятие о формальных системах
© Н.М. Светлов, 2006-2010
Формальная система –
это совокупность
абстрактных объектов
(символов), для которой
определены правила
оперирования данными
символами вне
зависимости от их
возможного смысла
4/19

4. 1. Определение формальной системы

Примеры алфавита
1. {а,б,в,г,д,е,ё,ж,з,и,й,к,л,м,н,о,п,р,с,т,у,ф,х,ц,ч,
ш,щ,ъ,ы,ь,э,ю,я}
2. { , , , , }
3. {1,2,3,4,5,6,7,8,9,0,(,),+,-,*,/}
4. Код ANSI
Понятие о формальных системах
© Н.М. Светлов, 2006-2010
5/19

5. 1. Определение формальной системы

Пример синтаксиса
Используется алфавит {1,2,3,4,5,6,7,8,9,0,(,),+,-,*,/}
‹Цифра› ::= 1|2|3|4|5|6|7|8|9|0
‹ПоложительноеЧисло› ::=
‹Цифра›|‹Цифра›‹ПоложительноеЧисло›
‹ОтрицательноеЧисло› ::=
-‹ПоложительноеЧисло›
‹Число› ::= ‹ПоложительноеЧисло›|
‹ОтрицательноеЧисло›
‹Оператор› ::= +|-|*|/
‹Выражение› ::= ‹Число›|(‹Выражение›)|
‹Выражение›‹Оператор›‹Выражение›
Понятие о формальных системах
© Н.М. Светлов, 2006-2010
6/19

6. 1. Определение формальной системы

Примеры аксиом
© Н.М. Светлов, 2006-2010
Понятие о формальных системах
1. ‹Число›*1 = ‹Число›
2. ‹Число›*0 = 0
3. ‹Число›+0 = ‹Число›
Такими аксиомами можно дополнить теорию
чисел (формальную арифметику)
4. ‹Число›/0 = ‹Число›
Может ли теория чисел содержать такую
аксиому?
Правильный ответ – ДА. У неё
всего лишь изменился алфавит.
A B, В C AПонятие
Cо формальных
x ·z+y
·z (x+y)·z
системах
(с) Н.М. Светлов, 2006
7/19

7. 1. Определение формальной системы

2. Понятия языка и метаязыка
(Формальный) язык образуют:
алфавит
синтаксис
В более узком смысле понятие языка включает:
алфавит
синтаксис
класс интерпретации
формул (слов)
Язык A, с помощью которого (на котором) описывается язык B, называется
метаязыком языка B.
Если язык B является языком формальной системы F (то есть имеет общие с нею
алфавит и синтаксис), то язык A называют метаязыком формальной системы F.
Понятие о формальных системах
© Н.М. Светлов, 2006-2010
8/19

8. 2. Понятия языка и метаязыка

• Использованные выше символы
{ , } (при задании алфавита)
::= | ‹ › (при задании синтаксиса)
(при задании продукционных правил) –
это символы метаязыка,
то есть языка, используемого для задания
(описания) другого языка или формальной
системы
Понятие о формальных системах
© Н.М. Светлов, 2006-2010
9/19

9. 2. Понятия языка и метаязыка

3. Примеры формальных систем
Пример 1
• Алфавит
{а, b, #}
• Синтаксис формул
‹Формула› ::= а|b|#
‹Формула› ::= ‹Формула›‹Формула›
• Аксиома
а#а
• Продукционные правила
x#y bx#yb
Некоторые теоремы:
а#а ba#аb bba#аbb bbba#аbbb …
Понятие о формальных системах
© Н.М. Светлов, 2006-2010
10/19

10. 3. Примеры формальных систем

Пример 2
• Алфавит
Теоремы:
MI
(2) MII
(2) MIIII
(1) MIIIIU
(3) MIUU
(2) MIUUIUU
…
{M, I, U}
Синтаксис формул
‹Формула› ::= M|I|U
‹Формула› ::=
‹Формула›‹Формула›
Аксиома
Задача:
MI
Продукционные правила
1.
2.
3.
4.
xI xIU
Mx Mxx
xIIIy xUy
xUUy xy
определить, является ли
теоремой формула MU.
Понятие о формальных системах
© Н.М. Светлов, 2006-2010
11/19

11. 3. Примеры формальных систем

Пример 3: исчисление
высказываний
• Алфавит
–
–
A1 = {p, q, …, z, pp, рq, … zz,
ppp, …}
A2 ={ , , (, )}
Синтаксис формул
‹Формула› ::= a | a A1
‹Формула› ::= (‹Формула›)
‹Формула› ::= ‹Формула›
‹Формула› ::=
‹Формула› ‹Формула›
Аксиомы
1. (a (b a))
2. (a (b c)) ((a b) (b c))
3. ( a b) (a b)
Продукционное правило
a
a b
b
Данная формальная система позволяет
рекурсивно перечислить все
возможные модели тождественноистинных высказываний, то есть
отражает законы дедуктивного
рассуждения
Понятие о формальных системах
© Н.М. Светлов, 2006-2010
12/19

12. 3. Примеры формальных систем

Исчисление высказываний (продолжение)
Пусть a b (a b), a b ( a b)
Тогда законы Аристотеля
–
–
–
закон тождества p p
закон исключения третьего p p
закон противоречия (p p)
являются теоремами исчисления высказываний
Исчисление высказываний:
непротиворечиво (в том смысле, что если p – теорема, то p – заведомо нетеорема)
полно (высказывание тождественно-истинно тогда и только тогда, когда оно является
теоремой исчисления высказываний)
разрешимо (существует конечный алгоритм доказательства того, что формула является
нетеоремой, именно: чтобы доказать, что p – нетеорема, достаточно доказать теорему
p)
Понятие о формальных системах
© Н.М. Светлов, 2006-2010
13/19

13. 3. Примеры формальных систем

Пример 4: исчисление предикатов первого порядка
• Получается из исчисления высказываний:
– введением в алфавит новых символов для обозначения
• констант
• предикатов
• квантора всеобщности
в дополнение к символам пропозициональных
переменных и логических операций
– дополнением синтаксиса:
предикатами, характеризуемыми арностью
конструкциями для квантификации пропозициональных
переменных
Понятие о формальных системах
© Н.М. Светлов, 2006-2010
14/19

14. 3. Примеры формальных систем

Пример 4: исчисление предикатов первого порядка
(продолжение)
– введением двух(+) новых аксиом
• (( t)B(t)) В(u)
– «аксиома спецификации»
• ( t)(a b) (a ( t)b) [при условии, что t не входит в a в качестве
свободной (неквантифицированной) переменной]
– введением нового продукционного правила
• a ( t)a
– «обобщение»
Понятие о формальных системах
© Н.М. Светлов, 2006-2010
15/19

15. 3. Примеры формальных систем

Свойства исчисления предикатов I порядка:
–
непротиворечивость
–
полнота
–
из пары p и p только одна может быть теоремой
одна из формул p и p является теоремой
полуразрешимость
существует алгоритм, доказывающий любую наперёд заданную теорему за
конечное число шагов
–
если заданная алгоритму формула не является теоремой, то такой алгоритм может никогда не достичь
команды завершения вычислений
не существует алгоритма, способного, доказывая теоремы одну за другой, на
каком-либо конечном шаге доказать любую из них
Исчисление предикатов I порядка является универсальным
метаязыком
–
–
его формулы могут интерпретироваться как определения алфавита,
синтаксиса, аксиоматики и продукционных правил
с помощью его формул может быть описана любая формальная система,
включая само исчисление предикатов и системы более высоких
порядков
Существуют и другие универсальные метаязыки
Понятие о формальных системах
© Н.М. Светлов, 2006-2010
16/19

16. 3. Примеры формальных систем

Исчисление предикатов I порядка является универсальным метаязыком
• его формулы могут интерпретироваться как определения алфавита, синтаксиса,
аксиоматики и продукционных правил
• с помощью его формул может быть описана любая формальная система, включая само
исчисление предикатов и системы более высоких порядков
Существуют и другие универсальные метаязыки
• Формальные системы, содержащие пять аксиом
исчисления предикатов первого порядка, называются
ф.с. первого порядка
• Ф.с., отвечающие условиям ф.с. I порядка и
допускающие квантификацию предикатов, называются
ф.с. II порядка
и т.д.
• Ф.с., отвечающие условиям ф.с. II порядка и
допускающие квантификацию метапредикатов,
называются ф.с. III порядка
Понятие о формальных системах
© Н.М. Светлов, 2006-2010
17/19

17. 3. Примеры формальных систем

1. Пример
первое свойство
нуля (сумма
числа и нуля равна числу);
5 – теория
чисел
2. второе свойство нуля (произведение числа и нуля равно нулю);
• Основана на исчислении предикатов первого порядка
3. третье свойство нуля (нуль не является следующим по отношению к
числу);
•какому-либо
Алфавит
пополняется символами 0, next, +, *, =
4. первое свойство единицы (увеличение слагаемого на единицу влечёт
•увеличение
Аксиоматика
пополняется девятью(+) аксиомами:
суммы на единицу);
5. второе свойство единицы (увеличение множителя на единицу влечёт
увеличение произведения на величину другого множителя);
6. если числа, следующие за некоторыми
числами a и b, (
равны
( a)( b)a+
a)( друг
b)(a=b)
другу, то сами числа a и b также равны;
(next(b))=next(a+b)
(next(a)= next(b))
7. если два числа равны друг другу, то равны между собой и следующие
за ними числа;
( a)( b)a*
( a)( b)( c)(a=b)
8. транзитивность равенства;
((a=c) (b=c))
(next(b))=a*b+a
9. правило математической индукции: если некоторое утверждение A
имеет место
к числу
0, а из
его истинности
для a)(A(a)
( a) по отношению
( a)(
b)(next(
a)=
(A(0),(
некоторого
его же
истинность
числа, то
b)) (
a=b) для следующего
A(next(a)))) (
a)A(a)
̚ (next(aчисла
))=0 следуетnext(
данное утверждение истинно для любого числа.
( a)a+0=a
( a)a*0=0
Понятие о формальных системах
© Н.М. Светлов, 2006-2010
Мат. индукция
18/19

18. 3. Примеры формальных систем

Теория чисел обладает следующими свойствами:
–
–
–
непротиворечивостью
неполнотой (пусть p – формула теории чисел; тогда существуют такие p, что
ни p, ни p не являются теоремами)
неразрешимостью (теоремы перечислить невозможно)
Теория чисел является универсальным метаязыком
–
т.к. она является обобщением исчисления предикатов I порядка
–
–
содержит все формулы и.п.Iп.
множество теорем теории чисел содержит все теоремы и.п.Iп.
Теория чисел содержится в более мощных ф.с.:
–
–
–
–
–
–
алгебра
линейная алгебра
дифференциальное исчисление
теория групп
топология
…
Понятие о формальных системах
© Н.М. Светлов, 2006-2010
19/19