Статья 261

Поэтому при построении систем натурального вывода используется понятие вывода более сложное, чем в исчислениях гильбертовского типа. Последовательность натурального вывода строится из элементов, которыми могут быть не только формулы, но и некоторые, возможно, очень сложные вспомогательные выводы, причем последние, в свою очередь, могут состоять и из формул, и из других вспомогательных выводов. Чтобы зафиксировать структуру натурального вывода, можно использовать различные средства. С этой целью, например, в первых системах Яськовского вспомогательные выводы заключались в прямоугольную рамку. Приведем простой пример.
Допустим, мы хотим построить вывод формулы из посылок. Запишем его в следующем виде.
В данном случае мы имеем не обычную в смысле гильбертовских систем, а субординатную последовательность, построенную следующим образом.