Определение теории первого порядка

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

система Т такая, что:

• языком формальной системы является язык первого порядка;

• аксиомами формальной системы являются логические аксиомы

языка теории T и некоторые другие аксиомы, называемые нелоги-

ческими аксиомами;

• правилами вывода формальной системы являются правило расши-

рения, правило сокращения, правило ассоциативности, правило се-

чения и правило ∃ введения.

Теперь разъясним эти понятия подробно.

Язык первого порядка. Чтобы задать язык первого порядка нужно

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

Символами языка первого порядка является:

1. переменные x, y, z, x_, y_, . . . , x1, y1, z1, . . . ;

2. n-арные функциональные символы f, g,h, . . . и n-арные предикат-

ные символы p, q, r, . . ., где n _ 0;

3. символы ￢, ∨, ∃.

Следующие символы называются

логическими символами: переменные, знаки ￢, ∨, ∃ и знак =.

Функциональные и предикатные символы, отличные от знака =, являют-

ся нелогическими символами. Они зависят от теории. Логические сим-

волы одни и те же во всех теориях. У каждой теории свой, индивидуаль-

ный набор функциональных и предикатных символов, отражающих поня-

тия данной теории. Число n-арных функциональных и предикатных сим-

волов для данного n произвольно и в, частности, может равняться 0. Од-

нако среди предикатных символов должен быть символ =.

Рассмотрим предназначение каждого типа знаков.

Символ = будет использоваться для обозначения равенства. Пере-

менные служат для обозначения произвольных объектов теории T. На-

пример, x может означать в арифметике число, в геометрии вектор, пря-

мую и т.п. Функциональные символы является знаками для обозначения

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

дикатов.

Рассмотрим на примере арифметики необходимость каждого из трех

типов знаков. Допустим, что мы описываем свойства натуральных чисел,

относящиеся к сложению, умножению, отношению > и отношению «сле-

довать за». Тогда мы запишем следующую систему аксиом.

N1. Sx _= 0. N6. x · Sy = (x · y) + x.

N2. Sx = Sy → x = y. N7. ￢(x < 0).

N3. x + 0 = x. N8. x < Sy ↔ x < y ∨ x = y.

N4. x + Sy = S(x + y). N9. x < y ∨ x = y ∨y < x.

N5. x · 0 = 0.

Смысл некоторых выражений уточним ниже, а пока рассмотрим симво-

лы, которые нам потребовались. Мы использовали следующие логиче-

38

ские символы: переменные x, y, знаки ￢, ∨ и знак = . Нелогические сим-

волы следующие: унарный функциональный символ S для обозначения

функции следования, бинарные функциональные символы + и · для вы-

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

< для выражения понятия меньше, константа 0 для обозначения конкрет-

ного элемента.

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

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

Рассмотрим вначале пример, а затем точное определения формулы.

Пример. Рассмотрим формулу N2: Sx = Sy → x = y, изображающую

следующее свойство. Если последующее число для x равно последующе-

му числу для y , то число x равно числу y.

Построение формулы начинается следующим образом: рассматрива-

ется x - это переменная, она предназначена для обозначения конкретных

натуральных чисел. Переменная x— это терм. Далее используем знак S

- это знак для функции «последующий элемент». Выражение Sx — это

терм. Терм изображает значение функции S от элемента x. Заметим, что

вместо традиционного S(x) мы записываем это выражение без скобок.

Дадим точное определение терма.

1. Переменная является термом;

2. если u1, . . .un —термы и f —n-арный функциональный символ, то

fu1u2 . . .un —терм;

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

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

Скобки и запятые отсутствуют среди символов теории первого поряд-

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

дем употреблять запись f(u1, u2, . . ., un), подразумевая вместо нее запись

fu1u2 . . .un.

Отдельный нульарный функциональный символ - это терм. Действи-

тельно, выражение fu1u2 . . .un при n = 0 имеет вид f. Нульарный функ-

циональный символ f можно отождествить с некоторым предметом, т.к.

значение функции от 0 переменных не может изменяться. Символ 0 в N1

– это терм.

Вернемся к рассмотрению предыдущего примера – формулы из N2

Sx = Sy → x = y отражающей мысль: если объект Sx совпадает с объ-

39

ектом Sy, т.е. последующий элемент за x равен последующему элементу

за y, то x = y. Эта формула построена в несколько шагов сборки 1–5.

1. Рассмотрим переменную x. Это – терм.

2. Рассмотрим переменную y. Это – терм.

3. Рассмотрим выражение Sx, образованное из унарного предикатного

символа y и ранее построенного терма x. Это выражение – терм.

4. Возьмем Sy. Это выражение – терм.

5. Рассмотрим символ бинарный предикатный символ =. Построим

выражения Sx = Sy и x = y. Эти выражения является атомными

формулами. Построим окончательное выражение Sx = Sy → x = y.

с помощью определяемого знака →. Это выражение является фор-

мулой, но не атомной формулой.

Введем точные определения атомной формулы и формулы в языке 1-го

порядка.

Атомной формулой называется выражение вида pu1u2 . . .un, где

p—n-арный предикатный символ, u1, . . . , un—термы.

Определение формулы.

1. Атомная формула является формулой.

2. Если A и B - произвольные формулы, то ￢A, ∨AB - формулы.

3. Если A - формула, то ∃xA - формула.

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

лучено несколькими применениями правил 1-3.

Задание символов и формул, полностью определяет язык 1-го порядка.

Отметим, что в пункте 2 речь идет о способе построении формул таком

же, как в исчислении высказываний. В пункте 3 добавляется новая кон-

струкция ∃xA.Она предназначена для отражения высказываний следую-

щего вида : существует x, для которого верно A. Например (∃x x2 > 4)

существует число с условием x2 > 4).

Соглашения о записях. Мы продолжаем использовать соглашения

из исчисления высказываний: вместо ∨AB для удобства восприятия за-

писываем A ∨ B, применяем определяемые знаки →,↔, ∧ и т.п. Со-

храняем соглашение о скобках из исчисления высказываний. Заметим,

40

что у нас нет квантора ∀. Это обусловлено следующей равносильностью:

∀x P(x) ≡ ￢∃x￢P(x), рассматривавшейся во вводном курсе математи-

ки. Поэтому ∀ – определяемый знак и запись ∀xP(x) является сокраще-

нием для записи ￢∃x￢P(x).

Вместо puv и fuv где p - бинарный предикатный символ, а f - бинар-

ныйфункциональный символ, записываем upv, и ufv.Кроме того, форму-

лу ￢upv будем записывать перечеркивая знак p, например, Sx _= 0 изоб-

ражает формулу ￢Sx = 0.