Всё для Учёбы — студенческий файлообменник
бесплатно
pdf

Лекции «Аксиоматическая теория Гильберта-Аккермана» по Дискретной математике (Сабуров М. А.)

М.А. Сабуров

1 Аксиоматическая система Гильберта-Аккермана

Аксиоматическая система Гильберта-Аккермана (Hilbert-Ackermann) состоит из трех

частей: 1) алфавит;

2) правила образования формул;

3) правила преобразования формул (правила образования тезисов).

1. Алфавит – список первичных понятий:

a) Прописные латинские буквы (возможно, с индексами) A, B, C, … , A1, A2, …

будут называться простыми высказываниями. Иногда их также называют

пропозициональными буквами. При этом о значениях истинности этих

высказываний речи не идет.

b) Знаки Ú и` , которые мы будем называть дизъюнкцией и отрицанием,

соответственно, или операциями. Никакого содержательного смысла этим

знакам мы не придаем.

c) Скобки ( , ) – знаки пунктуации.

2. Правила образования формул. Для удобства речи формулы будем обозначать

прописными готическими буквами: A, B, C, D и т.д.

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

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

Предметный язык надо изучать с помощью другого языка, который мы знаем. Он

называется метаязыком или языком исследователя. Естественный язык универсален –

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

должны различаться. В нашем случае метаязык состоит из естественного языка и

условных обозначений. Готические буквы суть символы метаязыка. Они вводятся для

удобства, их можно заменить словами.

a) Все простые высказывания суть формулы.

b) Если A и B – формулы, то (AÚB) – формула.

c) Если A – формула, то A – формула.

Примеры формул:

A , A , (A Ú B) , (A Ú B)

Для сокращения записи формул введем новые символы операций:

(A&B) есть сокращенная запись для (AÚB) . Назовем эту операцию

конъюнкцией.

(A⇒B) есть сокращенная запись для (AÚB) . Назовем эту операцию

импликацией. (AÛB) есть сокращенная запись для (A⇒B)&(B⇒A) (эквивалентность).

Для сокращения же условимся опускать скобки. Во-первых, опускаем внешние

скобки: вместо (AÚB) пишем AÚB, а также считаем, что знак отрицания заменяет

скобки: вместо (AÚB) ÚC пишем AÚBÚC. Во-вторых, введем понятие приоритета

операций. Будем считать, что конъюнкция связывает сильнее, чем дизъюнкция, а

дизъюнкция, в свою очередь, сильнее, чем импликация и эквивалентность. Здесь мы

несколько отступаем от Гильберта-Аккермана: у них дизъюнкция сильнее конъюнкции,

Аксиоматическая система Гильберта-Аккермана

© М.А. Сабуров, 2007 2

а импликация сильнее эквивалентности; кроме того, в их книге знак дизъюнкции

опускается, т.е. AB означает AÚB. Введенные нами правила использования скобок в

большей степени согласуются с принятыми в современной математике и потому более

привычны для нас. Итак, формула

A& B Ú C & D ⇒ E

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

(((A Ú B) Ú (C Ú D)) Ú E)

Для удобства восприятия разрешим использовать скобки разного вида (квадратные,

фигурные). 3. Правила преобразования формул.

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

формул, которые могут быть предметом нашего изучения, то правила преобразования

формул выделяют в этом множестве некоторое подмножество формул, которые мы

будем называть тезисами.

Правила преобразования формул, или правила образования тезисов, включают в себя

список первичных тезисов, или аксиом, и правила вывода.

Следующие формулы суть аксиомы:

A1: A Ú A⇒ A A2: A⇒ A Ú B

A3: A Ú B ⇒ B Ú A

A4: (A⇒ B)⇒ (C Ú A⇒C Ú B)

Правил вывода два. Первое из них – правило подстановки:

α: в тезисе можно заменить любое простое высказывание, всюду, где оно

встречается в нем, любой формулой.

Например, в тезисе A⇒ A Ú B заменим B на A и получим новый тезис: A⇒ A Ú A .

(Правило подстановки позволяет рассматривать формулы A1 – A4 как схемы

аксиом. Так, мы могли бы включить в список аксиом формулы B Ú B ⇒ B , C Ú C ⇒C

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

Второе правило вывода – правило заключения (modus ponens). Его также называют

правилом отрыва.

β: если формулы A⇒B и A суть тезисы, то B также есть тезис.

Для сокращения записи введем знак |–. С помощью этого знака правила вывода

можно записать следующим образом:

α: Φ(ω) |– Φ(A), где ω – произвольное простое высказывание, A – произвольная

формула. β: A⇒B , A |– B.

Из аксиом с помощью правил вывода можно получать новые тезисы. Так,

применение правила α к аксиоме A1 порождает тезисы B Ú B ⇒ B , C Ú C ⇒C и т.д.

Новые (вторичные) тезисы будем называть теоремами.

Теорема 1. (A⇒ B)⇒[(C ⇒ A)⇒ (C ⇒ B)]

В аксиоме A4 заменим C на C . Получим следующую формулу:

Аксиоматическая система Гильберта-Аккермана

© М.А. Сабуров, 2007 3

(A⇒ B)⇒ (C Ú A⇒C Ú B)

Заменив C Ú A на C ⇒ A , а C Ú B – на C ⇒ B , получим искомую формулу.

Заметим, что при этом пришлось добавить две пары скобок.

Кроме вторичных тезисов (теорем), можно вывести вторичные правила вывода.

Подставим в A1 вместо A формулу A. Получим AÚA⇒A. Если предположить,

что AÚA есть тезис, то, по правилу заключения, A также есть тезис. Таким образом,

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

R1: AÚA |– A Аналогичным образом из остальных аксиом можно получить еще три правила

вывода: R2: A |– AÚB

R3: AÚB |– BÚA

R4: A⇒B |– CÚA⇒CÚB

Из теоремы 1 можно вывести весьма полезное цепное правило. Подставим в теорему

1 вместо простых высказываний A, B, C некоторые формулы B, C, A соответственно,

при этом такие, что A⇒B и B⇒C суть тезисы. Получим

(B⇒C)⇒[(A⇒B)⇒ (A⇒C)]

Но поскольку B⇒C есть тезис, то по правилу β получим

(A⇒B)⇒(A⇒C) Снова замечаем, что A⇒B – также тезис, и применяем правило β. Получим новый

тезис A⇒C. Таким образом, из тезисов A⇒B и B⇒C можно вывести тезис

A⇒C: RT1: A⇒B, B⇒C |– A⇒C

Выведем еще несколько теорем.

Теорема 2. A⇒ A.

В аксиоме A2 заменим B на A: A⇒ A Ú A . Добавим аксиому A1 и применим цепное

правило: A⇒ A Ú A , A Ú A⇒ A |– A⇒ A.

Теорема 3. A Ú A .

Это ничто иное, как теорема 2, записанная без использования знака импликации.

Теорема 4. A Ú A .

Получается из теоремы 3 применением правила R3.

Теорема 5. A⇒ A.

В теореме 4 заменим A на A : A Ú A . Переписав это с учетом определения

импликации, получим A⇒ A.

Теорема 6. A⇒ A.

Аксиоматическая система Гильберта-Аккермана

© М.А. Сабуров, 2007 4

В теореме 5 заменим A на A : A⇒ A. По правилу R4 получим A Ú A⇒ A Ú A .

Далее, по теореме 4 и правилу β получим AÚ A . Применив правило R3, получим

AÚ A, что, с учетом определения импликации, можно переписать как A⇒ A.

Теорема 7. (A⇒ B)⇒(B ⇒ A) .

В теореме 5 заменим A на B : B ⇒ B . По правилу R4 получим A Ú B ⇒ A Ú B . В

аксиоме A3 заменим A на A и B на B : A Ú B ⇒ B Ú A . Применив к этим двум

тезисам цепное правило, получим A Ú B ⇒ B Ú A или, в другой записи,

(A⇒ B)⇒(B ⇒ A) .

Из теоремы 7 получается правило вывода RT7 (закон контрапозиции):

RT7: A⇒B |– B⇒A Теорема 8. A& B⇒ B & A.

В аксиоме A3 заменим A на B и B на A : B Ú A⇒ A Ú B . По закону контрапозиции

A Ú B ⇒ B Ú A. По определению конъюнкции, эту формулу можно записать как

A& B⇒ B & A.

Теорема 9. A& B ⇒ A Ú B .

В теореме 6 заменим A на A Ú B : A Ú B ⇒ A Ú B . По определению конъюнкции, это

можно переписать как A& B ⇒ A Ú B .

Теорема 10. AÚ B ⇒ A& B .

Выводится из теоремы 5 аналогично.

В качестве упражнения вывести двойственный закон Де-Моргана.

Теорема 11. A& B ⇒ A

В аксиому A2 подставим A вместо A и B вместо B :

A⇒ A Ú B По закону контрапозиции получим A Ú B ⇒ A , а из этой формулы и теоремы 6 по

цепному правилу получим A Ú B ⇒ A , что, с учетом определения конъюнкции, и

представляет собой искомую формулу.

Отсюда получаем правило вывода:

RT11: A&B |– A В качестве упражнения вывести формулу A& B ⇒ B .

Теорема 12. A Ú (B Ú C)⇒ B Ú (A Ú C)

Из аксиом A2 и A3 применением правил RT1 и α получим C ⇒ A Ú C . Затем,

дважды применив правило R4, получим сначала B Ú C ⇒ B Ú (A Ú C) , а потом

A Ú (B Ú C)⇒ A Ú (B Ú (A Ú C)) . В аксиому A3 вместо B подставим (B Ú (A Ú C)) и по

цепному правилу получим:

A Ú (B Ú C)⇒ (B Ú (A Ú C)) Ú A (*)

Аксиоматическая система Гильберта-Аккермана

© М.А. Сабуров, 2007 5

Из аксиомы A2 выводим тезис A⇒ A Ú C , а из аксиом A2 и A3 по правилам RT1 и α

выведем тезис A Ú C ⇒ B Ú (A Ú C) . Отсюда имеем A⇒ B Ú (A Ú C) . Теперь

воспользуемся правилом R4, взяв в качестве приписываемой слева формулы

заключение этой импликации:

(B Ú (A Ú C)) Ú A⇒(B Ú (A Ú C)) Ú (B Ú (A Ú C))

С помощью соответствующей подстановки в аксиому A1 и применения цепного

правила получим

(B Ú (A Ú C)) Ú A⇒ B Ú (A Ú C) (**)

Из формул (*) и (**) по цепному правилу получим искомый тезис.

Теорема 13. A Ú (B Ú C)⇒ (A Ú B) Ú C

Из аксиомы A3 применением правил R4 и α выводится тезис

A Ú (B Ú C)⇒ A Ú (C Ú B) , а из теоремы 12 заменой получим тезис

A Ú (C Ú B)⇒C Ú (A Ú B) . Отсюда по правилу RT1 имеем A Ú (B Ú C)⇒C Ú (A Ú B) .

Подстановка в аксиому A3 и применение цепного правила приведут к искомому тезису.

Для упрощения дальнейшей работы нам потребуется еще одно правило вывода. При

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

подвыражение на эквивалентное ему, и полученное таким образом выражение будет

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

сформулировано явно, однако, его можно вывести.

Будем называть формулы A и B взаимоследующими, если формулы A⇒B и

B⇒A суть тезисы. Пусть формулы A и B взаимоследующие. Тогда, по закону

контрапозиции, формулы A и B также взаимоследующие. Далее, путем подстановки

взаимоследующих формул в аксиому A4, обнаружим, что взаимоследующими будут и

формулы CÚA и CÚB, где C – произвольная формула, подставляемая в аксиому

вместо буквы C. Отсюда, используя аксиому A3 и правило RT1, видим, что формулы

AÚC и BÚC также взаимоследующие. Поскольку любая формула Φ(A), содержащая

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

последовательного применения трех правил – изображения сверху черты отрицания,

приписывания произвольной формулы слева или справа (через знак дизъюнкции), то на

каждом шаге i такого построения формулы Φi(A) и Φi(B) будут взаимоследующими, а

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

взаимоследующими:

A⇒B, B⇒A |– F(A)⇒ F(B) , F(B)⇒F(A)

Если формула Φ(A) окажется тезисом, то, по правилу заключения, Φ(B) также будет

тезисом:

R5: A⇒B, B⇒A, F(A) |– F(B)

Следует заметить, что при построении формулы Φ(A) мы не ставили никаких

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

формулой A или включать ее в качестве подформулы. Поэтому, в отличие от правила

α, можно заменять не все вхождения формулы A на взаимоследующую.

Сочетание правила R5 с аксиомой A3 представляет собой закон коммутативности

дизъюнкции, с теоремой 8 – закон коммутативности конъюнкции, а с теоремами 9 и 10

Аксиоматическая система Гильберта-Аккермана

© М.А. Сабуров, 2007 6

– закон Де-Моргана. Теоремы 5 и 6 позволяют заменять любую подформулу ее

двойным отрицанием и наоборот.

Теорема 14. (A Ú B) Ú C ⇒ A Ú (B Ú C)

Подстановка в теорему 13 дает:

C Ú (B Ú A)⇒ (C Ú B) Ú A

Применение закона коммутативности дизъюнкции дает искомый тезис.

Теоремы 13 и 14 в сочетании с правилом R5 образуют закон ассоциативности

дизъюнкции. Теорема 15. A⇒ (B ⇒ A& B)

A& B⇒ A& B A& B Ú A& B

(A Ú B) Ú A& B A Ú (B Ú A& B)

A Ú (B ⇒ A& B)

A⇒ (B ⇒ A& B) Теорема 15 дает нам еще одно правило вывода:

RT15: A, B |– A&B

Как частный случай имеем:

A⇒B, B⇒A |– AÛB

Аналогичным образом выводятся другие законы – ассоциативность конъюнкции,

законы дистрибутивности и пр.

Теперь самое время задаться следующими вопросами:

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

что нам удалось вывести некоторую формулу A и одновременно ее отрицание A?

Другими словами, является ли система Гильбера-Аккермана непротиворечивой?

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

алгебры высказываний?

3. Является ли набор аксиом A1 – A4 минимальным? Иначе говоря, можно ли какую-

либо из аксиом вывести из остальных?

Для ответа на эти вопросы мы построим интерпретацию нашей системы.

Аксиоматическая система Гильберта-Аккермана

© М.А. Сабуров, 2007 7

Исследование свойств системы Гильберта-Аккермана

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

этим исчислением и некоторой алгеброй, т.е. парой <M, S>, где M – некоторое

множество, называемое носителем, а S – набор операций (унарных и бинарных),

отображающих M или M2 в M. S называют сигнатурой алгебры.

Для интерпретации используем алгебру высказываний. Тогда носителем будет

множество {0, 1}, а сигнатурой – {` , Ú, &, ⇒, Û}. Каждой пропозициональной букве

