новости  материалы  справочник  форум  гостевая  ссылки Поиск с Яндексом  
Новости
Материалы
  Логические подходы
  Нейронные сети
  Генетические алгоритмы
  Разное
  Публикации
  Алгоритмы
  Применение
Справочник
Форум
Гостевая книга
Ссылки
О сайте
 

Логика предикатов


Источник: http://www.isu.ru/~slava/do/disc/predlog.htm
Курс: Дискретная математика



Понятие "предикат" обобщает понятие "высказывание". Неформально говоря, предикат – это высказывание, в которое можно подставлять аргументы. Если аргумент один – то предикат выражает свойство аргумента, если больше – то отношение между аргументами.

Пример предикатов. Возьмём высказывания: "Сократ - человек", "Платон - человек". Оба эти высказывания выражают свойство "быть человеком". Таким образом, мы можем рассматривать предикат "быть человеком" и говорить, что он выполняется для Сократа и Платона.

Возьмём высказывание: "расстояние от Иркутска до Москвы 5 тысяч километров". Вместо него мы можем записать предикат "расстояние" (означающий, что первый и второй аргумент этого предиката находятся на расстоянии, равном третьему аргументу) для аргументов "Иркутск", "Москва" и "5 тысяч километров".

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

Пример рассуждения, не выразимого в логике высказываний. Все люди смертны. Сократ - человек. Следовательно, Сократ смертен.

Это рассуждение на языке логики высказываний можно записать тремя отдельными высказываниями. Однако никакой связи между ними установить не удастся. На языке логики предикатов эти предложения можно выразить с помощью двух предикатов: "быть человеком" и "быть смертным". Первое предложение устанавливает связь между этими предикатами.

Перейдём теперь к формальному изложению логики предикатов.

Язык логики предикатов

"Предикатные формулы" обобщают понятие пропозициональной формулы, определённое в части 2.

Предикатная сигнатура – это множество символов двух типов – объектные константы и предикатные константы – с неотрицательным целым числом, называемым арностью, назначенным каждой предикатной константе. Предикатную константу мы будем называть пропозициональной, если её арность равна 0. Пропозициональные константы являются аналогом атомов в логике высказываний. Предикатная константа унарна, если её арность равна 1, и бинарна, если её арность равна 2. Например, мы можем определить предикатную сигнатуру
{ a, P, Q } (4)
объявляя a объектной константой, P – унарной предикатной константой, и Q – бинарной предикатной константой.

Возьмём предикатную сигнатуру s, которая включает по крайней мере одну предикатную константу и не включает ни одного из следующих символов:

  • объектные переменные x, y, z, x1, y1, z1, x2, y2, z2, ...,
  • пропозициональные связки,
  • квантор всеобщности " и квантор существования $,
  • скобки и запятая.
Алфавит логики предикатов состоит из элементов из s и четырёх групп дополнительных символов, указанных выше. Строка – это конечная последовательность символов из этого алфавита.

Терм – это объектная константа или объектная переменная. Строка называется атомарной формулой, если она является пропозициональной константой или имеет вид R(t1, ..., tn), где R – предикатная константа арности n (n > 0) и t1, ... , tn – термы. Например, если мы рассматриваем сигнатуру (4), то P(a) и Q(a, x) – атомарные формулы.

Множество X строк замкнуто относительно правил построения (для логики предикатов), если

  • каждая атомарная формула принадлежит X,
  • для любой строки F если F принадлежит X, то ¬F тоже принадлежит,
  • для любых строк F, G и любой бинарной связки Д, если F и G принадлежат X, то также принадлежит (F Д G),
  • для любого квантора K, любой переменной v и любой строки F если F принадлежит X, то также принадлежит Kv F.
Строка F является (предикатной) формулой, если F принадлежит всем множествам, которые замкнуты относительно правил построения.

Например, если рассматриваемая сигнатура есть (4), тогда

(¬P (a) Ъ $ x(P (x) & Q(x, y)))
– формула.

3.1 Является ли " x формулой?

