Главная страница Случайная страница
КАТЕГОРИИ:
АвтомобилиАстрономияБиологияГеографияДом и садДругие языкиДругоеИнформатикаИсторияКультураЛитератураЛогикаМатематикаМедицинаМеталлургияМеханикаОбразованиеОхрана трудаПедагогикаПолитикаПравоПсихологияРелигияРиторикаСоциологияСпортСтроительствоТехнологияТуризмФизикаФилософияФинансыХимияЧерчениеЭкологияЭкономикаЭлектроника
Метатеорема о дедукции.
|
|
Впервые данная теорема была сформулирована в 1930 году Эрбраном. Поэтому иногда ее называют теоремой Эрбрана. Но как общий методологический принцип, характеризующий аксиоматические дедуктивные системы, она появилась у А.Тарского.
Метатеорема о дедукции формулируется так:
Если А1,... Аn-1, Аn |- В, то А1,... Аn-1 |- Аn É В.
То есть если из формул А1,... Аn-1 и Аn выводимо В, то из формул А1,... Аn-1 выводима импликация Аn É В.
Другими словами: «Если дано доказательство формулы В из А1,... Аn-1, Аn, то можно построить на его основе доказательство импликации Аn É В из А1,... Аn-1».
Выводимость формулы на основе теоремы о дедукции характеризуется тремя особенностями, выражаемыми в следующих правилах:
а) из произвольных формул А1,... Аn выводима каждая из этих формул:
А1,... Аn |- Аi где 1 Ô і Ô n;
б) из произвольных формул А1,... Аn выводима каждая формула, выводимая в S2:
А1,... Аn |- R (R – выводимая формула в S2);
в) если из произвольных формул А1,... Аn выводимы посылки правила МР, то из них также выводимо заключение правила MP.
Данные особенности выводимости (дедукции) становятся очевидными на основе следующих семантических соображений:
1). Особенность а) выражает свойство рефлексивности следования «посылка следует из самой себя»: А |= А, так как |= А É А.
2). Особенность б) выражает свойство истинных (выводимых) формул «каждая истиная формула рассматривается в качестве консеквента логически истинной импликации с произвольным антецедентом».
3). Особенность в) фиксируется следующим образом: «если из А1,... Аn |- В¢ и из
А1,... Аn |- В¢ É В¢ ¢, то |= В¢ É В¢ ¢, а это возможно, когда |= В¢ ¢».
Перейдем к доказательству метатеоремы о дедукции:
Пусть вывод формулы В из посылок А1,... Аn-1, Аn представляет из себя последовательность формул B1, B2, … Bm, где Bm = В. Преобразуем каждую формулу Bi (і = 1, 2, …m) в формулу Аn É Вi. Тогда плучим последовательность формул Аn É В1, Аn É В2 , … Аn É Вm. В ней последней формулой является нужное нам заключение, но, к сожалению, эта последовательность в общем случае не может считаться доказательством формулы B.
Чтобы превратить ее в нужное нам доказательство, потребуется между некоторыми формулами данной последовательности вставить дополнительные формулы такие, чтобы рассматриваемая последовательность превратилась в вывод Аn É В из гипотез А1,... Аn-1. Для каждого і = 1, 2, …m выбор тех формул, которые следует поместить перед формулой Аn É Вi, зависит от основания, по которому Вi вошло в последовательность B1, B2, … Bm. Здесь возможны четыре случая, которые мы сейчас рассмотрим.
І. Вi может быть одним из допущений А1,... Аn-1, например, Вi = А1. В этом случае формула Аn É Вi имеет вид Аn É А1. Тогда перед данной формулой вставляем следующую последовательность формул:
1) А1 допущение
2) А É (В É А). - А 1
3) А1 É (Аn É A1) - по п/п в 1: А/А1, В/Аn
4) Аn É А1 - по МР к 1,, 3.
П. Вi является последним допущением, то есть Вi = Аn. Тогда перед формулой Аn É Аn вставляем следующую последовательность формул:
1) А É А - теоремa в S2
2) Аn É Аn - по п/п в 1: А/Аn.
Ш. Вi является аксиомой. Тогда перед Аn É Вi вставляем следующую последовательность формул:
1) Вi - аксиома
2) А É (В É А). - А 1
3) Вi É (Аn É Вi) - по п/п в 2: А/ Вi, В/Аn
4) Аn É Вi - по МР к 1,, 3.
IV. Вi получается из двух предыдущих формул Вj Вk(j, k < i) последовательности
B1, B2, … Bm применением правила MP. В этом случае формула Вk имеет вид Вj É Вi, и интересующая нас часть последовательности B1, B2, … Bm имеет следующий вид:
p) Аn É Вj
……………
q) Аn É (Вj É Вi)
…………….
r) Аn É Вi.
Чтобы данная последовательность давала вывод Аn É Вi, преобразуем ее следующим образом:
p) Аn É Вj
………………
q) Аn É (Вj É Вi)
q + 1) (А É (В É С) É ((А É В) É (А É С)) -- A2
q + 2) (Аn É (Вj É Bi) É ((Аn É Вj) É (Аn É Bi)) - по п/п в q + 1): A/An, B/Bj, C/Bi
q + 3) (Аn É Вj) É (Аn É Bi) - по MP к q), q + 2)
q + 4) (Аn É Bi) - по MP к p), q + 3).
Рассмотренные варианты доказательства метатеоремы о дедукции показывают, что она описывает одно из фундаментальных свойств исчислений, суть которого состоит в том, что формула, доказуемая из множества гипотез, может соединяться посредством импликации в качестве консеквента с любой из гипотез или их конъюнкцией и подобная импликация также будет доказуемой формулой.
3. Металогические принципы в S2.
Свойства разрешимости, непротиворечивости, полноты и независимости (аксиом) называют металогическими принципами. Анализируют данные принципы путем доказательства соответствующих метатеорем.