поставим в соответствие некоторое значение истинности (0 или 1), знакам операций

исчичсления – соответствующие операции алгебры высказываний.

Покажем, что в этой интерпретации множество тезисов совпадает с множеством

тавтологий.

Легко убедиться с помощью таблиц истинности, что каждая из четырех аксиом

исчисления окажется тавтологией в этой интерпретации, независимо от выбранного

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

очевидно, также суть тавтологии. В алгебре высказываний легко доказать, что если

некоторая импликация является тавтологией, и посылка этой импликации также

является тавтологией, то и заключение этой импликации есть тавтология.

Следовательно, всякий тезис, порожденный правилом modus ponens, есть тавтология.

Итак, всякий тезис в системе Гильберта-Аккермана оказывается тавтологией при

интерпретации алгеброй высказываний.

Отсюда сразу следует непротиворечивость системы Гильберта-Аккермана. В самом

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

отрицанием A, то и A, и A будут тавтологиями, что невозможно.

Можно показать, что всякая тавтология является тезисом (доказательство этого

утверждения мы опустим).

Итак, система аксиом Гильберта-Аккермана материально полна, т.е. в ней выводима

всякая тавтология. Но вопрос о полноте можно поставить и по-другому – можно ли

пополнить имеющуюся систему аксиом новой независимой от них аксиомой, не