Как и в логике высказываний можно доказать, что множество формул замкнуто относительно правил построения. Теоремы возможности и единственности разбора подобны соответствующим теоремам для пропозициональных формул.

В случае предикатных формул доказательство по структурной индукции имеет следующий вид. Для данного свойства формул мы проверяем, что

  • каждая атомарная формула обладает этим свойством,
  • для любой формулы F, обладающей этим свойством, ¬F также обладает этим свойством,
  • для любых формул F, G, обладающих этим свойством, и любой бинарной связки Д, (F Д G) также обладает этим свойством,
  • для любого квантора K, любой переменной v и любой формулы F, обладающей этим свойством, Kv F также обладает этим свойством.
Тогда это свойство выполняется для всех формул.

3.2 Если формула содержит квантор, тогда она содержит переменную. Верно или нет ?

3.3 Если формула содержит квантор, тогда она содержит скобки. Верно или нет ?

При записи предикатных формул мы будем опускать некоторые скобки и применять другие сокращения, введённые в части 2. Строку вида

" v1 ··· " vn (n і 0)
будем писать как " v1 ··· vn, и подобным образом для квантора существования.

Свободные и связанные переменные

Множество свободных переменных формулы F определяется рекурсивно, следующим образом:

Определение 22 (Свободные переменные).

  • Все переменные, входящие в атомарную формулу, являются свободными переменными этой формулы,
  • свободные переменные формулы F являются свободными переменными формулы ¬F,
  • переменные, являющиеся свободными для хотя бы одной из формул F или G, являются свободными переменными формулы (F Д G),
  • все свободные переменные формулы F кроме v являются свободными переменными формулы Kv F.

Определение 23 (Замкнутая формула). Формула без свободных переменных называется замкнутой формулой, или предложением.

Определение 24 (Связаная переменная). Переменная v связана в формуле F, если F содержит вхождение Kv, где K – квантор.

3.4 Найдите свободные переменные и связанные переменные формулы

$ y P(x, y) & ¬$ x P (x, x)

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

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

В этих упражнениях для перевода рассматривается сигнатура (4). Мы предполагаем, что объектные переменные служат для обозначения натуральных чисел и интерпретируем сигнатуру следующим образом:

  • a представляет число 10,
  • P(x) выражает условие "x является простым числом",
  • Q(x, y) выражает условие "x меньше чем y".

В каждой из следующих задач представьте данное предложение русского языка предикатной формулой.

3.5 Все простые числа больше чем x.

Ответ: " y(P (y) Й Q(x, y)).

3.6 Существует простое число, которое меньше чем 10.

3.7 x равно 2.

3.8 x равно 11.

3.9 Существует бесконечно много простых чисел.

Подстановка

Определение 25 (Подстановка терма). Пусть F – формула и v – переменная. Результат подстановки терма t вместо v в F – формула, определённая рекурсивно следующим образом:

  • результат подстановки t вместо v в атомарную формулу F получается из F одновременной заменой всех вхождений v на t,
  • если результат подстановки t вместо v в F есть F' тогда результат подстановки t вместо v в ¬F есть ¬F',
  • если результат подстановки t вместо v в F и G есть F' и G' тогда результат подстановки t вместо v в (F Д G) есть (F'Д G'),
  • если результат подстановки t вместо v в F есть F' и w – переменная, отличающаяся от v, тогда результат подстановки t вместо v в Kw F есть Kw F',
  • результат подстановки t вместо v в Kv F есть Kv F.

3.10 Найдите результат подстановки константы a вместо x в формулу из задачи 3.4.

Когда мы намереваемся рассмотреть подстановки вместо переменной v в некоторую формулу, удобно обозначать эту формулу выражением F(v), и обозначать результат подстановки терма t вместо v в этой формуле через F(t) .

3.11 Если v не является свободной переменной F(v), тогда F(t) равно F(v).

Пусть F(x) обозначает формулу

