V. Вывод

Вывод из, возможно пустого, списка гипотез (формул) Г (для) формулы А – это последовательность формул заканчивающаяся формулой А и такая, что каждая из них есть либо аксиома, либо одна из гипотез, либо непосредственное следствие предыдущих формул по одному из правил вывода. Формулы из списка Г называются гипотезами или посылками вывода. О формуле А говорят, что она выводима (имеет вывод) из гипотез Г.

Вывод – это вывод из пустого списка гипотез.

Теорема – формула имеющая вывод.

Формула А зависима от списка формул Г, если есть вывод ее из Г не использующий аксиомы. Список формул независим (формулы списка независимы друг от друга), если ни одна из них не зависит от остальных.

Аксиома независима, если она не зависит от остальных аксиом.

В метаязыке утверждение о выводимости формулы А из списка гипотез Г называют секвенцией и записывают с помощью знака выводимости ® в виде

Г ®А

– “из списка гипотез Г выводится формула А” или “формула А следует из гипотез Г ”.

В случае пустого списка гипотез Г =Æ пишут секвенцию

→ А

– “формула А выводима (доказуема)”,”существует вывод формулы А”,” формула А есть теорема”.

Если для списка формул-гипотез Г существует формула А, которая выводима из этого списка как и ее отрицание А, т.е. если существует формула, для которой одновременно Г А и Г А, то список формул-гипотез называется противоречивым и пишут секвенцию.

Г

-“ список гипотез Г противоречив”.

Cеквенцию

можно рассматривать как утверждение о противоречивости теории. Для ИВ это ложная секвенция (непротиворечивость ИВ).

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

_ив, _иис,_ип,….

Запись вывода в метаязыке (протокол вывода) начинают знаком начала вывода (доказательства) ◄‚ после которого иногда указывают формальную систему, в которой проводится рассмотрение и/или основную идею вывода, а заканчивают вывод знаком конца вывода (доказательства) 8. Для удобства ссылок удобно нумеровать формулы последовательности–вывода, для чего перед формулой с отступом от нее пишется ее порядковый номер в рассматриваемом выводе – соответствующая цифра с точкой. Формулы в выводе удобно сопровождать комментарием, достаточным для того, чтобы без напряжения можно было понять, какой именно гипотезой или аксиомой и при каких именно формулах-составляющих она является, или следствием каких предыдущих формул и по какому именно правилу вывода она получена. Очевидно, для этого необходимо перенумеровать аксиомы, гипотезы и правила вывода, если их больше одного; часто вместо номера удобно пользоваться собственными именами некоторых из этих объектов. Комментарий с отступом пишут после строки в которой написана формула в квадратных скобках располагая его в укороченном абзаце, так что формулы выделяются в столбце текста с комментарием. Примеры расшифровки комментариев:

[ G 2] ¾ гипотеза с номером 2;

[ А5 с. А =¼, В =¼, С =¼] - схема аксиом 5 со значениями формул –составляющих, вместо которых здесь написаны многоточия;

[R8 из 14 и 7] - формула получена по допустимому правилу вывода с номером 8 из формул 14 и 7 рассматриваемого вывода;

[MR из 3 к 17 ]- формула получена по МР из формул 3 и 17 рассматриваемого вывода.