приходя к противоречию? Иначе говоря, является ли данная система аксиом формально

полной? Возьмем произвольную формулу, которая не выводится из аксиом A1 – A4. Тогда

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

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

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

истинное значение, подставим формулу AÚA, где A – произвольная формула, а

вместо каждого простого высказывания, принимающего ложное значение, – формулу

A&A. Полученную формулу обозначим B. Эта формула, выведенная из новой

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

нее простых высказываний. Но тогда формула B будет тавтологией и, следовательно,

выводимой из аксиом A1 – A4. Таким образом, расширенная система аксиом оказалась

противоречивой – в ней одновременно выводимы формулы B и B.

Покажем, что в противоречивой системе аксиом выводима любая формула. В самом

деле, подстановка в аксиому A2 дает формулу A ⇒ (A ⇒ B) (закон Дунса Скотта).

Пусть A – формула, выводимая вместе со своим отрицанием A. Подставим A вместо

Аксиоматическая система Гильберта-Аккермана

© М.А. Сабуров, 2007 8

A, а вместо B – произвольную формулу B. Дважды применив правило modus ponens,

получим вывод формулы B:

A, A |– B Для доказательства независимости аксиомы A1 от аксиом A2 – A4 воспользуемся

другой интерпретацией. В качестве носителя возьмем множество {0, 1, 2}. Операцию Ú