" y (P(y) Й Q(x, y)),
предложенную выше как перевод условия "все простые числа больше чем x" (задача 3.5). Формула вида F(t), где t – терм, обыкновенно выражает то же условие применённое к значению t. Например, F(a) есть " y (P(y) Й Q(a, y)), что значит "все простые числа больше чем 10", F(z2) есть " y (P(y) Й Q(z2, y)), что значит "все простые числа больше чем z2". Существует, однако, одно исключение. Формула F(y), то есть, " y (P(y) Й Q(y, y)), выражает (неправильное) утверждение "каждое простое число меньше чем оно само". Проблема с этой подстановкой в том, что, когда мы подставляем переменную y вместо x в F(x), y "захватывается" квантором. Чтобы выразить утверждение "все простые числа больше чем y" предикатной формулой, мы будем использовать связанную переменную отличную от y и писать, например,
" z(P (z) Й Q(y, z))

Чтобы различать "плохие" подстановки, как в последнем примере, от "хороших", мы определим, когда терм t является подстановочным для переменной v в формуле F.

  • Если F – атомарная, тогда t является подстановочным для переменной v в F,
  • t является подстановочным для переменной v в ¬F тогда и только тогда, когда t является подстановочным для v в F,
  • t является подстановочным для v в (F Д G) тогда и только тогда, когда t является подстановочным для v и в F и в G,
  • t является подстановочным для v в Kw F тогда и только тогда, когда
    1. t не содержит w и является подстановочным для v в F, или
    2. v не является свободной переменной формулы Kw F.

3.12 Терм, не содержащий ни одной связанной переменной формулы F, является подстановочным в F для любой переменной.

Определение 26 (Универсальное замыкание). Универсальное замыкание формулы F – это предложение

" v1 ··· vn F,
где v1, ... , vn – все свободные переменные F.

Семантика

Семантика пропозициональных формул определяет, какое истиностное значение F I назначается пропозициональной формуле F интерпретацией I. Наша следующая цель – расширить это определение до предикатных формул. Сначала нам надо расширить определение интерпретации до предикатных сигнатур.

Интерпретация I предикатной сигнатуры s состоит из

  • непустого множества |I|, называемого пространством I,
  • элементов cI из |I| (для каждой объектной константы c из s),
  • элементов RI из множества {л,и} (для каждой пропозициональной константы R из s),
  • функций RI из |I|n в {л,и} (для каждой предикатной константы R из s арности n > 0).

Пример интерпретации. Теперь замечания, предшествующие упражнениям по переводу с русского языка, могут рассматриваться как определение интерпретации сигнатуры (4). Для этой интерпретации I
|I| = w,
a I = 10,
P I(n) =
м и, если n простое ,
н
о л, иначе,
Q I(m, n) =
м и, если m < n,
н
о л, иначе,
(5)

Семантика логики предикатов, вводимая ниже, определяет истиностное значение FI только для случая, когда F предложение. Как и в логике высказываний определение рекурсивно. Для пропозициональных констант, определять нечего: истиностное значение RI является частью интерпретации I. Для других атомарных предложений, мы можем определить

R(t1, ... , tn)I = RI(tI1, ... , tIn)
(Так как R(t1, ..., tn) – предложение, каждый терм ti является объектной константой, и, следовательно, tIi – часть I). Для пропозициональных связок, мы можем использовать те же правила, что и в логике высказываний. Но случай кванторов представляет сложность.

Рассмотрим интерпретацию I предикатной сигнатуры s. Для каждого элемента c из пространства |I|, выберем новый символ c* и добавим его в s в качестве объектной константы. Например, если s есть (4) и I есть (5), тогда расширенная сигнатура –

{a, 0*, 1*, 2*, ... , P, Q}

Интерпретация I может быть расширена до новой сигнатуры с помощью определения

(c*)I = c
для всех c О |I|.

Мы определим рекурсивно истиностное значение FI, которое назначается F интерпретацией I для каждого предложения F расширенной сигнатуры, которая включает, в частности, каждое предложение сигнатуры s . Для любой пропозициональной константы R, R I является частью интерпретации I. Иначе, мы определяем:

  • R(t1, ... , tn)I = RI(tI1, ..., tIn),
  • (¬F )I = ¬(F I),
  • (F Д G)I = Д(F I, G I) для каждой бинарной связки Д,
  • " w F(w)I = и тогда и только тогда, когда для всех c О |I|: F (c*)I = и,
  • $ w F(w)I = и тогда и только тогда, когда для некоторого c О |I|: F (c*)I = и.

