Числа, множества и списки
По-видимому, числа представляют собой наиболее яркий пример того, как может быть построена крупная теория из крошечного ядра аксиом. В этом разделе будет описана теория натуральных чисел, или неотрицательных целых чисел. Для этого потребуется предикат NatNum, который будет принимать истинное значение при использовании параметра, представляющего собой натуральное число; кроме того, требуется один константный символ, 0, и один функциональный символ, 5 (successor — преемник). Аксиомы Пеано определяют натуральные числа и операцию сложения8. Натуральные числа определяются рекурсивно:
NatNum{0)
Vn NatNum(n) => NatNum(S{n) )
Это означает, что 0 — натуральное число и для каждого объекта л, если п — натуральное число, S(n) — натуральное число. Поэтому натуральными числами являются 0, 5(0), 5(5(0)) и т.д. Необходимы также аксиомы для ограничения действия функции определения преемника:
Vn 0 S{n)
\/т,п т Ф п => S{m) Ф S(n)
Теперь мы можем определить операцию сложения в терминах функции определения преемника:
V.m NatNum(m) => +(0,т) - т
\/т,п NatNum{m) л NatNum(n) => +(S(m),n) = S(+(m,n))
В первой из этих аксиом утверждается, что сложение числа 0 с любым натуральным числом т приводит к получению самого числа т. Обратите внимание на использование бинарного функционального символа " + " в терме + (0, т); в обычной математике такой терм принято записывать в виде 0+т с использованием инфиксной системы обозначений. (Система обозначений, которая используется в этом разделе для логики первого порядка, называется префиксной.) Чтобы было удобнее читать высказывания, касающиеся чисел, здесь будет также разрешено использовать инфиксные обозначения. Кроме того, мы можем записывать как S(n) как п+1, поэтому вторая аксиома принимает следующий вид:
\/т,п NatNum{m) л NatNum(n) => (/п+1) +п = (т+п) + 1
Эта аксиома сводит сложение к повторному применению функции определения преемника.
Такое использование инфиксных обозначений представляет собой пример применения синтаксического упрощения, т.е расширения или сокращения стандартного синтаксиса, при котором семантика не изменяется. Любое высказывание, в котором используются такие сокращения, может быть "разупрощено" для получения эквивалентного высказывания в обычной логике первого порядка.
После определения понятия сложения становится простой задача определения умножения как повторного сложения, возведения в степень как повторного умножения, целочисленного деления и определения остатков от деления, формулировки понятия простых чисел и т.д. Таким образом, вся теория чисел (включая такие ее приложения, как криптография) может быть сформирована на основе одной константы, одной функции, одного предиката и четырех аксиом.
Проблемная область множеств также является фундаментальной не только для математики, но и для рассуждений на уровне здравого смысла. (В действительности на основе теории множеств может быть также построена теория чисел.) Необходимо иметь возможность представлять отдельные множества, включая пустое множество. Кроме того, требуется способ составления множеств с помощью добавления элемента к множеству или применения операции объединения или пересечения к двум множествам. К тому же необходимо знать, входит ли некоторый элемент в состав множества, и иметь возможность отличать множества от объектов, не являющихся множествами.
В качестве синтаксического упрощения в данном разделе будет использоваться обычный словарь теории множеств. Пустое множество представляет собой константу, которая записывается как {}. Применяется также один унарный предикат, Set, который принимает истинное значение, если его фактическим параметром является множество. Бинарными предикатами являются х е s (х — элемент множества S) и SI с s2 (sx — подмножество, не обязательно строгое, множества S2). В качестве бинарных функций применяются s± n s2 (пересечение двух множеств), s± u S2 (объединение двух множеств) и {х| S} (множество, полученное в результате присоединения элемента х к множеству s). Один из возможных наборов аксиом приведен ниже.
1. Единственными множествами являются пустое множество и множества, по-
лученные путем присоединения некоторого элемента к множеству.
Vs Set(s) <=> (s = {}) v (Vx,s2 Set(s2) л s = {x\s2})
2. Пустое множество не имеет присоединенных к нему элементов, иными сло-
вами, не существует способа разложения множества Empty Set на меньшее
множество и еще один элемент:
-,Vx,s {х| S} = {}
3. Присоединение к множеству элемента, уже имеющегося в этом множестве, не
оказывает никакого эффекта:
Vx, s х G s <=> s = {x\s}
4. Единственными элементами множества являются элементы, которые были к
нему присоединены. Мы выразим эту мысль рекурсивно, утверждая, что х —
элемент множества s тогда и только тогда, когда s эквивалентно некоторому
множеству s2, к которому присоединен некоторый элемент у, где либо у сов-
падает с х, либо хявляется элементом s2:
Vx, s х е s <=» [Vy, s2 (s = {y| s2] л (x = у v x e s2) ) ]
5. Множество является подмножеством другого множества тогда и только тогда, когда все элементы первого множества являются элементами второго множества: Vsi,s2 si С s2 <=» (Vx х 6 si => x 6 s2)
6. Два множества равны тогда и только тогда, когда каждое из них является подмножеством другого:
Vsi/s2 (Si = S2) <=> (Si С S2 Л S2 С Si)
7. Некоторый объект принадлежит к пересечению двух множеств тогда и только
тогда, когда он является элементом обоих этих множеств:
Vx, Si,S2 х е (Si n s2) <=> (x 6 Si Л X 6 s2)
8. Некоторый объект принадлежит к объединению двух множеств тогда и только
тогда, когда он является элементом того или другого множества:
Vx, si,s2 х е (si u s2) <=> (x e si v x e s2)
Списки подобны множествам. Различия между ними состоят в том, что списки упорядочены, а один и тот же элемент может появляться в списке несколько раз. Для списков может использоваться словарь ключевых слов Lisp: Nil — это список-константа без элементов; Cons, Append, First и Rest — функции; Find — предикат, который выполняет для списков такие же функции, какие Member выполняет для множеств. List? — предикат, принимающий истинное значение только при получении параметра, представляющего собой список. Как и в случае множеств, обычно принято использовать синтаксические упрощения в логических высказываниях, в которых применяются списки. Пустой список обозначается как [ ]. Терм Cons (х, у), где у— непустой список, записывается как [х|у]. Терм Cons(х,Nil) (т.е. список, содержащий только элемент х) записывается как [х]. Список из нескольких элементов, такой как [А, в, С], соответствует вложенному терму Cons (A, Cons {Bf Cons (С, Nil))). В упр. 8.14 предлагается составить аксиомы для списков.