Независимость системы аксиом теории

Создавая аксиоматическую теорию, естественно стремиться не выписывать лишних аксиом – тех, которые выводимы из остальных. Система аксиом формальной теории называется независимой, если ни одна аксиома этой системы не выводима из остальных. Более формально, ситема {A_i}_{i Î I} независима, если для любой аксиомы А_i и любого конечного множества аксиом Г Í {A_j}_{j Î I \ {i}} утверждение Г А_i неверно.

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

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

Как доказать независимость той или иной системы аксиом ? Основным методом доказательства является метод построения независимых моделей, основанный на следующей теореме:

Теорема (критерий независимости системы аксиом).Система аксиом (схем аксиом) {A_i}_{i Î I} независима тогда и только тогда, когда для каждого i Î I существует модель для системы аксиом (схем аксиом) {A_j}_{j Î I \ {i}} , в которой аксиома (схема аксиом) А_i ложна.

Доказательство. Ясно, что существование модели с указанным в формулировке теоремы свойством показывает, что утверждение Г А_i для любого конечного множества аксиом Г Í {A_j}_{j Î I \ {i}} неверно.

Обратно, если аксиома А_i не выводима из остальных, то непротиворечивой будет система аксиом Г_i = {A_j}_{j Î I \ {i}} È {} . Действительно, если бы эта система была противоречива, то любая формула была бы доказуема (выводима из некоторой конечной совокупности аксиом Г È {}, где Г Í Г_i ). Поэтому Г, A_i и, очевидно, Г, . По правилу опровержения отсюда следует, что Г , т.е. (с учётом аксиомы ® A_i ) верно Г А_i – противоречие. У непротиворечивого множества аксиом Г_i = {A_j}_{j Î I \ {i}} È {} существует модель, в которой аксиома А_i ложна, что и требовалось.

Теорема доказана.

Теорема (о независимости системы аксиом исчисления высказываний).Система аксиом формального исчисления высказываний (приведённая в § 1 главы III) независима.

Доказательство. Используем метод построения независимых моделей: для каждой схемы аксиом построим модель, в которой эта схема аксиом ложна, а остальные истинны. Все модели будут устроены однообразно: на некотором конечном множестве М определим функции из М в М : Ù , Ú , ® от двух аргументов и – от одного, которые будут интерпретировать логические связки исчисления высказываний. В каждом случае будет выделено некоторое подмножество И Í М, в котором находятся значения всех “истинных” в модели М схем аксиом, в отличие от независимой от них (“ложной” в М) схемы аксиом, которая принимает значения и не лежащие во множестве И. При этом применение правила modus ponens к формулам, имеющим значения только в И (к “истинным” в модели формулам), приводит снова к формуле, имеющем значения снова во множестве И (к “истинной” в модели формуле). Таким образом, все выводимые из “истинных” формул формулы снова будут истинными, а любая “ложная” формула не выводима из “истинных”. Итак, рассматриваемая в каждом случае “ложная” схема аксиом не выводится из остальных “истинных” аксиом.

Все вычисления подробно производиться не будут (это – задание для самостоятельной работы), но конструкции моделей будут описаны точно.Посколькусвязка импликации участвует во всех аксиомах исчисления высказываний, доказательство независимости аксиом группы импликации наиболее трудоёмко.

Независимость схемы (И1): (А ® (B ® A)) .Рассмотрим трёхэлементное множество М = {0, 1, 2} и определим на нём новое исчисление логических связок, полагая для x, y Î M следующие значения связок: x Ù y = min{x, y}, x Ú y = = max{x, y}, x ® y = , = 2 – x .

Проверим, что все схемы аксиом, кроме (И1) дают значения во множестве И = {2}, множество “истинных” формул замкнуто относительно правила modus ponens, а схема аксиом (И1) принимает значения не только во множестве И. Всё это проверяется путём построения многочисленных таблиц истинности.

А	В	В ® A	А ® (B ® A)		А	В	А ® В
0	0	2			0	0	2
1	0	2			1	0	0
2	0	2			2	0	0
0	1	0			0	1	2
1	1	2			1	1	2
2	1	2			2	1	0
0	2	0			0	2	2
1	2	0			1	2	2
2	2	2			2	2	2

 

Таблица слева показывает, что схема аксиом (И1) не всегда принимает значения во множестве И = {2}, а потому “ложна в рассматриваемой модели”. Таблица справа доказывает, что множество “истинных” формул замкнуто относительно правила modus ponens (более точно, если А = 2 = (А ® B) , то B = 2).

Наконец, проверим, что все остальные схемы аксиом “истинны” в этой модели, т.е. принимают значения только во множестве И = {2}:

