V.Вывод
Вывод из, возможно пустого, списка гипотез (формул) Г (для) формулы А – это последовательность формул заканчивающаяся формулой А и такая, что каждая из них есть либо аксиома, либо одна из гипотез, либо непосредственное следствие предыдущих формул по одному из правил вывода. Формулы из списка Г называются гипотезами или посылками вывода. О формуле А говорят, что она выводима (имеет вывод) из гипотез Г.
Вывод – это вывод из пустого списка гипотез.
Теорема – формула имеющая вывод.
Формула А зависима от списка формул Г, если есть вывод ее из Г не использующий аксиомы. Список формул независим (формулы списка независимы друг от друга), если ни одна из них не зависит от остальных.
Аксиома независима, если она не зависит от остальных аксиом.
В метаязыке утверждение о выводимости формулы А из списка гипотез Г называют секвенцией и записывают с помощью знака выводимости ®в виде
Г ®А
–“из списка гипотез Г выводится формула А” или “формула А следует из гипотез Г”.
В случае пустого списка гипотез Г=Æ пишут секвенцию
→ А
– “формула А выводима (доказуема)”,”существует вывод формулы А”,”формула А есть теорема”.
Если для списка формул-гипотез Г существует формула А, которая выводима из этого списка как и ее отрицание А, т.е. если существует формула, для которой одновременно ГА и ГА, то список формул-гипотез называется противоречивым и пишут секвенцию.
Г
-“список гипотезГ противоречив”.
Cеквенцию
можно рассматривать как утверждение о противоречивости теории. Для ИВ это ложная секвенция (непротиворечивость ИВ).
При одновременном рассмотрении разных теорий и, соответственно, разных понятий выводимости, знак выводимости снабжают индексом, указывающим теорию, к которой он относится: так
ив, иис,ип,….
Запись вывода в метаязыке (протокол вывода) начинают знаком начала вывода (доказательства) ◄‚ после которого иногда указывают формальную систему, в которой проводится рассмотрение и/или основную идею вывода, а заканчивают вывод знаком конца вывода (доказательства) 8. Для удобства ссылок удобно нумеровать формулы последовательности–вывода, для чего перед формулой с отступом от нее пишется ее порядковый номер в рассматриваемом выводе – соответствующая цифра с точкой. Формулы в выводе удобно сопровождать комментарием, достаточным для того, чтобы без напряжения можно было понять, какой именно гипотезой или аксиомой и при каких именно формулах-составляющих она является, или следствием каких предыдущих формул и по какому именно правилу вывода она получена. Очевидно, для этого необходимо перенумеровать аксиомы, гипотезы и правила вывода, если их больше одного; часто вместо номера удобно пользоваться собственными именами некоторых из этих объектов. Комментарий с отступом пишут после строки в которой написана формула в квадратных скобках располагая его в укороченном абзаце, так что формулы выделяются в столбце текста с комментарием. Примеры расшифровки комментариев :
[G2] ¾ гипотеза с номером 2;
[А5 с. А=¼, В=¼, С=¼] - схема аксиом 5 со значениями формул –составляющих, вместо которых здесь написаны многоточия;
[R8 из 14 и 7] - формула получена по допустимому правилу вывода с номером 8 из формул 14 и 7 рассматриваемого вывода;
[MR из 3 к 17 ]- формула получена по МР из формул 3 и 17 рассматриваемого вывода.