О понятии логического следования

Эта ссылка позволила нам дать компактную аксиомати-зацию, но не является обязательной. С равным успехом мы могли бы оставить одно лишь правило R.2, a R.1 за-менить на несколько аксиом, соответствующих аксио-мам булевой алгебры, по правилу: если А = В - аксиома булевой алгебры, то к набору наших аксиом-выводи-мостей мы добавляем две новые - {А}||-В и {В}||-А. Так как по нашему определению выводимости слева от знака ||- всегда стоит множество, мы будем опускать фигурные скобки и символ операции объединения мно-жеств формул. Запись двух множеств формул через за-пятую Г, Д служит сокращением для ГиД, запись двух формул А, В - сокращением для {А, В} и т.д. Дадим определение доказательства в нашем исчис-лении. Def.6 Доказательством называется непустая конеч-ная последовательность, каждый из элементов которой является либо доказуемой формулой классического ис-числения высказываний вида А=В, либо аксиомой-выводимостью А.1-А.З, либо выводимостью, получен-ной из предыдущих элементов последовательности по правилам R.1-R.2. Доказанной считается выводимость, являющаяся конечным элементом последовательности. Покажем непротиворечивость построенного исчис-ления. Для этого нам надо показать, что всякая доказуе-мая выводимость обладает свойством следования. Теорема о непротиворечивости ACL. Если ГЦ-А, то Г||=А. 51