А	В	С	А ® B	А ® C	B ® C	A ® (B ® C)	(A ® B) ® (А ® C)	(И2)	В Ù C	A ® (B Ù C)	(A ® С) ® (A ® (B Ù C))	(К3)	А Ú В	(A Ú B) ® C	(B ® C) ® ((A Ú B) ® C)	(Д3)
0	0	0	2	2	2	2	2		0	2	2		0	2	2
1	0	0	0	0	2	2	2		0	0	2		1	0	2
2	0	0	0	0	2	2	2		0	0	2		2	0	2
0	1	0	2	2	0	2	2		0	2	2		1	0	2
1	1	0	2	0	0	0	0		0	0	2		1	0	2
2	1	0	0	0	0	0	2		0	0	2		2	0	2
0	2	0	2	2	0	2	2		0	2	2		2	0	0
1	2	0	2	0	0	0	0		0	0	2		2	0	2
2	2	0	2	0	0	0	0		0	0	2		2	0	2
0	0	1	2	2	2	2	2		0	2	2		0	2	2
1	0	1	0	2	2	2	2		0	0	0		1	2	2
2	0	1	0	0	2	2	2		0	0	2		2	0	2
0	1	1	2	2	2	2	2		1	2	2		1	2	2
1	1	1	2	2	2	2	2		1	2	2		1	2	2
2	1	1	0	0	2	2	2		1	0	2		2	0	2
0	2	1	2	2	0	2	2		1	2	2		2	0	0
1	2	1	2	2	0	0	2		1	2	2		2	0	0
2	2	1	2	0	0	0	0		1	0	2		2	0	2
0	0	2	2	2	2	2	2		0	2	2		0	2	2
1	0	2	0	2	2	2	2		0	0	0		1	2	2
2	0	2	0	2	2	2	2		0	0	0		2	2	2
0	1	2	2	2	2	2	2		1	2	2		1	2	2
1	1	2	2	2	2	2	2		1	2	2		1	2	2
2	1	2	0	2	2	2	2		1	0	0		2	2	2
0	2	2	2	2	2	2	2		2	2	2		2	2	2
1	2	2	2	2	2	2	2		2	2	2		1	2	2
2	2	2	2	2	2	2	2		2	2	2		2	2	2

Таблица показывает, что схемы (И2), (К3), (Д3) “истинны” в этой модели.

А	В	А Ù В	К1	К2	А Ú В	Д1	Д2			О1	О2	A ® B	®	О3
0	0	0			0			2	0			2	2
1	0	0			1			1	1			0	0
2	0	0			2			0	2			0	0
0	1	0			1			2	0			2	2
1	1	1			1			1	1			2	2
2	1	1			2			0	2			0	0
0	2	0			2			2	0			2	2
1	2	1			2			1	1			2	2
2	2	2			2			0	2			2	2

Итак, схемы аксиом (К1), (К2), (Д1), (Д2), (О1), (О2), (О3) тоже “истинны” в построенной модели. Поэтому доказана независимость аксиомы (И1) от остальных аксиом формального исчисления высказываний.

Независимость схемы (И2): ((А ® (B ® С)) ® ((A ® B) ® (A ® C))) . Возьмём М = {0, 1, 2}, И = {0} и определим для x, y Î M следующие значения связок: x Ù y = max{x, y}, x Ú y = min{x, y}, x ® y = max{0, y – x}, = 2 – x.

Проверьте самостоятельно, что все схемы аксиом, кроме (И2) принимают значения во множестве И, множество “истинных” формул замкнуто относительно правила modus ponens, а схема аксиом (И2) принимает значения не только во множестве И.

Независимость схемы (К1): ((A Ù B) ® A) . Возьмём М = {0, 1}, И = {1} и определим для элементов x, y Î M следующие значения логических связок: x Ù y = y, а остальные связки Ú , ® , интерпретируем стандартно.

Следующие таблицы доказывают, что схема аксиом (К1) “ложна в рассматриваемой модели”, а множество “истинных” формул замкнуто относительно правила modus ponens (более точно, если А = 1 = (А ® B) , то B = 1):

 

 

Проверим теперь истинность остальных аксиом.

А	В	А Ù В	К2	А Ú В	Д1	Д2			О1	О2	А ® B	®	О3
0	0	0		0			1	0			1	1
1	0	0		1			0	1			0	0
0	1	1		1			1	0			1	1
1	1	1		1			0	1			1	1

 

А	В	С	А ® В	А ® C	B ® C	B ® А	И1	A ® (B ® C)	(A ® B) ® (А ® C)	И2	В Ù C	A ® (B Ù C)	(A ® С) ® (A ® (B Ù C))	К3	А Ú В	(A Ú B) ® C	(B ® C) ® ((A Ú B) ® C)	Д3
0	0	0	1	1	1	1		1	1		0	1	1		0	1	1
1	0	0	0	0	1	1		1	1		0	0	1		1	0	0
0	1	0	1	1	0	0		1	1		0	1	1		1	0	1
1	1	0	1	0	0	1		0	0		0	0	1		1	0	1
0	0	1	1	1	1	1		1	1		1	1	1		0	1	1
1	0	1	0	1	1	1		1	1		1	1	1		1	1	1
0	1	1	1	1	1	0		1	1		1	1	1		1	1	1
1	1	1	1	1	1	1		1	1		1	1	1		1	1	1

 