определим как умножение по модулю 4: A Ú B = A* Bmod 4. Результат этой операции

при всевозможных сочетаниях значений операндов представлен в таблице:

0 1 2 0 0 0 0 1 0 1 2

2 0 2 0 Операцию отрицания определим следующим образом:

0 = 1; 1 = 0 ; 2 = 2

Легко проверить, что в этой интерпретации аксиомы A2 – A4 принимают нулевое

значение при любых значениях букв A, B, C. Формулы, полученные по правилу

подстановки из формул, тождественно равных 0, очевидно, также будут тождественно

равны 0. Правило modus ponens также сохраняет это свойство. Таким образом,

формулы, выведенные из аксиом A2 – A4, будут тождественно равны 0. В то же время,

аксиома А1 принимает значение 2 при A=2. Следовательно, она не может быть

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

всех аксиом (для этого потребуются другие интерпретации).

Независимость аксиом друг от друга не имеет принципиального значения, однако

минимальная система представляется более изящной. В то же время, отказ от

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

Примеры других интерпретаций

«Логика лжи». Пусть простые высказывания принимают значения истины и лжи,

как и в случае интерпретацией алгеброй логики. Знаку Ú поставим в соответствие

конъюнкцию, а отрицание будет иметь обычный смысл. В такой интерпретации все

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