Как и в логике высказываний, мы говорим, что F истинно при I и пишем I |= F, если F I = и.

3.13 Покажите, что $ x Q(x, a) истинно при интерпретации (5).

3.14 Пусть F(x) является формулой, дающей ответ на задачу 3.5 выше. Покажите, что для любого n О w, при интерпретации (5) F(n*) истинно тогда и только тогда, когда n < 2.

Выполнимость

После того, как мы определили семантику логики предикатов, определение выполнимости для логики предикатов (также как и определение логического следования в следующем пункте) совпадает с соответствующим определением для логики высказываний.

Определение 27 (Выполнимость). Если существует интерпретация, при которой предложение F истинно, мы говорим, что F выполнима. Множество G предложений выполнимо, если существует интерпретация, при которой истинны все предложения из G.

В каждой из следующих задач определите, является ли данное множество предложений выполнимым. Мы предполагаем, что P и Q – предикатные константы, арности которых будут каждый раз ясны из контекста.

3.15 P(a), $ x ¬P(x).

3.16 P(a), " x ¬P(x).

3.17 " x$ y P(x, y), " x ¬P(x, x).

Логическое следование

Множество предложений G влечёт предложение F, или формула F является логическим следствием G (символически, G |= F), если для каждой интерпретации, при которой истинны все предложения из G, F также истинно. Свойство пропозиционального следования, сформулированное в задаче 2.23, выполняется и в логике предикатов.

3.18 Определите, является ли формула

$ x (P(x) & Q(x))
логическим следствием формул
$ x P(x), $ x Q(x)

Предложение F называется тождественно истинным, если при любой интерпретации F истинно. Тождественно истинное предложение следует из любого множества предложений. Утверждение задачи 2.25 может быть расширено до логики предикатов: F следует из { G1, ... , Gn } тогда и только тогда, когда предложение (G1 & ··· & Gn) Й F тождественно истинно.

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

Выводы в логике предикатов

В логике предикатов вывод определяется так же, как и в исчислении высказываний и секвенции имеют тот же синтаксис. Аксиомы тоже определяются так же, как в логике высказываний. Все правила вывода логики высказываний – правила введения и удаления для пропозициональных связок, правила противоречия и сведения к противоречию – включены в множество правил вывода логики предикатов, с метапеременными для формул понимаемыми теперь как предикатные формулы. В дополнение, есть четыре новых правил вывода: правила введения и удаления для кванторов.

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

G |– F(v)
")
G |– " v F(v)
G |– " v F(v)
")
G |– F (t)
где v не является свободной где t является
переменной для любой формулы в G подстановочным для v в F(v)

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

3.19 (P(a) & " x (P(x) Й Q(x))) Й Q(a).

3.20 " xy P(x, y) Й " x P (x, x).

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

G |– F(t)
$)
G |– $ v F(v)
G |– $ v F(v)       G И { F(v) }|– C
$)
G |– C
где t – подстановочный где для C и любой формулы из G
для v в F(v) v не является свободной переменной

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

3.21 (P(a) Ъ P(b)) Й $ x P(x).

3.22 ¬$ x P(x) є " x ¬P(x).

Корректность и полнота логики предикатов

Множество правил вывода для логики предикатов обладает свойством корректности и полноты подобно свойствам пропозициональных выводов.

Теорема корректности. Если существует вывод замкнутой формулы F из множества формул G, тогда G влечёт F.

Теорема полноты. Для любой замкнутой формулы F и любого множества предложений G, если G влечёт F, то существует вывод F из некоторого подмножества G.

Полнота логики предикатов для случая счётного G и для другого множества правил вывода была доказана Куртом Гёделем в 1930 году.

Функциональные символы и равенство: синтаксис