Независимость схемы (К2): ((A Ù B) ® B) . Докажите самостоятельно, видоизменив интерпретацию конъюнкции.

Независимость схемы (К3): ((A ® B) ® ((A ® C) ® (A ® (B Ù C)))) . Возьмём М = {0, 1}, И = {1} и определим для элементов x, y Î M следующие значения логических связок: x Ù y = 0, а остальные связки Ú , ® , интерпретируем стандартно.

Ясно, что множество “истинных” формул замкнуто относительно правила modus ponens (импликация стандартна).

Схема аксиом (К3) “ложна в рассматриваемой модели”, т.к. принимает значение 0 Ï И при А = В = С = 1. Среди остальных аксиом нужно проверять только схемы (К1) и (К2), которые, очевидно, будут принимать всегда значение 1, т.к. А Ù В = 0 и импликация вычисляется стандартно.

Независимость схемы (Д1): (A ® (A Ú B)) . Проверки аналогичны вычислениям для схемы (К1): берём М = {0, 1}, И = {1}, и для элементов x, y Î M полагаем x Ú y = y, интерпретируя остальные связки Ù , ® , стандартно.

Независимость схемы (Д2): (B ® (A Ú B)) . Докажите самостоятельно, видоизменив интерпретацию дизъюнкции.

Независимость схемы (Д3): ((A ® C) ® ((B ® C) ® (A Ú B ® C))) . Проверки аналогичны вычислениям для схемы (К3): берём М = {0, 1}, И = {1}, и для элементов x, y Î M полагаем x Ú y = 1, интерпретируя остальные связки Ù , ® , стандартно.

Независимость схемы (О1): (А ® ) . Пусть М = {0, 1, 2}, И = {2} и определим для x, y Î M новые значения логических связок: x Ù y = min{x, y}, x Ú y = max{x, y}, . Проделайте все вычисления самостоятельно.

Независимость схемы (О2): ( ® А) . Полагаем М = {0, 1, 2}, И = {2} и определим для x, y Î M новые значения логических связок: x Ù y = min{x, y} , x Ú y = max{x, y}, . Проделайте все вычисления самостоятельно.

Независимость схемы (О3): ((A ® B) ® (® )) . Здесь М = {0, 1}, И = {1} и для элемента x Î M новое значение отрицания = x , а остальные связки Ù , Ú , ® стандартны. Проделайте все вычисления самостоятельно.

Если рассматривать исчисление высказываний с эквивалентностью, то нужно доказать ещё независимость аксиом эквивалентности (Э1) и (Э2).

Независимость схемы (Э1): ((A « B) ® (( А ® В) Ù (В ® A))) . Нужно взять М = {0, 1}, И = {1} и определить x « y = 1, а все остальные логические связки Ù , Ú , ® интерпретировать стандартно. Проделайте все вычисления самостоятельно.

Независимость схемы (Э2): ((( А ® В) Ù (В ® A)) ® (A « B)) . Нужно взять М = {0, 1}, И = {1} и определить x « y = 0, а все остальные логические связки Ù , Ú , ® интерпретировать стандартно. Проделайте все вычисления самостоятельно.

Теорема о независимости системы аксиом полностью доказана.

Теорема (о независимости аксиом исчисления предикатов).Система аксиом формального исчисления предикатов независима.

Доказательство. Проведём рассуждения схематично. Доказательство независимости схем аксиом исчисления высказываний остаются в силе, если значениям формул (" x A(x)) и ($ x A(x)) с навешенными кванторами вычислять на моделях стандартным образом.

Независимость схемы ("): ((" x А(x)) ® А(t)) . Достаточно интерпретировать логические связки стандартно, как и значения формул с навешенным квантором существования, а формулы с навешенными кванторами всеобщности всегда считать истинными. Тогда, например, аксиома ((" x P(x)) ® P(t)) будет принимать значение 0, если P(t) = 0. Остальные аксиомы при этом останутся тождественно истинными.

Независимость схемы ($): (А(t) ® ( $ x А(x))). Достаточно интерпретировать логические связки стандартно, как и значения формул с навешенными кванторами всеобщности, а формулы с навешенными кванторами существования всегда считать ложными. Тогда, например, аксиома (P(t) ® ($ x P(x))) будет принимать значение 0, если P(t) = 0. Остальные аксиомы при этом останутся тождественно истинными.

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