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

Пусть п е N{0}.

Определение [13, с. 143].

  • 1) Линейным доказательством формулы А называется такая последовательность А1?..., Ап формул сигнатуры а, что Ап = А, и для каждого 1 < i < п формула А{ удовлетворяет одному из следующих условий:
    • а) А, — аксиома;
    • б) А, является непосредственным следствием некоторых формул Aj и Ak (j, к < Г) по основному правилу вывода 1;
    • в) А, является непосредственным следствием формулы Ат {т < Г) по одному из основных правил вывода 2 или 3.
  • 2) Формулой, доказуемой в гильбертовском исчислении первого порядка (доказуемой формулой или теоремой) (обозначается: ЬА или ЬС1А («classic» или «S. Cleene>>)), будем называть формулу, для которой существует ее линейное доказательство.

Символ «Ь» был введён Г. Фреге (1879), который дал отдельные интерпретации его горизонтальной и вертикальной частям; данное его употребление принадлежит Дж. Россеру (1935) и С. Клини (1934).

Условимся опускать до появления других исчислений «индекс» С1 у буквы «Ь».

Обозначим Я — множество формул (которое может быть бесконечным).

Определение [13, с. 143].

  • 1) Линейным выводом формулы А из множества формул Я называется такая последовательность Аь ...,Ап формул сигнатуры а, что Ап= А, и для каждого I < п формула А(- удовлетворяет одному из условий:
    • а) А,- — аксиома;
    • б) At 6 Я;
    • в) А,- является непосредственным следствием некоторых формул Д (j < 0 по одному из основных правил вывода 1, 2, 3, причём при применении основных правил вывода 2 и 3 предметная переменная х не должна входить свободно ни в одну формулу из множества Я.
  • 2) Формулой, выводимой из множества формул Я (обозначается: Я Ь А или Я ЬС1 А), будем называть формулу, для которой существует линейный вывод из множества формул Я. В этом случае множество формул Я называется множеством гипотез.

Недоказуемость формул не следует смешивать с их недоказанностью.

Если некоторая формула в тот или иной момент времени ещё не доказана (является недоказанной формулой) в гильбертовском исчислении, то это ещё не означает, что эта формула недоказуема (т. е. не является теоремой) в этом исчислении.

Недоказанную формулу впоследствии, возможно, удастся доказать, в то время как недоказуемая формула не может быть доказана принципиально (если, конечно, гильбертовское исчисление является непротиворечивым исчислением). Иначе говоря, не все недоказанные формулы являются недоказуемыми формулами.

Определение.

1) Отношением выводимости назовём (и обозначим «Ь») бинарное отношение между множествами 2F и F, которое определим так:

2) Отношением доказуемости назовем (и обозначим «Ь») бинарное отношение между множествами 0 и F, которое определим так:

И, если Л — формула, выводимая из множества аксиом;

def Л, если неверно, что А — формула, выводимая из аксиом;

Ь А = <

не определено, если не установлен ни один из предыдущих случаев;

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

Итак, отношение выводимости Н Ь А является частично определённым отношением, так как выводимость Л из множества Н либо имеет место, либо не установлено ни то, ни другое, т. е. имеет место «неопределённостъ» или «неизвестность» в смысле С. К. Клини [19, §64].

Сформулируем на языке исследователя несколько лёгких неформальных утверждений, которые будем называть общими свойствами отношения «Ь», ибо формулировка свойств не зависит от акси- омных схем и правил вывода.

Предложение (общие свойства отношения выводимости) [19, с. 83—84].

  • 1) Н Ь А, если А е Н (рефлексивность);
  • 2) если Н1 Ь Л, то Нг и Н2 Ь А для любого множества формул Н2 (в частности, можно рассматривать любую доказуемую формулу как выводимую из любого множества гипотез) Смонотонность);
  • 3) если Н] I- А, то Н2 Ь А, где множество Н2 получается из множества Нг удалением любых формул, которые являются доказуемыми или выводимыми из остающихся формул множества Н3 (транзитивность).

Утверждение 3 данного Предложения может быть сформулировано следующим образом: если Аь ..., Ап, В, С — формулы,

то ьА2, ..., AJ Ь С.

 
Посмотреть оригинал
< Пред   СОДЕРЖАНИЕ   ОРИГИНАЛ     След >