проверить, что подстановка и modus ponens переводят противоречие в противоречие,

т.е. все тезисы суть противоречия. Знаку импликации фактически соответствует

антиимпликация A<B, знаку конъюнкции – дизъюнкция, а эквивалентности

соответствует сложение Жегалкина. Таким образом, это двойственная логика.

Алгебра множеств. Носителем алгебры множеств является множество всех

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

множеством, или универсумом. Сигнатура включает операции объединения,

пересечения и дополнения. Знаку дизъюнкции соответствует операция объединения,

конъюнкции – пересечение, а отрицанию – дополнение. Знаки импликации и

эквивалентности не будем использовать. В этой интерпретации значения всех тезисов

совпадают с универсумом.

Аксиоматическая система Гильберта-Аккермана

© М.А. Сабуров, 2007 9

Другие системы аксиом

Аксиоматическое построение исчисления высказываний впервые было

осуществлено Готлобом Фреге в 1879 г. В его системе было две связки – импликация и

отрицание – и 6 аксиом:

1) A⇒ (B ⇒ A) (истина следует из чего угодно)

2) [A⇒ (B ⇒C)]⇒[B ⇒(A⇒C)] (правило перестановки посылок)

3) [A⇒ (B ⇒C)]⇒[(A⇒ B)⇒(A⇒C)] (самодистрибутивность импликации)

