Математическая логика
жүктеу/скачать 0.93 Mb.
|
| B1, B2, . . . , Bt , (1)
в которой каждая из формул Bi является либо аксиомой, либо, получена по правилам вывода из некоторых предыдущих формул последовательности (1). Эта последовательность называется доказательством формулы (теоремы). Мы будем говорить, что формула B выводима из формул U1, U2, . . . ,Un в формальной теории, если формулу B можно вывести используя правила вывода, приняв за исходные формулы U1, U2, . . . ,Un и все истинные в данном исчислении формулы. То есть, формула B выводима из формул U1, U2, . . . ,Un, называемых исходными, что записывается символически как U1, U2, . . . ,Un B, если существует такая конечная последовательность формул (1), что Bt есть B и для каждой формулы Bi выполнено одно из условий: Bi есть посылка или теорема исчисления; Bi получена из некоторых предыдущих формул последовательности (1) по правилам вывода. Последовательность (1) называется в этом случае выводом формулы B из системы посылок U1, U2, . . . ,Un. жүктеу/скачать 0.93 Mb. Достарыңызбен бөлісу:
|