Логика предикатов, определённая выше немного более ограничена, чем что обыкновенно называется "логикой первого порядка", и наша следующая цель – удалить эти ограничения. Во-первых, мы обобщим понятие терма. В дополнение к объектным константам и объектным переменным, мы разрешим построение термов с использованием символов для функций, "функциональных констант". Во-вторых, мы добавим к языку знак равенства, и уравнения будут включены как новый тип атомарных формул.

Наше наиболее общее понятие сигнатуры определяется следующим образом.

Определение 28 (Сигнатура,константы). Сигнатура – это множество символов двух типов – функциональных констант и предикатных констант – с неотрицательным целым числом, называемым арностью, связанным с каждым символом. Объектная константа – это функциональная константа арности 0. Функциональная константа унарна, если её арность равна 1, и бинарна, если её арность равна 2. Пропозициональная константы, так же как унарные и бинарные предикатные константы, определены как выше.

Определение 29 (Терм). Возьмём сигнатуру s, не включающую ни дополнительных символов, указанных в начале данной части, ни знака равенства. Множество X строк замкнуто относительно правил построения термов, если

  • каждая объектная константа принадлежит X,
  • каждая объектная переменная принадлежит X,
  • для каждой функциональной константы h арности n (n > 0) и любой строки t1, ... , tn, если t1, ... , tn принадлежит X, тогда также принадлежит h(t1, ... , tn).
Строка является термом, если она принадлежит все множествам, которые замкнуты относительно правил построения.

3.23 Каждый терм содержит объектную константу или объектную переменную. Верно или нет ?

В логике первого порядка существуют три типа атомарных формул:

  • пропозициональные константы,
  • строки вида R(t1, ... , tn) где R – предикатная константа арности n (n > 0) и t1, ..., tn – термы,
  • строки вида (t1 = t2), где t1, t2 – термы.
Взяв в качестве множества атомарных формул данное множество, мы получаем, что определение формул (первого порядка) совпадает с определением предикатных формул в начале этой части.

Для любых термов t1 и t2, t1 t2 обозначает формулу ¬(t1 = t2).

Функциональные символы и равенство: семантика

Чтобы обобщить понятие интерпретации на случай произвольной сигнатуры, нам надо сказать, как разрешено интерпретировать функциональную константу арности n > 0. Такой символ может быть интерпретирован как произвольная тотальная функция n переменных, чьи аргументы и значения принадлежат пространству интерпретации.

Определение 30 (Интерпретация сигнатуры логики предикатов). Интерпретация I сигнатуры s состоит из

  • непустого множества |I|, называемого пространством I,
  • элементов cI из |I| (для каждой объектной константы c из s),
  • функций hI из |I|n в |I| для каждой функциональной константы h из s арности n > 0,
  • элементов RI из множества {л,и} (для каждой пропозициональной константы R из s),
  • функций RI из |I|n в {л,и} (для каждой предикатной константы R из s арности n > 0).

Пример 1. Рассмотрим сигнатуру арифметики первого порядка
{ a, s, f, g }, (6)
где a – объектная константа (предназначенная для представления 0), s – унарная функциональная константа (для функции следования), и f, g – бинарные функциональные константы (для сложения и умножения). Так как эта сигнатура не включает предикатных констант, единственными атомарными формулами являются равенства. Интерпретация I сигнатуры (6) определяется следующим образом:
|I| = w,
aI= 0,
sI(n) = n + 1,
fI(m, n) = m + n,
gI(m, n) = m · n.
(7)

3.24 Выразите аксиому 1 части 1 и утверждения задач 1.1 и 1.16 замкнутыми формулами первого порядка.

Заметим, что синтаксис логики первого порядка не позволяет представить аксиому индукции и утверждения некоторых других задач из части 1, в частности, задачи 1.51.8. Аксиома индукции "говорит" про множества натуральных чисел, а задачи 1.51.8 – про функции из натуральных чисел в натуральные числа, и не существует переменных для таких объектов в языке первого порядка сигнатуры (6). "Формулы второго порядка" (не обсуждаемые здесь подробно) дают такую возможность. Кроме объектных переменных, такие формулы могут включать "предикатные переменные" и "функциональные переменные". Например, аксиома индукции может быть представлена замкнутой формулой второго порядка
" p((p(a) & " x(p(x) Й p(s(x)))) Й " x p(x)), (8)
где p – унарная предикатная переменная.