4) (A⇒ B)⇒(B ⇒ A) (закон контрапозиции)

5) A⇒ A 6) A⇒ A

В 1910 г. Рассел и Уайтхэд в своем сочинении Principa Mathematica предложили

систему аксиом, которая отличалась от системы Гильберта-Аккермана наличием

дополнительной аксиомы A Ú (B Ú C)⇒ B Ú (A Ú C) , которая, как было показано

позже, может быть выведена из других аксиом (см. теорему 12).

Система Фреге, как и система Рассела-Уайтхэда, была также впоследствии

подвергнута упрощению – Лукасевич предложил систему из трех аксиом:

1) A⇒ (B ⇒ A)

2) [A⇒ (B ⇒C)]⇒[(A⇒ B)⇒(A⇒C)]

3) (A⇒ B)⇒(B⇒ A)

Лукасевич предложил также ряд других систем, в том числе состоящих из

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

предложена Нико в 1917 г., причем в качестве единственной логической связки

использовался штрихШеффера:

(A | (B | C)) | {(E | (E | E)) | [(D | B) | ((A | D) | (A | D))]}

Правило modus ponens в этой системе имеет следующий вид:

A| (B|C) , A |– C

В книге Д. Гильберта и П. Бернайса «Основания математики» приводится система, в

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

сокращенная запись. В связи с этим аксиомы разбиты на группы, каждая из которых

«вводит» новую операцию.

I. Аксиомы для импликации.

1) A⇒ (B ⇒ A) 2) [A⇒ (A⇒ B)]⇒ (A⇒ B)

3) (A⇒ B)⇒[(B ⇒C)⇒ (A⇒C)]

II. Аксиомы для конъюнкции.

1) A& B ⇒ A 2) A& B ⇒ B

3) (A⇒ B)⇒[(A⇒C)⇒ (A⇒ B &C)]

III. Аксиомы для дизъюнкции.

Аксиоматическая система Гильберта-Аккермана

© М.А. Сабуров, 2007 10

1) A⇒ A Ú B 2) B ⇒ A Ú B

3) (A⇒C)⇒[(B ⇒C)⇒(A Ú B ⇒C)]

IV. Аксиомы для эквивалентности.

1) (AÛ B)⇒ (A⇒ B)

2) (AÛ B)⇒ (B ⇒ A)

3) (A⇒ B)⇒[(B ⇒ A)⇒(AÛ B)]

V. Аксиомы для отрицания.

1) (A⇒ B)⇒(B ⇒ A)

2) A⇒ A 3) A⇒ A

Во всех приведенных примерах действуют два правила вывода – правило

подстановки и modus ponens. Можно исключить правило подстановки, если вместо

конечного набора аксиом задать схемы аксиом, которые сразу задают бесконечное

