25. Свойства дедуктивных теорий

Выберем один из трех способов задания теорем дедуктивной теории. Из-

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

по-лучать различные множества теорем Т. Это множество Т - множество

теорем (множество доказуемых формул) является существенной

характеристикой дедуктивной теории.

Может оказаться, что множество теорем Т покрывает все множество формул

(правильно построенных выражений) теории. Иначе, это означает, что до-

казуема любая формула (правильно построенное выражение) и если в теории

есть отрицание, то из доказуемости какой-то формулы тут же следует

доказуемость ее отрицания. Следовательно, в этом случае доказуем какой-то

факт и его отрицание. Ясно, что теории, в которых можно доказать, что

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

Дедуктивные теории, в которых множество теорем покрывает все множество

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

в противном случае – непротиворечивыми. Выяснение непротиворечивости

дедуктивной теории является одной из важнейших проблем. К сожалению,

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

Пусть множество теорем Т является частью, не совпадающей со всем

множеством формул (правильно построенных выражений) Ф, т.е. наша дедук-

тивная теория непротиворечива. Тогда можно уже интересоваться, а какую

часть Ф занимают теоремы. Для этого вводят свойство полноты теории. Свой-

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

каких-то целей. В зависимости от того, для каких целей должно быть

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

полноты.

Рассмотренные свойства - непротиворечивость и полнота, являются важ-

нейшими свойствами дедуктивной теории. Кроме этих свойств, имеется и ряд

других свойств. Рассмотрим еще два свойства дедуктивной теории.

Независимость аксиом теории. Отдельная аксиома дедуктивной теории,

называется независимой, если эту аксиому нельзя вывести в этой теории из

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

них нельзя вывести из остальных.

Разрешимость теории. Дедуктивная теория называется разрешимой, если в

этой теории понятие теоремы эффективно, т.е. существует правило (метод),

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

нить, является она теоремой или нет.

Пусть заданы две дедуктивные теории B1 и B2 такие, что:

1) алфавит теории B1 содержится в алфавите теории B2 или эти алфавиты

совпадают,

2) каждая формула из B1 является формулой из B2

3) каждая теорема из B1 является теоремой в B2

При выполнении этих условий говорят, что теория B2 является расшире-нием

теории B1.

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

теорий (полуформальную и формальную аксиоматическую теорию,

естествен-ный вывод), их свойства, а также примеры таких теорий.

40

26. Формальные аксиоматические теории

Как уже известно, формальная аксиоматическая теория B считается за-

данной, если:

1. Задано некоторое множество символов - алфавит теории B. Конечная

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

Алфавит, следовательно, и выражения теории, задаются эффективным

образом.

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

теории. Формулы тоже обычно задаются эффективным образом.

3. Заданы аксиомы теории B как подмножество множества формул. Если

аксиом конечное число, то их можно задать перечислением. Если же их

беско-нечное множество, то задают с помощью схем, т.е. правил построения

аксиом. Если аксиомы заданы эффективным образом, то теория B

называется эффек-тивно аксиоматизированной.

4. Задано конечное число правил вывода R1, R2,..., Rn, согласно каждому из

которых некоторая формула, именуемая непосредственным следствием (за-

ключением), непосредственно выводима из некоторого конечного множества

формул, называемых посылками. При этом для каждого Ri существует целое

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

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

не-посредственным следствием данных k формул по правилу Ri.

Выводом в B называется всякая последовательность A1, A2,...,An формул,

такая, что для каждого i (1≤ i ≤ n) формула Ai есть либо аксиома теории B,

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

последова-тельности по одному из правил вывода.

Формула А теории B называется теоремой теории B если существует вы-вод

в B, в котором последней формулой является A, такой вывод называется

выводом формулы А.

Формула А называется следствием в B множества формул G тогда и только

тогда, когда существует такая последовательность формул A1, A2,..., An, что

An=A и для любого i Ai есть либо аксиома, либо элемент G, либо непосред-

ственное следствие некоторых предыдущих формул этой

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

называется выводом А из G. Элементы G называются гипотезами или

посылками вывода. Для сокра-щения утверждения «А есть следствие G»

будем употреблять запись: G├A . Например, если G={B1,B2,...Bm}, то будем

писать

B1,B2,...,Bm ├ A.

Нетрудно видеть, что если G есть пустое множество, т. е. G =∅ то ∅ ├ A

имеет место тогда и только тогда, когда А является теоремой. Вместо ∅ ├ А

принято писать просто

├ А,

что читается: «формула А является теоремой».

Чтобы избежать путаницы там, где будут рассматриваться не одна, а не-

сколько теорий, употребляют запись

G ├ A и ├ А B B указывая индексом B на то, о какой теории идет речь.

41