3.25 Представьте следующие предложения формулами первого порядка:

  • Существует не более одного x такого, что P(x).
  • Существует в точности один x такой, что P(x).
  • Существует по крайней мере два x таких, что P(x).
  • Существует не более двух x таких, что P(x).
  • Существует в точности два x таких, что P(x).

Чтобы определение FI было применимо в случае присутствия функциональных констант арности > 0, нам надо расширить обозначение tI с объектных констант до произвольных свободных от переменных термов сигнатуры sI, и добавить правило для равенства. Значение tI, назначенное интерпретацией I терму t, определено рекурсивно формулами

h(t1, ... , tn)I = hI (tI1, ... , tIn)
Дополнительное правило в определении значений формул при интерпретации читается следующим образом:
  • (t1 = t2)I = и тогда и только тогда, когда tI1 = tI2.

Определения значений формул при интерпретации и всех других семантических понятий, введённых выше для формул предикатной сигнатуры, применимы к формулам с функциональными константами и равенством без всяких изменений.

3.26 Для каждого из следующих предложений определите, является ли оно выполнимым:

  • a = b,
  • " xy (x = y),
  • " xy (x y).

Выводы в логике первого порядка

Определение вывода в логике предикатов с функциональными константами и равенством включает новый тип аксиом и два новых правила вывода. Правила, как и раньше, содержат метапеременные, служащие для обозначения формул и термов.

Новые аксиомы выражают рефлексивность равенства и имеют вид Ж |– t = t , где t – произвольный терм. Новые правила вывода – правила замены:

G |– t1 = t2       G |– F(t1)
(З=)
G |– F(t2)
G |– t1 = t2       G |– F(t2)

G |– F(t1)
где t1 и t2 свободные для v в F(v).

Для каждой из следующих формул найдите вывод из пустого множества посылок.

3.27 x = y Й f(x, y) = f(y, x).

см. Решение

3.28 " x $ y (y = f(x)).

3.29 $ y (x = y & y = z) Й x = z.

3.30 $ x (x = a & P (x)) є P (a).

Теории первого порядка

Теория первого порядка сигнатуры s определяется с помощью аксиом. Интерпретация, при которой истинны все аксиомы теории первого порядка G, называется моделью G. Если теория первого порядка G выполнима, мы также говорим что она непротиворечива. Логические следствия теории первого порядка называется её теоремами. Доказательство предложения F в теории первого порядка G есть вывод F из подмножества аксиом из G.

Теоремы корректности и полноты выполняются для логик предикатов с функциональными символами и равенством и могут быть сформулированы в рамках теорий первого порядка следующим образом. В соответствие с теоремой корректности, если существует доказательство предложения F в теории первого порядка G, тогда F является теоремой G. В соответствие с теоремой полноты Гёделя, обратное также верно: для любой теоремы F теории первого порядка G, существует доказательство F в G.

Однако, добавление правил вывода для кванторов второго порядка ведёт к формальной системе которая корректна, но не полна.

Пример: Теория линейного порядка

Сигнатура этой теории первого порядка состоит всего из одного символа – бинарной предикатной константы P. Мы будем писать атомарную формулу P(t1, t2) как t1 Ј t2. Аксиомы теории являются универсальным замыканием следующих формул:

  1. x Ј x.
  2. (x Ј y & y Ј z) Й x Ј z.
  3. (x Ј y & y Ј x) Й x = y.
  4. x Ј y Ъ y Ј x.
Для любых термов t1 и t2, t1 < t2 обозначает t1 Ј t2 & t1 t2.

3.31 Найдите доказательство замкнутой формулы

" xyz((x Ј y & y < z) Й x < z)
в теории линейного порядка.

3.32 Покажите, что теория линейного порядка имеет

  • модель, пространство которой состоит из одного элемента,
  • модель, пространство которой содержит более чем один элемент.