множество аксиом:

A1: AÚA⇒A

A2: A⇒AÚB A3: AÚB⇒BÚA

A4: (A⇒B)⇒ (CÚA⇒CÚB)

Легко показать, что множество теорем такой системы совпадает с множеством

теорем системы Гильберта-Аккермана. Это верно и для всех приведенных выше

примеров систем аксиом.

Аксиоматическая система Гильберта-Аккермана

© М.А. Сабуров, 2007 11

Исчисление предикатов

Алфавит исчисления предикатов включает в себя те же символы, что и исчисление

высказываний (пропозициональные буквы, знаки операций и скобки), а также

дополнительные символы:

d) предметные переменные x, y, … , z, …;

e) предикатные переменные F1, G1, H1 , … , F2, G2, H2, …;

f) кванторы ", $ .

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

числом мест.

Правила образования формул также расширим:

a) Все простые высказывания суть формулы.

b) Если Fn – n-местная предикатная переменная, а x1,…,xn суть предметные

переменные, то Fn (x1,…,xn) – формула; при этом предметные переменные

x1,…,xn называют свободными.

c) Если A(x) есть формула, в которой предметная переменная x либо является

свободной, либо вовсе не встречается, то "xA(x) и $xA(x) также суть

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

связанной, а формула A(x) – областью действия квантора.

d) Если A и B – формулы, такие, что одна и та же предметная переменная не

встречается связанной в одной формуле и свободной в другой, то (AÚB) –

формула.

e) Если A – формула, то A – формула.

Как и в исчислении высказываний, для сокращения записи введем новые символы

операций: &, ⇒, Û, а также правила для экономии скобок. Как и раньше, будем

опускать внешние скобки и скобки под чертой отрицания. Будем считать, что кванторы

связывают сильнее, чем конъюнкция, конъюнкция связывает сильнее, чем дизъюнкция,

а дизъюнкция, в свою очередь, сильнее, чем импликация и эквивалентность. Также

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

восстановить, пересчитав использованные места.

К прежним аксиомам добавим еще две:

A5: "xF(x)⇒ F( y)

A6: F( y)⇒$xF(x)

Правила вывода включают правило подстановки (α), правило заключения (β), схемы

для кванторов (γ) и правило переименования связанных переменных (δ).

Правило подстановки:

α1: в тезисе можно заменить любое простое высказывание, всюду, где оно

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

получается формула и, кроме того, подставляемая формула не содержит

предметной переменной, являющейся связанной в исходном тезисе.

α2: в тезисе можно заменить любую свободную предметную переменную,

всюду, где она встречается в нем, любой другой предметной переменной, не

являющейся связанной в исходном тезисе.

Аксиоматическая система Гильберта-Аккермана

© М.А. Сабуров, 2007 12

α3: в тезисе можно заменить любую n-местную предикатную переменную,

всюду, где она встречается в нем, любой формулой A, содержащей по меньшей

мере n свободных переменных (обозначим их x1,…,xn), при условии, что ни одна

из прочих свободных переменных, возможно, входящих в A, не является

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

При замене каждого вхождения заменяемой предикатной переменной вместо

каждой предметной переменной xi в формулу A подставляется переменная,

стоящая на i-том месте при данном вхождении заменяемой предикатной

переменной; при этом заменяются обязательно все вхождения xi в A.

Правило заключения сохраняется в неизменном виде:

β: A⇒B , A |– B.

Схемы для кванторов предполагают, что предметная переменная x является

свободной в формуле B(x) и не встречается в формуле A:

γ1: A⇒B(x) |– A⇒"xB(x) .

γ2: B(x)⇒A |– $xB(x)⇒A.

Правило переименования связанных переменных:

δ: в тезисе можно заменить любую связанную предметную переменную при

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

действия этого квантора на другую предметную переменную при условии, что

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

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

Показать полностью…
Похожие документы в приложении