Непротиворечивая теория первого порядка G полна, если для каждой замкнутой формулы F либо F или ¬F является теоремой G.

3.33 Определите, является ли теория линейного порядка полной.

Арифметика первого порядка

Мы будем упрощать запись формул сигнатуры арифметики первого порядка (6) введением следующего обозначения: a будет записываться как 0, s(t) как t' , f(t1, t2) как t1+t2, и g(t1, t2) как t1 · t2. Аксиомы арифметики первого порядка являются универсальным замыканием следующих формул:

  1. x' 0.
  2. x'= y'Й x = y.
  3. (F(0) & " v (F(v) Й F(v'))) Й " v F(v) для любой формулы F(v).
  4. x + 0 = x.
  5. x + y'= (x + y)'.
  6. x · 0 = 0.
  7. x · y'= x · y + x.

Интерпретация (7) является моделью этой теории. Арифметика первого порядка имеет также другие модели, и некоторые из них совсем не похожи на систему натуральных чисел (задача 3.40).

В следующих формулах 1 обозначает терм 0', 2 – 0", и 4 – 0"". Через t1 Ј t2 мы обозначаем формулу $ v(t2 = t1 + v), где v – первая объектная переменная, которая не встречается в t1, t2.

В каждой из следующих задач найдите доказательство данной формулы в арифметике первого порядка.

3.34 2 4.

3.35 x' x.

3.36 x'= x + 1.

3.37 x Ј x.

Нестандартные модели арифметики

Термы 0, 0', 0", ... называются цифрами. Модель M арифметики первого порядка стандартна, если для каждого c О |M| существует цифра t такая, что tM = c.

3.38 Модель арифметики первого порядка (7) стандартна.

В соответствие с задачей 3.40, существуют модели арифметики первого порядка, которые не обладают этим свойством. Чтобы доказать существование такой модели, полезно рассмотреть следующую теорию первого порядка G. Сигнатура G получается из сигнатуры арифметики первого порядка добавлением буквы b в качестве новой объектной константы. Множество аксиом G получается из множества аксиом арифметики первого порядка добавлением формул b 0, b 0', b 0", ... в качестве новых аксиом.

3.39 G непротиворечива.

3.40 Арифметика первого порядка имеет нестандартную модель.

Существование нестандартных моделей арифметики следует из теоремы Сколема (1920), который обобщил раннюю работу Леопольда Лёвенхейма (1915). Возможность таких моделей резко контрастирует с результатом задачи 1.41. Разница связана с тем, что язык арифметики первого порядка является слишком ограниченным для выражения аксиомы индукции. "Арифметика второго порядка", в которой схема индукции заменяется по аксиоме (8), не имеет нестандартных моделей.

Теорема неполноты Гёделя

Пусть M – нестандартная модель арифметики первого порядка. Может случится что M "не отличима" от модели (7) в том смысле, что для любой замкнутой формулы F арифметики первого порядка F истинно при M тогда и только тогда, когда F истинно при (7). Но некоторые нестандартные модели не обладают этим свойством: может существовать предложение F такое, что при M предложение F истинно, а при (7) ¬F истинно. Так как и M и интерпретация (7) являются моделями арифметики первого порядка, значит ни F, ни ¬F не являются теоремами, а это означает, что арифметика первого порядка неполна. Этот факт, известный как теорема неполноты Гёделя, был доказан Куртом Гёделем в 1931 году.

Недоказуемые теоремы для диофантовых уравнений

Такое "недоказуемое утверждение" F может иметь, в действительности, очень простую логическую структуру. Существует недоказуемое утверждение, состоящее из атомарной формулы, перед которой стоит строка из кванторов существования:
$ v1 ··· vn (t1 = t2) (9)
Это утверждение выражает факт существования решения диофантова уравнения. Недоказуемость (9) означает, что уравнение не имеет решений в натуральных числах, но имеет "нестандартное решение" в некоторой нестандартной модели арифметики первого порядка.

Существование недоказуемого утверждения вида (9) было установлено Юрием Матиясевичем в 1970 году.